MASA : Systèmes Multi-Agents Pilotés par LLM pour l'Autoformalisation

Informations Fondamentales

• ID de l'article : 2510.08988
• Titre : MASA: LLM-Driven Multi-Agent Systems for Autoformalization
• Auteurs : Lan Zhang (University of Manchester), Marco Valentino (University of Sheffield), André Freitas (University of Manchester, Idiap Research Institute, National Biomarker Centre)
• Classification : cs.CL (Linguistique Computationnelle), cs.FL (Langages Formels)
• Date de publication : 10 octobre 2025 (prépublication arXiv)
• Lien de l'article : https://arxiv.org/abs/2510.08988

Résumé

L'autoformalisation joue un rôle crucial dans la connexion entre le langage naturel et le raisonnement formel. Cet article propose MASA, un cadre de construction de systèmes multi-agents pilotés par des modèles de langage de grande taille (LLMs) pour les tâches d'autoformalisation. MASA exploite des agents collaboratifs pour convertir les énoncés en langage naturel en leurs représentations formelles. L'architecture de MASA met l'accent sur la modularité, la flexibilité et l'extensibilité, permettant l'intégration transparente de nouveaux agents et outils pour s'adapter à l'évolution rapide du domaine. Les auteurs démontrent l'efficacité de MASA par des cas d'usage impliquant des définitions mathématiques du monde réel et des expériences sur des ensembles de données de mathématiques formelles. Ce travail souligne le potentiel des systèmes multi-agents pilotés par les LLMs et l'interaction avec les prouveurs de théorèmes pour améliorer l'efficacité et la fiabilité de l'autoformalisation.

Contexte de Recherche et Motivation

Définition du Problème

L'autoformalisation est la tâche de convertir automatiquement des énoncés mathématiques en langage naturel en formules logiques formelles vérifiables par machine. Les défis fondamentaux de ce problème sont :

1. Fossé sémantique : Écart considérable entre l'ambiguïté du langage naturel et la rigueur du langage formel
2. Complexité : Les énoncés mathématiques du monde réel impliquent souvent des concepts complexes et des chaînes de raisonnement élaborées
3. Exigences de précision : Les résultats formalisés doivent être corrects tant sur le plan syntaxique que sémantique

Importance du Problème

L'autoformalisation revêt une importance significative :

• Vérification mathématique : Fournit une base pour la preuve de théorèmes et la vérification mathématique
• Transparence du raisonnement : Le raisonnement formel est plus systématique, transparent et rigoureux que le raisonnement en langage naturel
• Besoin d'automatisation : La formalisation manuelle nécessite des connaissances spécialisées considérables et des investissements temporels

Limitations des Approches Existantes

Les systèmes d'autoformalisation basés sur les LLMs existants présentent les problèmes suivants :

1. Limitations architecturales monolithiques : Un seul LLM a du mal à traiter les problèmes d'autoformalisation complexes du monde réel
2. Manque de modularité : Les implémentations existantes manquent de modularité, de flexibilité et d'extensibilité
3. Interaction insuffisante des composants : Incapacité à intégrer efficacement plusieurs composants interactifs

Motivation de la Recherche

Les auteurs proposent le cadre MASA motivés par :

• La construction de systèmes multi-agents modulaires pour résoudre la complexité de l'autoformalisation
• La fourniture d'un cadre flexible et extensible permettant aux chercheurs de développer et d'étendre rapidement les systèmes
• L'amélioration de l'efficacité et de la fiabilité de l'autoformalisation par la collaboration entre agents

Contributions Fondamentales

1. Proposition d'un cadre multi-agents modulaire : MASA fournit un cadre modulaire pour la construction de systèmes multi-agents d'autoformalisation, offrant une bonne flexibilité et extensibilité
2. Démonstration d'applications du monde réel : Par la formalisation d'agents de définitions mathématiques du monde réel, le cadre met en évidence son potentiel pratique
3. Évaluation systématique : Évaluation du cadre dans trois configurations multi-agents, démontrant son efficacité et fournissant des perspectives précieuses. Le système d'amélioration itérative finale atteint des taux de formalisation syntaxiquement corrects et sémantiquement alignés de 35,25 % et 61,89 % respectivement sur Qwen2.5-7B et GPT-4.1-mini
4. Implémentation open-source : Fourniture de code et de données complets, réduisant les obstacles à la recherche

Détails de la Méthode

Définition de la Tâche

L'autoformalisation peut être définie comme une fonction de transformation A qui mappe un énoncé en langage naturel s à sa représentation formelle φ = A(s). Les approches traditionnelles l'implémentent via des invites LLM : A = LLM(prompt). MASA étend cette définition en implémentant un processus de transformation plus complexe via un système multi-agents.

Architecture du Modèle

Le cadre MASA comprend cinq composants fondamentaux :

1. Agent (Agent)

Les agents sont des éléments fondamentaux exécutant des fonctions spécifiques, incluant :

• AutoformalizationAgent : Exécute l'autoformalisation avec peu d'exemples
• HardCritiqueAgent : Fournit des critiques au niveau syntaxique basées sur le prouveur de théorèmes
• SoftCritiqueAgent : Fournit des critiques au niveau sémantique basées sur le LLM
• FormalRefinementAgent : Affine le code formel basé sur les critiques dures
• InformalRefinementAgent : Affine le code formel basé sur les critiques douces
• DenoisingAgent : Agent outil de débruitage
• ImportRetrievalAgent : Agent outil de récupération d'importations

2. Large Language Model (Modèle de Langage de Grande Taille)

Le LLM fournit aux agents des capacités de raisonnement et de langage, supportant :

• Les modèles OpenAI (comme GPT-4.1-mini)
• Les modèles locaux HuggingFace (comme Qwen2.5-7B, DeepSeek-Math)

3. Knowledge Base (Base de Connaissances)

Stocke les informations des bibliothèques de langages formels, supportant la récupération de connaissances pertinentes. L'implémentation actuelle comprend une base de connaissances des énoncés et preuves formels Isabelle/HOL.

4. Retriever (Récupérateur)

Classe les points de données dans les bibliothèques mathématiques par pertinence, l'implémentation actuelle étant basée sur la méthode BM25.

5. Theorem Prover (Prouveur de Théorèmes)

Vérifie la correction syntaxique et logique de la formalisation, fournissant des messages d'erreur. Supporte :

• Isabelle (via serveur dédié)
• Lean4 (via REPL)

Points d'Innovation Technique

1. Conception modulaire : Utilise une conception de classe de base abstraite, facilitant l'extension de nouveaux agents et outils
2. Mécanisme de critique multi-niveaux : Combine les critiques dures (syntaxe) et douces (sémantique)
3. Processus d'amélioration itérative : Supporte la collaboration multi-agents d'auto-amélioration
4. Intégration d'agents outils : Intègre des outils pratiques tels que le débruitage et la récupération d'importations

Configuration Expérimentale

Ensembles de Données

1. miniF2F : Fournit des formalisations réelles en Isabelle/HOL et Lean4, utilisées pour l'évaluation comparative
2. ProofNet : Fournit des formalisations réelles de code Lean4

Métriques d'Évaluation

Correction Syntaxique

• Pass Rate : Pourcentage de formalisations syntaxiquement correctes

Évaluation Sémantique

• BLEU-4 : Chevauchement d'n-grammes avec la formalisation réelle
• ChrF : F-score au niveau des caractères
• RUBY : Métrique d'évaluation de migration de code

Évaluation des Agents

• Alignment Faithfulness (AF) : Si le code formel s'aligne précisément avec la sémantique du langage naturel
• Formalization Correctness (FC) : Si le code formel lui-même est valide, naturel et bien formaté

Méthodes de Comparaison

• Invites zéro-shot (ZS) : Utilisation directe du LLM pour la formalisation
• Invites few-shot (FS) : Formalisation utilisant 3 exemples
• Différentes combinaisons de LLM : GPT-4.1-mini, DeepSeek-Math-7B, Qwen2.5-7B

Détails d'Implémentation

• Utilisation de GPT-4.1-mini comme LLM backend pour l'agent de critique douce
• Support des deux langages formels Isabelle/HOL et Lean4
• Implémentation Python complète et exemples de Jupyter Notebook

Résultats Expérimentaux

Résultats Principaux

Système d'Amélioration Formelle par Critique Dure (Tableau 1)

miniF2F-Test (Isabelle/HOL) :

• GPT-4.1-mini zéro-shot : Pass Rate 65,57 % → 77,05 % (+11,48 %)
• GPT-4.1-mini few-shot : Pass Rate 76,23 % → 86,48 % (+10,25 %)
• DeepSeek-Math few-shot : Pass Rate 29,10 % → 36,48 % (+7,38 %)

ProofNet-Test (Lean4) :

• GPT-4.1-mini zéro-shot : Pass Rate 3,30 % → 3,85 % (+0,55 %)
• GPT-4.1-mini few-shot : Pass Rate 12,09 % → 14,84 % (+2,75 %)

Système d'Amélioration Informelle par Critique Douce (Tableau 2)

miniF2F (Lean4) :

• DeepSeek-Math + GPT-4.1-mini amélioration : AF 38,52 % → 90,57 %, FC 47,54 % → 79,92 %
• Qwen2.5-7B + GPT-4.1-mini amélioration : AF 54,51 % → 93,44 %, FC 62,70 % → 85,25 %

Expériences d'Auto-Amélioration Itérative

Les résultats de la Figure 2 montrent :

• Qwen2.5-7B : Après 4 itérations, la proportion syntaxiquement correcte et sémantiquement alignée atteint 35,25 %
• GPT-4.1-mini : Après 4 itérations, la proportion syntaxiquement correcte et sémantiquement alignée atteint 61,89 %

Découvertes Expérimentales

1. Few-shot surpasse zéro-shot : L'apprentissage few-shot améliore significativement les performances dans tous les contextes
2. Impact de la capacité du modèle : Les modèles forts (GPT-4.1-mini) performent mieux dans l'amélioration formelle
3. Efficacité de l'amélioration itérative : Les itérations multiples améliorent continuellement la qualité de la formalisation
4. Amélioration inter-modèles : Les modèles forts peuvent améliorer les résultats des modèles faibles

Travaux Connexes

Recherche en Autoformalisation

• Méthodes d'invites : Wu et al. (2022) et autres utilisent les invites LLM pour l'autoformalisation
• Génération de données : Jiang et al. (2024) et Liu et al. (2025b) développent des corpus parallèles à grande échelle
• Implémentations système : Les systèmes existants manquent de modularité et d'extensibilité

Systèmes Multi-Agents

• Domaines d'application : Systèmes d'exploitation, éducation médicale, vérification de réponses, etc.
• Tâches de raisonnement : Raisonnement arithmétique et raisonnement général
• Applications d'autoformalisation : La recherche sur les systèmes multi-agents dans le domaine de l'autoformalisation est limitée

Conclusion et Discussion

Conclusions Principales

1. Efficacité du cadre : MASA a construit avec succès un système multi-agents d'autoformalisation modulaire
2. Amélioration des performances : La collaboration multi-agents améliore significativement la précision de l'autoformalisation
3. Valeur pratique : Le cadre fournit aux chercheurs une plateforme de développement flexible

Limitations

1. Absence de contrôle central : Le système manque d'un agent central pour allouer et contrôler différents agents
2. Limitations de l'évaluation sémantique : L'évaluation sémantique se limite aux jugements de haut niveau, nécessitant des critères d'évaluation plus granulaires
3. Dépendance au modèle : Les performances du système dépendent largement des capacités du LLM sous-jacent

Directions Futures

1. Amélioration du contrôle central : Développer des mécanismes de contrôle de systèmes multi-agents plus avancés
2. Affinement de l'évaluation : Établir des critères d'évaluation sémantique plus précis
3. Extension des applications : Appliquer le cadre à un éventail plus large de tâches de formalisation

Évaluation Approfondie

Points Forts

1. Innovation forte : Premier cadre systématique d'autoformalisation multi-agents
2. Conception judicieuse : L'architecture modulaire est élégante et facilement extensible
3. Expériences complètes : Couvre plusieurs configurations et métriques d'évaluation
4. Valeur pratique élevée : L'implémentation open-source réduit les obstacles à la recherche
5. Résultats convaincants : Validation de l'efficacité de la méthode sur plusieurs ensembles de données

Insuffisances

1. Analyse théorique insuffisante : Manque d'analyse théorique des mécanismes de collaboration multi-agents
2. Coût computationnel : L'analyse des frais généraux de calcul du système multi-agents est insuffisante
3. Propagation d'erreurs : Analyse insuffisante du problème de propagation d'erreurs entre agents
4. Limitations d'évaluation : L'évaluation sémantique dépend toujours du jugement du LLM, pouvant présenter des biais

Impact

1. Contribution académique : Fournit un nouveau paradigme pour la recherche en autoformalisation
2. Valeur pratique : Le cadre peut être directement utilisé pour le développement d'applications
3. Reproductibilité : L'implémentation open-source complète garantit la reproductibilité
4. Promotion du développement : Susceptible de promouvoir l'application des systèmes multi-agents dans le domaine de la formalisation

Scénarios Applicables

1. Formalisation mathématique : Appropriée pour l'autoformalisation de théorèmes et définitions mathématiques complexes
2. Applications éducatives : Peut être utilisée pour la formation à la formalisation dans l'enseignement mathématique
3. Outil de recherche : Fournit une plateforme de base pour la recherche en autoformalisation
4. Applications industrielles : Peut être intégrée dans les systèmes logiciels nécessitant une vérification formelle

Références

Les références clés incluent :

• Wu et al. (2022): Autoformalization with large language models
• Zheng et al. (2022): miniF2F: a cross-system benchmark for formal olympiad-level mathematics
• Azerbayev et al. (2023): ProofNet: Autoformalizing and formally proving undergraduate-level mathematics
• Jiang et al. (2023): Draft, sketch, and prove: Guiding formal theorem provers with informal proofs

Résumé : MASA est un cadre d'autoformalisation multi-agents innovant qui améliore significativement l'efficacité de l'autoformalisation grâce à une conception modulaire et à la collaboration entre agents. Ce travail excelle en innovation technique, validation expérimentale et valeur pratique, ouvrant de nouvelles directions pour la recherche en autoformalisation. Malgré certaines limitations, son implémentation open-source et sa bonne extensibilité en font une contribution importante au domaine.