Résumé technique : Construction–Vérification : Un benchmark pour la formalisation des mathématiques appliquées dans Lean 4

1. Énoncé du problème

Les benchmarks actuels pour la preuve de théorèmes automatisée, tels que MiniF2F et ProofNet, se concentrent principalement sur la vérification logique de propositions déclaratives (c'est-à-dire prouver l'existence d'une solution). Ce paradigme est insuffisant pour les mathématiques appliquées, où l'objectif principal est souvent la dérivation de valeurs concrètes, d'algorithmes exécutables ou de transformations structurelles plutôt que la simple preuve d'existence.

Les jeux de données existants souffrent de deux limitations critiques dans ce domaine :

1. Écart de portée : Ils manquent de couverture des mathématiques appliquées de niveau licence et supérieur, incluant l'analyse convexe, l'optimisation, l'algèbre numérique et les probabilités de haute dimension.
2. Déficit constructif : Ils ne parviennent pas à imposer un flux de travail « construction–vérification ». En mathématiques appliquées, un modèle doit explicitement synthétiser une solution (par exemple, un algorithme ou une valeur spécifique) avant de prouver sa correction. Les benchmarks actuels permettent aux modèles de contourner cela en utilisant des tactiques non constructives (par exemple, prouver l'existence via le théorème de la valeur extrême sans calculer l'optimum spécifique), déreprésentant ainsi la capacité du modèle à effectuer un raisonnement computationnel.

2. Méthodologie

Le cadre Construction–Vérification

Les auteurs proposent un paradigme de formalisation dans Lean 4 qui impose structurellement un flux de travail en deux étapes : la Construction suivie de la Vérification. Ce cadre empêche les agents d'exploiter des raccourcis non constructifs en exigeant des définitions explicites avant les preuves. Le cadre traite trois catégories spécifiques de tâches mathématiques appliquées :

• Problèmes d'évaluation : Au lieu de prouver $\exists x, Q(x)$, l'agent doit définir une fonction def x (V) := ... qui calcule la solution $x(V)$ basée sur des paramètres $V$, suivie d'un théorème prouvant $Q(x(V), V)$. La signature de la fonction restreint strictement les entrées aux paramètres bruts, empêchant le modèle d'utiliser la propriété cible pour « tricher » lors de la construction.
• Problèmes de conception d'algorithmes : L'agent doit définir une fonction récursive représentant un processus itératif (par exemple, la descente de gradient). La tâche consiste à remplir la règle de transition (le corps de la boucle) pour l'étape $(n+1)$, suivie d'une preuve de propriétés telles que la convergence ou la monotonie.
• Transformation de représentation : L'agent doit modéliser une instance de problème brute sous une forme canonique cible (par exemple, transformer un problème de coupe de graphe en une formulation de clustering spectral). Cela implique de définir le nouveau domaine, les contraintes et la fonction objectif, et de prouver une relation de relaxation ou d'équivalence entre le problème source et le problème cible.
• Preuve de théorèmes : Un sous-ensemble de base de tâches de déduction traditionnelles est inclus pour mesurer les capacités de raisonnement logique pur, distinctes de la synthèse constructive.

Curation du Benchmark (AMBER)

Les auteurs introduisent AMBER (Applied Mathematics BEnchmark for Reasoning), un jeu de données couvrant quatre domaines fondamentaux :

1. L'analyse convexe
2. L'optimisation
3. L'algèbre numérique
4. Les probabilités de haute dimension

Sources de données et difficulté : Les problèmes sont tirés de manuels classiques (ex: Boyd & Vandenberghe, Vershynin) et classés par difficulté (Facile : exercices standards ; Difficile : niveau examen de doctorat).
Formalisation et validation : 50 problèmes par sous-domaine ont été formalisés par des utilisateurs expérimentés de Lean. La validation a impliqué un processus en deux étapes : une vérification sémantique basée sur un LLM suivie d'une validation croisée manuelle rigoureuse par des contributeurs de Mathlib afin de garantir un alignement strict avec les énoncés mathématiques originaux.
Métriques de complexité : Le benchmark est caractérisé par une haute densité de dépendance sémantique. En utilisant une analyse de graphe de dépendance ($k=3$), AMBER présente une densité de dépendance moyenne de 164,21, nettement supérieure à MiniF2F (29,72), ProofNet (33,95) et FATE (53,14), indiquant un besoin plus profond de récupération et de raisonnement sur des concepts mathématiques complexes.

3. Contributions clés

1. Changement de paradigme : L'article propose un passage de la vérification de propositions existentielles à la synthèse de solutions constructives, alignant les tâches formelles sur l'intuition computationnelle des mathématiques appliquées.
2. Benchmark AMBER : Un jeu de données complet couvrant les principaux domaines appliqués avec différents niveaux de difficulté, présentant des tâches complexes comme la conception d'algorithmes et la transformation de représentation, et non seulement la preuve de théorèmes.
3. Modèles de formalisation : Des modèles spécialisés en Lean 4 pour l'évaluation, la conception d'algorithmes et la transformation de représentation qui imposent des barrières syntaxiques strictes contre le raisonnement non constructif.
4. Analyse empirique : Une évaluation systématique révélant un compromis fondamental dans les systèmes neuro-symboliques actuels : la tension entre la compétence tactique locale (provers spécialisés) et la synthèse algorithmique de haut niveau (modèles généraux).

4. Résultats expérimentaux

Performance des modèles

Les auteurs ont évalué un ensemble diversifié de modèles, incluant des agents de raisonnement à usage général (DeepSeek-V3.2-Thinking, GPT-5.1, Gemini-3.0 Pro) et des prouveurs de théorèmes spécialisés (Goedel Prover-32B, Kimina Prover-72B).

• Difficulté globale : La performance de tous les modèles est remarquablement basse. Sur le sous-ensemble « Difficile », les taux de réussite sont proches de zéro pour presque tous les modèles.
• Général vs Spécialisé : Contrairement à la tendance des benchmarks de mathématiques pures, les modèles de raisonnement à usage général surpassent systématiquement les prouveurs de théorèmes spécialisés.
  • Pass@16 (AMBER complet) : Les modèles généraux ont atteint 4,50 %–6,00 %, tandis que les prouveurs spécialisés ont atteint 4,00 %.
  • Pass@16 (Sous-ensemble Difficile) : Les modèles généraux ont atteint 0 %–0 % (avec une certaine variation dans les sous-ensembles Faciles), tandis que les prouveurs spécialisés ont également lutté de manière significative.
• Étude d'ablation : La stratégie de prompt de construction-vérification a produit un taux de réussite de 8 % sur un sous-ensemble de 100 problèmes, surpassant la complétion de code standard (6 %) et les prompts traditionnels de preuve seule (5 %). Les prompts de preuve seule ont fréquemment conduit les modèles à utiliser des raccourcis non constructifs (ex: Classical.choice).

Analyse d'erreurs

Une analyse de 3 189 messages d'erreur du modèle DeepSeek-R1 a révélé :

1. Hallucination (47,3 %) : Le mode de défaillance le plus courant, où les modèles invoquent des théorèmes ou des définitions inexistants (ex: convexHull eq sInter).
2. Compétence de formalisation (32,7 %) : Mauvaise application de tactiques valides ou échec de la satisfaction des conditions secondaires.
3. Sorties incomplètes (15,2 %) : Échec de la fourniture de code entièrement exécutable, laissant souvent des espaces réservés sorry dans des étapes inductives complexes.
4. Formatage/Syntaxe (4,8 %) : Erreurs de base de markdown ou de syntaxe.

5. Signification et affirmations

L'article affirme que le paysage actuel de la formalisation automatisée fait face à un phénomène de « surapprentissage tactique » (tactical overfitting). Les modèles spécialisés, largement affinés sur des corpus de preuves, semblent dégrader leurs capacités générales de suivi d'instructions. Ils traitent chaque défi structurel comme une tâche de preuve pure, ignorant souvent les exigences multi-étapes des mathématiques appliquées (ex: définir une fonction avant de la prouver).

En revanche, les modèles à usage général conservent la polyvalence nécessaire pour combler le fossé entre l'intention informelle et la syntaxe formelle, en synthétisant avec succès des objets mathématiques avant d'entrer dans la phase de vérification. Les auteurs concluent que l'avancement des mathématiques appliquées formalisées nécessite d'aller au-delà de la simple recherche de preuve vers des systèmes neuro-symboliques qui intègrent le raisonnement algorithmique de haut niveau avec une vérification formelle rigoureuse. Le benchmark AMBER sert de fondation pour la recherche future visant à étendre les frontières des mathématiques appliquées formalisées en fournissant un standard qui exige la synthèse constructive plutôt que la simple validité logique.