Résumé technique : Lean-as-Judge contrôlé par le risque pour le raisonnement mathématique en langage naturel

1. Énoncé du problème

L'article aborde le défi consistant à utiliser des assistants de preuve formels (spécifiquement Lean) comme juges pour le raisonnement mathématique en langage naturel généré par des modèles de langage de grande taille (LLM). Bien qu'une preuve Lean réussie constitue une forte preuve positive en faveur d'une affirmation formelle, l'absence de preuve est un signal ambigu. Une preuve échouée peut indiquer une réponse mathématiquement incorrecte, mais elle peut tout aussi bien résulter d'une formalisation mal typée, de faits de bibliothèque manquants ou de dépassements de temps de recherche de preuve.

Les approches actuelles traitent souvent l'échec de la preuve comme un signal de non-validité, risquant de confondre l'incorrectitude mathématique avec un manque de couverture formelle. Les auteurs identifient une « falaise de couverture » : la fiabilité de la sélection formelle dépend fortement de la proportion de réponses candidates pouvant être correctement formalisées et prouvées. Lorsque la couverture est élevée, la sélection formelle est très précise ; lorsque la couverture est faible, le signal devient peu fiable.

Le problème central consiste à déterminer quand un système en aval doit faire confiance à un signal formel Lean et quand il doit traiter ce signal comme hors de couverture (c'est-à-dire non résolu) plutôt que comme incorrect, tout en fournissant une garantie de risque à échantillon fini pour les réponses acceptées.

2. Méthodologie : COVCAL

Les auteurs proposent COVCAL (Coverage-Calibrated Lean), un wrapper sélectif contrôlé par le risque qui décide d'accepter une réponse formelle ou de s'abstenir sur la base de diagnostics de couverture.

2.1 Cadre d'observation partielle

Le système traite le pipeline formel comme un mécanisme d'observation partielle. Il n'observe pas la vérité de chaque réponse candidate, mais observe uniquement :

1. Quelles classes de réponses normalisées atteignent une affirmation Lean bien formée (Couverture typée).
2. Parmi ces classes, lesquelles sont prouvées avec succès (Couverture prouvée).
3. Le poids de la classe prouvée la plus lourde par rapport au rival non résolu le plus lourd (Marge formelle).

Une classe de réponse est définie comme un groupe de chaînes candidates désignant la même réponse finale (par exemple, $1/2$, $0.5$, $2/4$). Les classes qui ne sont pas formalisées ou non prouvées sont considérées comme non résolues, et non automatiquement fausses.

2.2 Diagnostics de couverture

COVCAL calcule quatre métriques clés pour un problème donné $x$ :

• Couverture typée ($C_{typ}$) : Le poids total des classes candidates ayant atteint une affirmation Lean bien formée (statut : proved, typechecked ou timeout).
• Couverture prouvée ($C_{prf}$) : Le poids total des classes candidates ayant reçu une preuve vérifiée par le noyau.
• Masse de rival non résolu ($R_{unres}$) : Le poids de la classe de réponse la plus lourde qui n'a pas été prouvée.
• Marge formelle ($M$) : La différence entre le poids de la classe prouvée la plus lourde et la masse du rival non résolu.

2.3 Sélection et certification

COVCAL n'accepte la classe prouvée la plus lourde que si une règle pré-déclarée basée sur des seuils $(\tau_{typ}, \tau_{prf}, \tau_M)$ est satisfaite. Si la règle n'est pas remplie, le système s'abstient (ou recourt à une méthode non formelle comme la cohérence de soi).

Pour garantir la fiabilité, COVCAL emploie une certification de risque sélectif à échantillon fini. Il garantit que, avec une probabilité $1-\delta$, le risque sélectif (taux d'erreur) des réponses acceptées est au plus $\epsilon$. Deux régimes de certification sont proposés :

1. Régime de Bonferroni : Recherche sur une grille de seuils sur un ensemble de calibration et application d'une correction de borne d'union ($\delta/|T|$) pour tenir compte des comparaisons multiples. Cette approche est conservative et nécessite une forte densité de signal pour être réalisable.
2. Régime Dev-then-Cal : Sélection du seuil sur un ensemble de développement indépendant et certification unique sur l'ensemble de calibration en utilisant une seule borne de Clopper-Pearson ($\delta$). Cette approche est plus efficace en échantillons mais nécessite une séparation stricte entre les données de développement et de calibration.

2.4 Limites théoriques

L'article démontre que sans diagnostics de couverture (c'est-à-dire en se fiant uniquement à l'existence d'une preuve), aucune certification de validité ponctuelle non vacante ne peut être dérivée si une classe rivale non résolue et non équivalente existe. L'absence de preuve formelle n'est pas une preuve de fausseté mathématique ; c'est une preuve d'un statut non résolu.

3. Contributions clés

1. Caractérisation de la falaise de couverture : Sur le jeu de données MATH-500, les auteurs démontrent que la réponse « gagnante en preuve » est correcte dans 96 % des cas à haute couverture prouvée, mais seulement dans 20 % des cas à faible couverture. Cela établit que les preuves Lean ne sont fiables que lorsque la couverture et la marge sont élevées.
2. Sparsité et fidélité du signal : Le signal formel est épars et imparfait. Un auto-formalisateur de 7B prouve une classe pour seulement 28 % des problèmes. De plus, un audit manuel révèle que seulement $\approx 43\%$ de ces preuves sont fidèles au problème original (le reste étant des identités triviales ou des affirmations vraies mais sans pertinence).
3. Méthode COVCAL : Un cadre de prédiction sélective qui certifie le risque sous observation partielle. Il gère explicitement l'asymétrie de l'échec de la preuve et fournit des garanties à échantillon fini pour les prédictions acceptées.
4. Faisabilité dépendante de l'auto-formalisateur : L'article démontre que la faisabilité de la certification est régie par la couverture de l'auto-formalisation. Un formalisateur de 7B génère un signal trop épars pour le régime conservateur de Bonferroni (rejetant toutes les 20 partitions bootstrap), tandis qu'un formalisateur spécialisé en preuve (Goedel-Prover-V2-8B) atteignant 79 % de couverture rend la méthode réalisable sur 17/20 partitions.

4. Résultats expérimentaux

Les expériences ont été menées sur un sous-ensemble filtré de MATH-500 (378 exemples) utilisant Qwen2.5-Math-7B pour la génération et divers formalisateurs pour l'auto-formalisation.

• Performance de référence : La cohérence de soi seule atteint 91 % de précision sans abstention.
• Performance de COVCAL :
  • Sous le régime de Bonferroni avec un formalisateur de 7B, la méthode rejette toutes les entrées (0/20 partitions) car le signal est trop épars pour satisfaire la stricte borne d'union.
  • Sous le régime dev-then-cal avec le formalisateur de 7B, 12/20 partitions sont certifiées. La fraction acceptée est d'environ 21 %, avec une précision acceptée de 0,93.
  • Avec le Goedel-Prover-V2-8B (formalisateur spécialisé), la couverture prouvée passe à 79 %. Le régime de Bonferroni devient réalisable sur 17/20 partitions, acceptant environ 48 % des problèmes avec une précision acceptée de 0,98.
• Audit de fidélité : Un audit manuel de 45 exemples stratifiés a montré que, bien que 73,6 % des affirmations prouvées soient non triviales et correctes, seulement 43 % étaient fidèles à l'énoncé du problème. De nombreuses affirmations « prouvées » étaient des faits secondaires vrais ou des identités triviales qui ne capturaient pas les contraintes du problème.

5. Importance et affirmations

L'article affirme que sa contribution principale est un compte rendu précis du moment et du formalisateur avec lesquels un signal formel partiel peut être fait confiance sous contrôle de risque, plutôt qu'une simple amélioration de la précision brute.

• Contrôle du risque sur la précision brute : Puisque la cohérence de soi est déjà précise à 91 %, la valeur de COVCAL réside dans sa capacité à fournir une certification pour le sous-ensemble de réponses qu'il accepte, distinguant entre « vérifié » et « non résolu » plutôt que « correct » et « incorrect ».
• Gestion des observations partielles : Ce travail reformule la vérification formelle comme un problème de prédiction sélective où les preuves manquantes sont traitées comme des candidats non résolus, empêchant l'étiquetage erroné d'un raisonnement correct comme incorrect en raison d'échecs de formalisation.
• Dépendance à la spécialisation : Les résultats soulignent que l'échelle brute du modèle ne remplace pas la spécialisation. Un formalisateur spécialisé en preuve surpasse nettement un modèle généraliste plus grand en termes de couverture de preuve, qui est la contrainte limitante pour un contrôle de risque certifiable.

Les auteurs concluent que COVCAL sert d'interface conservative pour utiliser Lean comme juge : il n'est réalisable et informatif que lorsque l'auto-formalisateur couvre suffisamment de masse de réponse pour soutenir une certification de risque, mais il ne garantit pas que toutes les réponses sont vérifiées.