Résumé Technique : IMProofBench

Énoncé du Problème

Les benchmarks actuels pour évaluer les modèles de langage de grande taille (LLM) en mathématiques sont insuffisants pour évaluer les capacités de niveau recherche. Les jeux de données existants se concentrent principalement sur des problèmes de niveau lycée ou premier cycle universitaire (par exemple, AIME, MATH), qui sont de plus en plus solubles par les modèles de pointe et ne parviennent pas à tester de véritables capacités de rédaction de preuves. De plus, les benchmarks ciblant les mathématiques avancées, tels que FrontierMath et Humanity's Last Exam (HLE), limitent souvent l'évaluation à la justesse de la réponse finale. Cette limitation permet aux modèles d'employer des raccourcis ou de deviner la bonne réponse sans construire d'arguments logiquement fondés, négligeant ainsi la compétence critique de la génération de preuves rigoureuses. Il existe un manque de benchmark standardisé et privé capable d'évaluer la génération de preuves de niveau recherche dans un environnement réaliste et augmenté par des outils.

Méthodologie

Construction du Benchmark (IMProofBench)

IMProofBench est un benchmark privé comprenant 77 problèmes examinés par des pairs, développés en collaboration avec plus de 44 mathématiciens professionnels. Le pipeline de création des problèmes implique :

• Auteur : Les problèmes sont rédigés par des chercheurs dans leurs domaines d'expertise respectifs, allant des questions d'examen oral de niveau master aux problèmes de recherche ouverte.
• Examen par les pairs : Chaque soumission est soumise à un processus de révision rigoureux par un membre de l'équipe centrale et un expert externe dans le domaine concerné afin de garantir l'exactitude mathématique, la difficulté appropriée et la clarté.
• Structure : Chaque problème se compose d'une tâche principale de rédaction de preuve et de sous-questions de suivi avec des réponses uniques et automatiquement évaluables. Cette double structure permet à la fois l'évaluation humaine de la preuve par un expert et l'analyse quantitative automatisée des réponses finales.
• Nature Dynamique : Le benchmark est conçu comme une plateforme continue. Les problèmes sont ajoutés de manière régulière, et les auteurs sont encouragés à retirer les problèmes s'ils deviennent solubles grâce à de nouvelles recherches, garantissant ainsi que le benchmark ne soit pas saturé.

Cadre d'Évaluation

L'évaluation simule un environnement de recherche réaliste en utilisant un cadre agentique construit sur le framework Inspect. Les modèles opèrent avec accès à :

• Outils de Calcul : Python (NumPy, SciPy, SymPy), Bash (Arch Linux), et des logiciels mathématiques spécialisés incluant SageMath, GAP, Maxima, PARI/GP et Singular.
• Recherche de Littérature : Des capacités de recherche web pour localiser des théorèmes, des articles ou des données pertinents (ex: OEIS).
• Interaction : Les modèles s'engagent dans des interactions multi-tours, utilisant un outil submit pour distinguer les étapes de raisonnement des sorties finales.

Processus de Notation

L'évaluation se déroule en deux étapes :

1. Notation Automatisée : Les sous-questions de suivi sont notées en comparant les sorties du modèle aux réponses de référence (ground-truth).
2. Notation par des Experts Humains : La preuve principale est évaluée par l'auteur du problème selon une échelle de 0 à 3 :
   • 0/3 : Aucun progrès.
   • 1/3 : Progrès mineur (avancement limité).
   • 2/3 : Progrès majeur (travail substantiel accompli).
   • 3/3 : Solution complète.
     Les correcteurs annotent également les types d'erreurs spécifiques (erreurs logiques, hallucinations, erreurs de calcul, incompréhensions conceptuelles) et les indicateurs de réussite (compréhension, résultats corrects, intuitions, utilité). Pour éviter les biais, l'identité des modèles est masquée lors de la notation.

Contributions Clés

1. IMProofBench : Un benchmark privé et évolutif spécifiquement conçu pour la génération de preuves mathématiques de niveau recherche, développé via une collaboration directe avec la communauté mathématique.
2. Analyse Systématique : Une évaluation complète des LLM de pointe sur la génération de preuves, jugée par des experts humains, allant au-delà de la simple exactitude de la réponse finale.
3. Aperçus Qualitatifs : Une analyse détaillée des forces et des modes de défaillance des modèles, soulignant l'écart entre l'exactitude de la réponse finale et la capacité réelle de rédaction de preuves, ainsi que l'interaction des modèles avec les outils de recherche.

Résultats Expérimentaux

Aperçu des Performances

Les auteurs ont évalué 10 LLM sur la partie basée sur les preuves du benchmark :

• Meilleurs Performeurs : GPT-5.4 a obtenu la meilleure performance, produisant des solutions complètes (3/3) pour 49 % des tâches. GEMINI-3.1-PRO suit de près avec 46 %.
• Moins Bons Performeurs : CLAUDE-OPUS-4.6 n'a fourni des solutions complètes que pour 32 % des tâches.
• Problèmes Ouverts : Parmi les 23 questions de recherche ouvertes du benchmark, GPT-5 en a résolu une en décembre 2025.

Réponse Finale vs Génération de Preuve

Sur le sous-ensemble de 45 questions comportant des sous-questions de suivi, GPT-5.4 a obtenu un score de 75 % sur l'exactitude de la réponse finale. La corrélation entre les scores des sous-questions et le progrès de la preuve noté par l'humain était de 0,51, suggérant que bien que l'exactitude de la réponse finale soit un indicateur utile, elle manque de la nuance requise pour évaluer la qualité du processus de raisonnement.

Analyse des Erreurs et des Outils

• Types d'Erreurs : Les erreurs logiques étaient le mode de défaillance le plus courant (ex: hypothèses non fondées), particulièrement dans CLAUDE-OPUS-4.6 (40 % des réponses). Des hallucinations de théorèmes inexistants ont également été observées.
• Utilisation des Outils : Les modèles varient considérablement dans leur utilisation des outils. GEMINI-3.1-PRO a effectué près de quatre fois plus d'appels d'outils que les autres modèles, mais a utilisé le moins de jetons de sortie.
• Étude d'Ablation : Une ablation sur la configuration agentique a révélé que l'accès aux outils améliore généralement la performance (ex: +14,4 % pour GROK-4), bien que certains modèles (ex: GEMINI-2.5-PRO) aient connu de légères baisses, probablement dues à une sélection d'outils sous-optimale (ex: surutilisation des interpréteurs de code pour le raisonnement mathématique).

Observations Qualitatives

• Connaissance de la Littérature : Les modèles de tête ont démontré une forte familiarité avec la littérature mathématique spécialisée mais ont éprouvé des difficultés avec les sources plus obscures comme les notes de cours privées.
• Hallucination et Confiance : Les modèles ont fréquemment halluciné des résultats pour forcer une réponse et ont rarement décliné de fournir une solution, même lorsqu'ils étaient bloqués. Ils présentent souvent des arguments erronés avec une grande confiance.
• Intuition : Malgré les erreurs, les modèles fournissent fréquemment des intuitions et des progrès partiels qui pourraient être utiles aux chercheurs humains, GPT-5.4 offrant des contributions significatives dans environ 60 % des tentatives.

Signification et Revendications

L'article affirme que IMProofBench comble une lacune critique dans l'évaluation de l'IA en déplaçant l'accent des problèmes de type compétition vers la génération de preuves de niveau recherche. Les auteurs soutiennent que :

1. Capacités Actuelles : Les LLM de pointe peuvent déjà résoudre un sous-ensemble significatif de problèmes de niveau recherche, indiquant leur potentiel en tant que collaborateurs mathématiques.
2. Limitations : Les modèles actuels restent imparfaits, sujets aux erreurs logiques et aux hallucinations, et manquent souvent de la capacité à distinguer une réponse finale correcte d'une preuve valide.
3. Nécessité d'Évaluation : Le benchmark démontre que les métriques de réponse finale sont insuffisantes pour mesurer la capacité mathématique ; l'évaluation humaine de l'expert sur le processus de raisonnement est essentielle.
4. Direction Future : Ce travail établit un cadre pour une évaluation continue et dynamique des LLM dans des contextes de recherche réalistes, facilitant l'étude de la manière dont l'IA peut être intégrée efficacement dans les flux de travail mathématiques.

Les auteurs maintiennent une position modeste, notant que le benchmark est actuellement en développement actif avec un nombre limité de problèmes (77), mais soutiennent que même cette échelle fournit des informations précieuses sur la trajectoire de l'IA dans la recherche mathématique.