Résumé technique : Juger ce que nous ne pouvons pas résoudre

Énoncé du problème

Les progrès récents des grands modèles de langage (LLM) ont démontré leur capacité à générer des tentatives plausibles de recherche en mathématiques. Cependant, un goulot d'étranglement critique subsiste : la vérification. Valider ces solutions nécessite généralement un temps d'expert rare ou repose sur des évaluateurs « sans oracle » tels que des juges LLM et des modèles de récompense, qui sont souvent peu fiables, biaisés et susceptibles d'être induits en erreur par des indices stylistiques ou des déclarations d'autorité.

Le défi central abordé est la manière d'évaluer la correction de solutions candidates pour des questions de niveau recherche où les réponses de vérité terrain sont indisponibles, où les problèmes ne sont pas encore résolus par l'état de l'art, et où la validation par des experts n'est pas évolutive. Les méthodes existantes sans oracle (par exemple, le vote majoritaire, les modèles de récompense, les juges LLM) peinent à distinguer les solutions correctes des solutions incorrectes dans ce régime de haute difficulté, échouant souvent à séparer le raisonnement valide de l'hallucination « plausible mais erronée ».

Méthodologie : Utilité basée sur les conséquences (CBU)

Les auteurs proposent l'Utilité basée sur les conséquences (Consequence-Based Utility - CBU), un cadre d'évaluation sans oracle fondé sur le concept mathématique de « support par les conséquences ». L'hypothèse centrale est qu'une solution correcte contient une information au niveau de la méthode qui se transfère efficacement à des problèmes connexes, contrairement à une solution incorrecte.

Mécanisme central

1. Construction du voisinage : Pour une question de recherche cible $Q$ et une solution candidate $C$, le système construit un ensemble de questions de voisinage $\mathcal{N}(Q)$. Ce sont des variantes de $Q$ (par exemple, des paramètres modifiés ou des théorèmes liés) conçues pour être vérifiables (ayant des vérités terrain connues) et légèrement plus faciles que l'originale, tout en étant solubles en utilisant la logique de $C$.
2. Transfert en contexte : La solution candidate $C$ est utilisée comme un exemple contextuel (démonstration) pour un modèle de résolution $M_\theta$. Le solveur est incité à résoudre chaque question $Q^* \in \mathcal{N}(Q)$ conditionnée par $(Q, C)$.
3. Score d'utilité : Le score d'utilité $U(C)$ est défini comme l'exactitude moyenne du solveur sur les questions de voisinage lorsque $C$ est fourni en contexte.
   $$U(C) = \frac{1}{|\mathcal{N}(Q)|} \sum_{Q^* \in \mathcal{N}(Q)} \mathbb{E}_{\tilde{C} \sim M_\theta(\cdot|Q,C,Q^*)} [v(Q^*, \tilde{C})]$$
   où $v$ est un vérificateur contrôlant la correction de la sortie du solveur.
4. Classement : Les candidats sont classés par leurs scores d'utilité induits. Un score plus élevé implique que le candidat fournit un raisonnement plus utile et transférable, suggérant qu'il est plus susceptible d'être correct.

Jeu de données : EXPERTMATH

Pour évaluer cette approche, les auteurs introduisent EXPERTMATH, un benchmark composé de :

• 192 problèmes de niveau recherche écrits par des experts (couvrant la théorie des représentations, la combinatoire algébrique, la géométrie et la théorie de l'homotopie). La moitié d'entre eux restent non résolus par les modèles de pointe (ex: GPT-5, Gemini-3-Pro).
• 425 problèmes générés par LLM dérivés de la littérature existante.
• Vérité terrain : Chaque problème est associé à une solution écrite par un expert et à neuf solutions candidates générées par LLM (quatre correctes, cinq incorrectes), vérifiées manuellement par des humains.

Principales contributions

1. Utilité basée sur les conséquences (CBU) : Une nouvelle méthode de validation sans oracle qui évalue les solutions sur la base de leurs performances en aval sur des questions connexes plutôt que par l'inspection directe du texte de la solution.
2. Benchmark EXPERTMATH : Un jeu de données de haute difficulté comprenant des problèmes mathématiques de niveau recherche avec des solutions vérifiées par des experts et des candidats générés par LLM, spécifiquement conçu pour tester les méthodes d'évaluation sur des problèmes que les modèles actuels ne peuvent pas résoudre directement.
3. Supériorité empirique : Démonstration que la CBU surpasse systématiquement les autres bases de comparaison sans oracle, y compris les juges LLM, les modèles de récompense (RM) et les modèles de récompense génératifs (GenRM).
4. Analyse d'erreurs et modes de défaillance : Identification de modes de défaillance spécifiques des juges LLM (par exemple, dépendance excessive à la verbosité, compression injustifiée et indices d'autorité) que la CBU évite avec succès en pénalisant les solutions qui ne parviennent pas à transférer le raisonnement.

Résultats expérimentaux

Évaluée sur EXPERTMATH en utilisant des modèles tels que GPT-OSS-120B et Qwen3-235B-A22B :

• Qualité du classement : La CBU améliore significativement les métriques de classement par rapport aux bases de comparaison.
  • Pour GPT-OSS-120B agissant comme solveur/évaluateur, la CBU améliore l'Acc@1 (exactitude de la solution la mieux classée) de 67,2 % à 76,3 % et l'AUC (Aire sous la courbe) de 71,4 % à 79,6 %.
  • Des gains similaires sont observés pour des modèles plus petits (ex: l'AUC de GPT-OSS-20B passe de 69,0 à 79,2).
• Écart Solveur-Évaluateur : La CBU maintient une séparation plus grande entre les solutions correctes et incorrectes, même sur des questions que le solveur sous-jacent ne peut pas résoudre lui-même. Alors que la capacité des juges LLM à distinguer les solutions correctes des incorrectes se dégrade fortement à mesure que la difficulté du problème augmente, la CBU reste robuste.
• Pouvoir prédictif : Les classificateurs de régression logistique entraînés sur les scores CBU atteignent une précision plus élevée pour prédire la correction binaire par rapport à ceux entraînés sur les scores des juges LLM (ex: gains de +6 à +18 points de pourcentage à travers les backbones).
• Robustesse au style : Contra-irement aux juges LLM, souvent induits en erreur par des solutions incorrectes verbeuses ou au ton « autoritaire », la CBU déclasse les solutions présentant une compression injustifiée (étapes manquantes) et un raisonnement incorrect, car celles-ci ne fournissent pas d'informations transférables pour les questions de voisinage.

Signification et affirmations

L'article affirme que l'Utilité basée sur les conséquences offre une alternative évolutive et fiable à la validation par des experts humains pour les productions scientifiques de niveau recherche. Sa signification réside dans :

• Validation sans oracle : Elle permet l'évaluation de problèmes « insolubles » sans nécessiter d'oracle de vérité terrain pour la question cible spécifique.
• Changement de paradigme d'évaluation : Elle déplace l'évaluation de l'« inspection statique » (juger le texte d'une preuve) vers l'« utilité dynamique » (juger la capacité d'une preuve à permettre la résolution de problèmes connexes).
• Applicabilité pratique : Les auteurs fournissent un guide pour les praticiens, montrant que la CBU reste efficace même lorsque les questions de voisinage sont générées par des LLM (à condition que les questions cibles soient suffisamment difficiles) et que des estimations stables peuvent être obtenues avec un nombre modéré de passages (ex: $n \ge 8$).

Les auteurs concluent que la CBU est particulièrement adaptée à la validation scientifique à enjeux élevés, où une séparation de haute confiance entre hypothèses correctes et incorrectes est requise, et là où les juges LLM traditionnels échouent en raison d'erreurs de raisonnement subtiles ou de biais stylistiques.