Résumé Technique : FormalRewardBench

Énoncé du Problème

Les avancées récentes dans les prouveurs de théorèmes neuronaux reposent fortement sur l'apprentissage par renforcement avec des récompenses vérifiables (RLVR). Dans ce paradigme, les assistants de preuve (tels que Lean 4) fournissent des signaux binaires de correction (succès/échec) basés sur la vérification de types. Bien que ces signaux soient évolutifs et immunisés contre le piratage des récompenses, ils souffrent d'une attribution de crédit sparse : les modèles ne reçoivent aucun signal d'apprentissage pour les progrès partiels sur des problèmes difficiles, car une preuve qui échoue à la dernière étape reçoit la même récompense nulle qu'une approche totalement incorrecte.

Pour atténuer ce problème, les chercheurs ont proposé des modèles de récompense appris capables d'évaluer la qualité des preuves au-delà de la vérification binaire. Cependant, la comparaison de ces modèles de récompense est actuellement difficile car elle nécessite généralement des ablations coûteuses d'apprentissage par renforcement (RL). De plus, les benchmarks existants pour les modèles de récompense (par exemple, RewardBench, ProcessBench) se concentrent sur le raisonnement en langage naturel informel et ne traitent pas de la précision syntaxique, de la correction des types et de la validité logique requises pour la preuve de théorèmes formels. Il n'existe actuellement aucun benchmark pour évaluer directement les modèles de récompense sur des preuves formelles sans exécuter d'entraînements.

Méthodologie

Les auteurs introduisent FormalRewardBench, le premier benchmark conçu pour évaluer les modèles de récompense pour la preuve de théorèmes formels en Lean 4. Le benchmark se compose de 250 paires de préférences, où chaque paire contient une preuve correcte vérifiée formellement et une variante incorrecte.

Construction du Jeu de Données

Le jeu de données est dérivé de MiniF2F, une collection de 488 problèmes mathématiques de niveau olympique formalisés en Lean 4. Les auteurs emploient un pipeline contrôlé d'injection d'erreurs pour générer des preuves incorrectes satisfaisant trois critères :

1. Validité Syntaxique : La preuve incorrecte doit être analysée comme du code Lean valide.
2. Plausibilité Sémantique : Les erreurs ne doivent pas être triviales (par exemple, des variables non définies) mais refléter plutôt des modes de défaillance réalistes.
3. Modèles d'Erreurs Réalistes : Les erreurs doivent imiter les échecs réels des grands modèles de langage (LLM).

Stratégies d'Injection d'Erreurs

Cinq stratégies curatées par des experts sont utilisées pour générer des variantes incorrectes, mises en œuvre via des invites adressées à un LLM de pointe (Claude Opus 4.5) :

1. Variations Minimales à Point Unique : Modifications chirurgicales de preuves correctes (par exemple, échanger des hypothèses, modifier un seul nom de variable ou de lemme) qui provoquent un échec sémantique tout en maintenant la validité syntaxique.
2. Justification en Langage Naturel : Ajout de commentaires en langage naturel trompeurs justifiant le raisonnement défectueux dans les preuves incorrectes, testant le « biais de verbosité ».
3. Injection de Code Python : Remplacement des étapes de preuve formelle Lean par du code Python exécutable qui peut résoudre le problème de manière computationnelle mais échoue à satisfaire l'exigence d'une preuve formelle (test de l'adhésion à la tâche).
4. Erreurs LLM Forcées : Génération de preuves contenant des erreurs formelles courantes identifiées dans les sorties précédentes des modèles, telles qu'une application incorrecte de tactiques, une sélection d'hypothèses erronée ou une instanciation incorrecte de lemme.
5. Preuves Incorrectes Verbeuses : Génération de preuves inutilement longues avec des structures sophistiquées et des lemmes intermédiaires qui masquent des défauts logiques fondamentaux.

Protocole d'Évaluation

Le benchmark évalue les modèles dans deux configurations :

• Point par Point : Le modèle attribue un score à chaque preuve indépendamment ; la précision est mesurée si le score de la preuve correcte dépasse celui de la preuve incorrecte.
• Par Paires : Le modèle compare deux preuves et émet une préférence. Pour atténuer le biais de position, la précision n'est comptabilisée que si le modèle identifie de manière cohérente la preuve correcte dans les deux ordres (correct en premier et correct en second).

Résultats Clés

Les auteurs ont évalué quatre catégories de modèles : LLMs de pointe, LLMs Juges, LLMs à usage général et Modèles Spécialisés en Preuve de Théorèmes.

1. Hiérarchie des Performances : Les LLMs de pointe (par exemple, Claude Opus 4.5) ont obtenu les meilleures performances (59,8 % de précision par paires). Les LLMs Juges (entraînés sur des données de préférence) ont largement surpassé les prouveurs de théorèmes spécialisés parmi les modèles à poids ouverts (52,8 % contre 12,8 % pour certains modèles spécialisés).
2. Le Fossé Génération-Évaluation : Les modèles spécialisés en preuve de théorèmes (par exemple, DeepSeek-Prover-V2-7B, Gödel-Prover-V2-8B) ont obtenu les pires résultats (variant de 0,0 % à 24,4 %). Malgré l'atteinte de métriques pass@k de pointe sur MiniF2F, ces modèles peinent à évaluer les preuves. Les auteurs attribuent cela à un manque d'entraînement sur la détection d'erreurs ; ces modèles sont optimisés pour générer des preuves correctes via SFT et RLVR mais n'ont pas appris à identifier ou critiquer les erreurs.
3. Gradient de Difficulté des Erreurs :
   • Plus Facile : Injection de Code Python (S3), où la détection repose sur l'identification du langage plutôt que sur la compréhension de la preuve.
   • Plus Difficile : Preuves Incorrectes Verbeuses (S5) et Erreurs Forcées (S4). Même les meilleurs modèles n'ont atteint que ~60 % sur S5 et ~50 % sur S4.
   • Limites des Modèles Juges : Les modèles Juges ont montré un motif bimodal : une performance quasi parfaite sur l'injection Python mais s'effondrant à presque zéro sur les preuves verbeuses, suggérant que leur entraînement par préférence développe une discrimination de surface plutôt qu'un raisonnement formel profond.
4. Biais de Position : Un biais de position significatif a été observé dans toutes les catégories, en particulier chez les prouveurs spécialisés (par exemple, DeepSeek-Prover-V2-7B a préféré la première preuve 94,9 % du temps, indépendamment de la correction).

Importance et Revendications

L'article revendique trois contributions principales :

1. FormalRewardBench : Un nouveau benchmark permettant la comparaison directe des modèles de récompense pour la preuve de théorèmes formels sans nécessiter d'ablations coûteuses d'entraînement par RL.
2. Méthodologie : Un ensemble réutilisable de cinq stratégies d'injection d'erreurs pour générer des preuves formelles incorrectes réalistes, applicable à d'autres assistants de preuve, à l'augmentation de données ou à la conception de curriculums.
3. Insight Empirique : La découverte que les capacités générales de modélisation des récompenses (trouvées dans les modèles de pointe et les modèles Juges) se transfèrent plus efficacement à l'évaluation des preuves que l'entraînement spécifique au domaine en preuve de théorèmes.

Les auteurs soulignent que, bien que le développement de modèles de récompense efficaces puisse accélérer la découverte et la vérification mathématiques, les modèles actuels présentent des limitations significatives. Ils mettent en évidence que la vérification formelle reste l'arbitre ultime de la correction, car des modèles de récompense imparfaits comportent des risques de sur-reliance. Le benchmark est publié publiquement pour encourager de nouvelles recherches sur les modèles de récompense pour les mathématiques formelles.

L'article conclut en notant des limites, notamment la dépendance à la vérification automatique pour la plupart des exemples, le focus exclusif sur Lean 4, et l'exclusion d'une évaluation au niveau du processus ou étape par étape. Des travaux futurs sont suggérés pour se concentrer sur des approches hybrides combinant des modèles de récompense appris avec la vérification formelle et pour étendre le benchmark à d'autres assistants de preuve comme Coq et Isabelle.