Comment un laboratoire chinois a surmonté le goulot d'étranglement de la preuve mathématique assistée par IA

Les preuves mathématiques formelles, celles vérifiées par des machines et non par des humains, sont l'étalon-or de la rigueur. Mais traduire les preuves informelles que les mathématiciens écrivent en langage naturel vers des langages formels comme Lean reste un défi tenace et de longue haleine. Une équipe de l'Université de Nanjing et de Polixir Technologies affirme désormais avoir résolu un goulot d'étranglement clé dans ce pipeline.

Leur cadre, appelé ToMap (Test-time Optimization for Multi-Agent Proof autoformalization), traite la formalisation complète des preuves non pas comme une seule tâche de traduction, mais comme un système multi-agents en trois étapes : un Décomposeur qui divise la preuve en unités atomiques, un Formaliseur qui rend chaque unité en syntaxe Lean, et un Prouveur qui génère les tactiques pour clore chaque objectif. La découverte surprenante, publiée dans un préprint, est que le maillon le plus faible est la première étape, et que concentrer le calcul sur l'amélioration de la seule décomposition produit des gains démesurés.

Analyse du goulot d'étranglement

Pour identifier où le calcul au moment du test est le mieux utilisé, les chercheurs ont mené une expérience d'intervention contrôlée. Sous des traces d'erreur Lean identiques et un budget de correction fixe, ils ont permis à un seul des trois agents de réviser sa sortie tout en gelant les deux autres. L'intervention du Décomposeur a systématiquement atteint la précision totale de preuve la plus élevée : 51,1 % après cinq passages sur l'échantillon de 184 de ProofFlowBench, contre 45,1 % pour le Formaliseur et 33,7 % pour le Prouveur.

« Le Décomposeur définit la difficulté de chaque obligation en aval », écrivent les auteurs. Une décomposition qui produit des unités de preuve atomiques et autonomes avec des dépendances explicites réduit la formalisation et la preuve à des tâches locales que les agents en aval peuvent gérer. Des unités mal délimitées laissent l'exécuteur avec des objectifs ambigus ou incomplets.

Comment fonctionne ToMap

Plutôt que de répartir le calcul au moment du test entre les trois agents, ToMap le concentre sur le Décomposeur. Il maintient un pool de décompositions candidates en langage naturel, note chacune selon une grille tridimensionnelle (fidélité sémantique, prouvabilité, et convivialité Lean), et utilise la frontière de Pareto résultante pour guider l'évolution itérative des invites de décomposition, une technique inspirée de l'algorithme GEPA pour l'optimisation réflexive des invites.

Une porte de validation réserve le cycle coûteux en aval Formaliseur-Prouveur-vérification Lean aux candidates qui atteignent un seuil minimum sur les trois dimensions de la grille. « Le retour de la grille est peu coûteux et dense, guidant l'essentiel de la recherche, tandis que la vérification Lean fournit des signaux de vérité terrain fidèles mais coûteux, réservés aux candidates prometteuses », expliquent les auteurs.

Résultats et comparaisons

Sur ProofFlowBench, ToMap propulsé par Gemini3-Pro a atteint un score conjoint de correction syntaxique et de fidélité sémantique de 40,22 %, une amélioration de 19,0 points de pourcentage par rapport à la meilleure méthode précédente, Codex End2End (21,20 %). Sur miniF2F, l'ensemble de données de problèmes de compétition de niveau lycée, ToMap a atteint 55,74 %, soit une amélioration de 8,2 %. Le système a également surpassé les approches basées sur l'entraînement comme ProofBridge, qui nécessite un modèle de récupération et un traducteur affiné, tout en maintenant des coûts d'inférence uniquement plus faibles.

Les études d'ablation révèlent un compromis clair entre temps et performance : la plupart des gains émergent dans les 3 à 5 itérations d'évolution, après quoi les rendements diminuent. Cela donne une orientation pratique pour choisir le budget d'itération sous contraintes de latence ou de coût.

« Les méthodes qui génèrent une seule preuve Lean monolithique peuvent atteindre une correction syntaxique relativement élevée, mais elles peinent à traduire fidèlement les étapes individuelles des preuves en langage naturel », notent les auteurs. « La formalisation des preuves étape par étape préserve mieux la fidélité sémantique en alignant explicitement le processus de formalisation avec les étapes intermédiaires de la preuve. »

Limites et travaux futurs

L'évaluation est limitée à des preuves de taille benchmark, et non à des mathématiques de niveau recherche longues. Le système suppose également que les preuves d'entrée sont correctes ; traiter les preuves informelles incorrectes ou incomplètes reste un problème ouvert. Étendre le cadre pour détecter et réparer un raisonnement erroné est signalé comme un travail futur.

La contribution de l'équipe de Nanjing est moins une percée dans la capacité de raisonnement formel qu'une démonstration que l'allocation intelligente du calcul au moment du test, éclairée par une analyse systématique des goulots d'étranglement, peut extraire plus de valeur des modèles existants que la simple mise à l'échelle d'approches monolithiques. Pour la communauté croissante qui travaille à combler les mathématiques informelles et formelles, cette idée pourrait s'avérer aussi précieuse que les benchmarks eux-mêmes.