💬 NLP

OProver: A Unified Framework for Agentic Formal Theorem Proving

OProver est un cadre unifié pour la preuve formelle de théorèmes par agents en Lean 4 qui intègre la révision itérative des preuves avec les retours du compilateur et la récupération, atteignant des performances de pointe sur plusieurs benchmarks grâce à une nouvelle pipeline d'entraînement combinant un pré-entraînement continu, un ajustement fin supervisé sur des trajectoires de réparation et un apprentissage par renforcement sur des cas difficiles.

Auteurs originaux : David Ma, Kaijing Ma, Shawn Guo, Yunfeng Shi, Enduo Zhao, Jiajun Shi, Zhaoxiang Zhang, Gavin Cheung, Jiaheng Liu, Zili Wang

Publié 2026-05-19

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : David Ma, Kaijing Ma, Shawn Guo, Yunfeng Shi, Enduo Zhao, Jiajun Shi, Zhaoxiang Zhang, Gavin Cheung, Jiaheng Liu, Zili Wang

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez de résoudre un casse-tête mathématique très difficile, mais que vous devez écrire la solution dans un langage strict et robotique appelé Lean 4. Si vous faites même une seule faute de frappe ou une erreur logique, l'ordinateur (le « compilateur ») rejette tout et dit : « Non, c'est faux. »

Pendant longtemps, les modèles d'IA tentant de résoudre ces casse-têtes fonctionnaient comme un élève passant un examen : ils devinaient une réponse, et si elle était fausse, ils repartaient de zéro pour deviner à nouveau. Ils ne comprenaient pas vraiment pourquoi ils avaient tort, et ils n'utilisaient pas les retours spécifiques de l'ordinateur pour corriger leurs erreurs.

OProver est un nouveau système qui change la donne. Au lieu de simplement deviner, il agit comme un détective perfectionniste qui ne renonce jamais. Voici comment il fonctionne, en utilisant des analogies simples :

1. Le détective « Agent » (Le Preuveur)

Imaginez OProver non pas comme un manuel statique, mais comme un détective qui suit un processus d'enquête en plusieurs étapes.

L'ancienne méthode : Le détective rédige une théorie, le juge (l'ordinateur) dit « Faux », et le détective rédige une toute nouvelle théorie à partir de zéro.
La méthode OProver : Le détective rédige une théorie. Le juge dit : « Vous avez fait une erreur ici : vous avez utilisé le mauvais type de nombre. » Le détective édite alors cette partie spécifique de la théorie, la vérifie à nouveau, et continue de l'affiner jusqu'à ce que le juge dise : « Correct ! »

OProver est entraîné à effectuer automatiquement cette danse de « modification et d'affinement ». Il ne se contente pas de deviner ; il apprend à écouter les plaintes spécifiques du juge et à les corriger.

2. La « Bibliothèque de solutions » (Récupération)

Avant que le détective ne commence à écrire, il ne travaille pas dans le vide. Il se rend dans une immense bibliothèque (appelée Mémoire de récupération).

Si le détective tente de résoudre un casse-tête sur les triangles, la bibliothèque extrait instantanément les 5 meilleures preuves sur les triangles que d'autres détectives ont résolues avec succès auparavant.
OProver lit ces « mémos » pour voir comment d'autres personnes ont résolu des problèmes similaires, en utilisant leurs stratégies comme guide. Cela aide le détective à éviter les pièges courants.

3. La « Boucle d'amélioration autonome » (L'entraînement)

C'est la partie la plus magique. Habituellement, les modèles d'IA sont entraînés sur un ensemble de données fixe, puis laissés tranquilles. OProver est différent ; il possède un cycle d'amélioration autonome.

Étape 1 : OProver tente de résoudre un tas de casse-têtes.
Étape 2 : Lorsqu'il réussit, il enregistre cette solution dans la bibliothèque afin qu'elle puisse servir de « mémo » pour les problèmes futurs.
Étape 3 : Lorsqu'il échoue, il enregistre l'histoire complète de son échec, ce que l'ordinateur a dit, et comment il l'a finalement corrigé.
Étape 4 : Le système utilise ces « histoires d'échec » pour s'enseigner à lui-même comment mieux faire la prochaine fois.

C'est comme un élève qui, après chaque examen, ne se contente pas de mémoriser les bonnes réponses, mais écrit aussi exactement pourquoi il a eu tort sur certaines questions et ajoute ces notes à son guide d'étude. Avec le temps, l'élève devient plus intelligent, et son guide d'étude s'épaissit et devient plus utile.

4. Le résultat : Un super-élève

L'article a testé ce système sur cinq « olympiades de mathématiques » différentes (allant du niveau lycée à des compétitions universitaires très difficiles).

La réalisation : OProver (spécifiquement la version à 32 milliards de paramètres) est devenu le meilleur performer parmi tous les prouveurs d'IA open source. Il a résolu plus de problèmes correctement que tout autre système similaire, battant même des modèles beaucoup plus grands.
Pourquoi c'est important : Cela a prouvé que donner à l'IA la capacité de écouter les retours, de consulter les solutions passées et de corriger itérativement son propre travail est bien plus puissant que de simplement la rendre plus grande ou plus douée pour deviner.

En résumé

OProver est une IA de résolution de problèmes mathématiques qui ne se contente pas de « deviner et vérifier ». C'est un apprenant collaboratif qui :

Consulte d'abord des problèmes résolus similaires.
Rédige une preuve.
Écoute les messages d'erreur spécifiques de l'ordinateur.
Édite son travail pour corriger ces erreurs.
Répète jusqu'à ce qu'il réussisse, puis enregistre la leçon pour la prochaine fois.

En transformant l'« échec » en opportunité d'apprentissage et en maintenant un journal continu de ce qui fonctionne, OProver est devenu la meilleure IA open source pour prouver formellement des théorèmes mathématiques aujourd'hui.

Résumé Technique : OProver : Un Cadre Unifié pour la Preuve de Théorèmes Formels Agente

Énoncé du Problème

Les récentes avancées dans la preuve de théorèmes formels, en particulier au sein de l'écosystème Lean 4, ont exploité la génération de preuves à grande échelle et un entraînement conscient du vérificateur pour améliorer les performances sur des références telles que MiniF2F et PutnamBench. Cependant, une limitation critique persiste : les capacités de preuve agente (récupération, retour du compilateur et réparation itérative) sont généralement traitées comme des heuristiques appliquées au moment de l'inférence à un prouveur fixe, plutôt que comme des politiques apprises intégrées au processus d'entraînement.

Cela crée un décalage entraînement-inférence. Les modèles entraînés principalement sur des preuves finalisées et réussies ne rencontrent le retour du compilateur et le contexte récupéré qu'au moment du déploiement, dans des distributions pour lesquelles ils n'ont jamais été optimisés. De plus, les corpus formels existants se concentrent sur les produits finaux (énoncés et preuves vérifiées), omettant les historiques d'interaction multi-tours — tentatives échouées, contexte récupéré et diagnostics du compilateur — essentiels pour apprendre à réparer les preuves. Par conséquent, le signal de supervision guidant la réparation des preuves dans la pratique reste largement inexploité dans l'entraînement des modèles.

Méthodologie

L'article présente OProver, un cadre unifié qui intègre la récupération, le retour du compilateur et la réparation itérative directement dans la politique du prouveur grâce à un pipeline d'entraînement co-évolutif.

1. Le Cadre OProver

OProver traite la preuve de théorèmes comme une boucle de raffinement bornée et multi-tours. À chaque tour $t$ , la politique $\pi$ se conditionne sur un état compact $X_t = (s, R_t, p_{t-1}, f_{t-1})$ , où :

$s$ : L'énoncé du théorème cible.
$R_t$ : Les $k$ meilleures preuves récupérées et vérifiées par le compilateur issues d'une mémoire $M$ .
$p_{t-1}$ : La tentative de preuve précédente.
$f_{t-1}$ : Le retour brut textuel du compilateur (diagnostics) du vérificateur Lean 4.

La politique génère une tentative révisée $p_t$ . Si la vérification échoue, le retour brut est renvoyé à la politique pour le tour suivant. Crucialement, la politique se conditionne uniquement sur la tentative la plus récente et le retour correspondant, préservant ainsi les signaux de correction locaux tout en maintenant l'état compact.

2. OProofs : Un Corpus d'Entraînement Unifié

Pour soutenir ce cadre, les auteurs construisent OProofs, un corpus à grande échelle spécifiquement conçu pour la preuve agente. Contrairement aux jeux de données antérieurs qui ne conservent que les preuves finales, OProofs enregistre des trajectoires sérialisées incluant :

Le contexte récupéré.
Les tentatives échouées.
Le retour brut du compilateur.
Les réparations subséquentes.

OProofs est construit à partir de trois sources : des ressources Lean publiques, une synthèse de preuves à grande échelle (autoformalisation + vérification) et des traces issues de la preuve agente par OProver lui-même. Il contient 1,77 million d'énoncés Lean uniques et 6,86 millions de preuves vérifiées par le compilateur, appariés à 1,07 million de trajectoires agentes.

3. Pipeline d'Entraînement Co-Évolutif

Le processus d'entraînement suit une boucle itérative (Algorithme 1) où le prouveur et le corpus co-évoluent :

Pré-entraînement Continu (CPT) : Un modèle de base est entraîné sur un mélange de code Lean, de mathématiques et de données de raisonnement à contexte long pour créer OProver-Base.
Post-entraînement Itératif :
- Déploiements Agentes : La politique actuelle effectue une preuve multi-tours sur un pool de théorèmes, en récupérant depuis la mémoire courante $M_k$ et en vérifiant avec le compilateur Lean.
- Collecte de Données : Les nouvelles preuves vérifiées sont ajoutées au corpus et indexées dans la mémoire de récupération. Les tentatives échouées et les réparations réussies sont décomposées en exemples au niveau du tour $(s, R_t, p_{t-1}, f_{t-1}) \to p_t$ .
- Affinement Supervisé (SFT) : Le modèle est mis à jour en utilisant les exemples de réparation collectés.
- Apprentissage par Renforcement (RL) : L'optimisation de politique de séquence par groupes (GSPO) est appliquée aux cas non résolus plus difficiles, en utilisant un signal de récompense basé sur le succès de la vérification et la correction du format.
- Recirculation : Le corpus et la mémoire mis à jour alimentent la prochaine itération, permettant à la politique d'apprendre de ses propres preuves améliorées.

Contributions Clés

Cadre Unifié pour la Preuve Agente : OProver unifie la récupération, le retour et la réparation itérative en une seule politique apprise, éliminant le décalage entraînement-inférence en entraînant le modèle à utiliser ces signaux comme partie intégrante de sa stratégie de base plutôt que comme des heuristiques externes.
Corpus OProofs : La construction d'un corpus à grande échelle (1,77 million d'énoncés, 6,86 millions de preuves) qui préserve explicitement les historiques d'interaction multi-tours, incluant les tentatives échouées et le retour brut du compilateur, offrant une supervision précédemment indisponible dans les jeux de données formels.
Pipeline Co-Évolutif : Une méthodologie d'entraînement où le prouveur génère de nouvelles données (preuves vérifiées et trajectoires de réparation) qui sont immédiatement réintégrées dans le corpus d'entraînement et la mémoire de récupération, créant une boucle d'auto-amélioration.
Performances de l'État de l'Art : OProver obtient des résultats de premier plan parmi les prouveurs de preuves complètes à poids ouverts, démontrant que les stratégies de raffinement agente peuvent surpasser des modèles significativement plus grands.

Résultats Expérimentaux

OProver a été évalué sur cinq références Lean 4 : MiniF2F, MathOlympiadBench, ProofNet, ProverBench et PutnamBench.

Performance : Le modèle OProver-32B a obtenu les meilleurs scores Pass@32 sur trois références (MiniF2F : 93,3 %, ProverBench : 58,2 %, PutnamBench : 11,3 %) et le deuxième meilleur sur les deux autres (MathOlympiad : 22,8 %, ProofNet : 33,2 %).
Efficacité : OProver-32B (32 milliards de paramètres) a surpassé DeepSeek-Prover-V2 (671 milliards) et LongCat-Flash-Prover (560 milliards avec TIR) sur la plupart des références, malgré un nombre de paramètres nettement inférieur. Même la variante 8B a surpassé Goedel-Prover-V2 (32 milliards) sur toutes les références.
Mise à l'Échelle au Moment du Test : Les performances se sont améliorées de manière constante avec l'augmentation des budgets de calcul (plus d'échantillons ou de tours de raffinement), bien qu'avec des rendements décroissants. L'allocation optimale entre la profondeur de raffinement et la largeur d'échantillonnage variait selon la difficulté de la référence.
Études d'Ablation : La suppression du retour du compilateur multi-tours a causé la dégradation de performance la plus significative, confirmant le raffinement itératif comme le principal moteur des gains. La suppression de l'augmentation par récupération a également causé des baisses constantes, bien que plus faibles, soulignant la valeur complémentaire de l'ancrage par récupération.

Signification et Revendications

L'article revendique qu'OProver démontre que la preuve de théorèmes formels agente peut être efficacement apprise comme une politique unifiée plutôt que comme un assemblage de modules séparés au moment de l'inférence. En s'entraînant sur la trajectoire complète de la construction de la preuve, de l'échec et de la réparation, le modèle apprend à exploiter le retour du compilateur et le contexte récupéré comme des parties intrinsèques de son processus de raisonnement.

Les auteurs soulignent que les gains de performance ne résultent pas simplement de l'échelle du modèle, mais découlent de la synergie entre l'ancrage par récupération augmentée et le raffinement itératif guidé par le compilateur. La co-évolution de la politique OProver et du corpus OProofs permet au système d'améliorer continuellement ses capacités de preuve en apprenant de ses propres tentatives réussies et échouées, établissant ainsi un nouveau paradigme pour l'entraînement des systèmes de raisonnement formel.