Résumé technique : Raffinement monotone sans référence pour l'autoformalisation

1. Énoncé du problème

Bien que les modèles de langage à grande échelle (LLM) aient fait progresser le raisonnement mathématique, l'autoformalisation complète de théorèmes—la conversion de théorèmes en langage naturel et de leurs preuves associées en énoncés et preuves formels complets et mécaniquement vérifiables—reste sous-explorée. Les approches existantes se concentrent souvent uniquement sur la formalisation de l'énoncé, en s'appuyant sur des espaces réservés « sorry » pour les preuves, ou traitent la génération d'énoncés et la preuve de théorèmes comme des tâches isolées.

Le défi central réside dans la nature multidimensionnelle d'une autoformalisation de haute qualité. Une formalisation réussie doit simultanément satisfaire :

1. Validité formelle (VF) : Correction syntaxique et vérification mécanique par un prouveur de théorèmes (par exemple, Lean4).
2. Préservation logique (PL) : Alignement sémantique avec la structure logique de l'énoncé en langage naturel original.
3. Cohérence mathématique (CM) : Représentation précise des objets et opérations mathématiques.
4. Qualité formelle (QF) : Clarté structurelle, concision et réutilisabilité.

Les méthodes actuelles de raffinement itératif peinent à optimiser conjointement ces dimensions, améliorant souvent un aspect (par exemple, la syntaxe) au détriment d'autres (par exemple, l'alignement sémantique). De plus, les méthodes existantes reposent souvent sur des formalisations de vérité terrain ou une intervention humaine pour la sélection, limitant ainsi leur applicabilité dans des contextes sans référence.

2. Méthodologie

Les auteurs proposent un processus d'optimisation itératif, monotone et sans référence qui opère au moment du test sans accès à des formalisations de vérité terrain ni à une sélection humaine. Le cadre intègre les retours des prouveurs de théorèmes et de juges basés sur des LLM pour guider un ensemble de LLM spécialisés.

2.1 Fonction objectif

Les auteurs définissent une fonction objectif composite masquée $J_{OA}(x)$ pour équilibrer les quatre dimensions. La Validité formelle ($\pi_{FV}$) agit comme une contrainte dure (un masque), tandis que la Préservation logique ($\pi_{LP}$), la Cohérence mathématique ($\pi_{MC}$) et la Qualité formelle ($\pi_{FQ}$) sont traitées comme des dimensions souples :
$$J_{OA}(x) = \frac{1}{3}\pi_{FV}(x) \left( \pi_{LP}(x) + \pi_{MC}(x) + \pi_{FQ}(x) \right)$$
Cette formulation garantit que les formalisations invalides (où $\pi_{FV}=0$) ne sont pas sélectionnées, indépendamment de leurs scores souples.

2.2 Juges LLM et incertitude

Puisque les dimensions souples sont intraitables à calculer exactement, le cadre emploie des juges LLM pour estimer les scores. Pour gérer le bruit et les biais inhérents aux LLM, les auteurs supposent :

• Stabilité asymptotique : Les jugements se stabilisent après calibration.
• Incertitude mesurable : Une borne inférieure de confiance (LCB) unilatérale peut être établie pour les vrais scores.
  L'objectif est optimisé à l'aide d'un estimateur basé sur la LCB, garantissant que les décisions de sélection soient conservatrices et robustes face au bruit d'évaluation.

2.3 Rôles des générateurs et réactivité

Le cadre décompose les rôles des LLM en trois catégories, guidées par une carte de réactivité qui modélise les améliorations attendues par dimension :

1. Générateurs ponctuels (OOG) : Génèrent des formalisations initiales à partir de zéro (par exemple, des modèles mathématiques spécialisés comme DeepSeek-Prover).
2. Réparateurs VF (FVR) : Ciblent et corrigent spécifiquement les candidats formellement invalides (par exemple, des modèles capables de révision itérative de preuves).
3. Générateurs récurrents (REG) : Affinent le meilleur candidat actuel en fonction des retours des juges LLM concernant des dimensions souples spécifiques (PL, CM ou QF).

2.4 Politique d'acceptation monotone

Le processus itère sur la génération et la sélection de candidats. Une Politique d'acceptation conservatrice est appliquée : un nouveau candidat n'est accepté que si son score objectif estimé (basé sur la LCB) est strictement supérieur au meilleur actuel. Cela garantit une amélioration monotone certifiée, signifiant que la qualité de la formalisation sélectionnée ne diminue jamais au cours des itérations. Il est démontré que le processus converge et se termine sous des conditions spécifiques.

3. Contributions clés

1. Définition formelle et cadre : L'article est le premier à définir formellement l'autoformalisation complète de théorèmes comme une tâche unifiée et à proposer un processus itératif monotone sans référence pour la résoudre.
2. Fonction objectif composite masquée : Introduction d'une fonction objectif qui impose la Validité formelle comme contrainte dure tout en optimisant simultanément plusieurs dimensions souples (PL, CM, QF).
3. Ensemble spécialisé par rôle : Décomposition de la tâche d'autoformalisation en rôles OOG, FVR et REG, utilisant une carte de réactivité pour sélectionner les générateurs les plus efficaces pour des dimensions de qualité spécifiques.
4. Garanties théoriques : Apport de preuves théoriques pour la monotonie certifiée, la convergence et la terminabilité du processus, assurant un progrès non décroissant même en présence de bruit réaliste des juges.
5. Validation empirique : Démonstration que le cadre assemble efficacement les forces des LLM spécialisés et généralistes pour obtenir des résultats de haute qualité sur des benchmarks standards.

4. Résultats expérimentaux

La méthode a été évaluée sur miniF2F-Test et ProofNet-Test en utilisant Lean4. Le cadre a employé un ensemble de modèles incluant DeepSeek-Prover-V2-7B, Goedel-Prover-V2-8B, Seed-Coder-8B, Qwen2.5-7B et GPT-4.1-mini (en tant que juges).

Indicateurs de performance clés :

• miniF2F : A atteint 100,00 % de Validité formelle et un score global de 90,27 %. Le taux de formalisations « parfaites » (toutes les dimensions notées 1) a atteint 49,18 %.
• ProofNet : A atteint 77,96 % de Validité formelle et un score global de 52,45 %, avec 17,74 % de formalisations parfaites.

Constats comparatifs :

• Monotone vs. Baselines : Le processus monotone a nettement surpassé à la fois le Best-of-k (échantillonnage de $k$ sorties) et l'Auto-raffinement itératif (ISR) sans politiques d'acceptation.
• Ensemble vs. Modèle unique : Bien qu'un modèle unique puissant (GPT-5.4) ait montré une amélioration, l'ensemble de modèles plus petits et spécialisés assignés à des rôles spécifiques a atteint des performances supérieures, en particulier en matière de Validité formelle.
• Robustesse : La tendance monotone a persisté même lors de l'évaluation par différentes familles de juges LLM (par exemple, Qwen vs. GPT) et par des experts humains, indiquant que les améliorations ne sont pas des artefacts de biais des juges.

5. Signification et revendications

L'article revendique que ce travail offre une étape pratique et théoriquement fondée vers une autoformalisation fiable. En opérant de manière sans référence, l'approche est applicable même dans des domaines dépourvus de bibliothèques formelles étendues, pouvant potentiellement aider à la formalisation de domaines sous-explorés des mathématiques et des sciences.

Les auteurs soulignent que le cadre fournit une méthodologie rigoureuse pour l'autoformalisation assistée par l'IA qui :

• Réduit le besoin de supervision humaine dans les pipelines de vérification formelle à grande échelle.
• Quantifie et contrôle explicitement l'incertitude dans le jugement grâce aux hypothèses LCB.
• Démontre que la combinaison de LLM complémentaires avec les retours des vérificateurs formels peut produire des formalisations d'une qualité prouvée non décroissante.

L'ouvrage conclut que, bien que les coûts computationnels soient plus élevés que l'inférence en un seul passage, le compromis est justifié par les gains significatifs en performance et en stabilité, ouvrant la voie à de futures recherches sur un raisonnement formel assisté par l'IA sûr et fiable.