Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models

Ce papier présente OlymMATH, un nouveau benchmark de niveau olympique composé de 350 problèmes mathématiques rigoureusement sélectionnés et disponibles en anglais et en chinois, conçu pour évaluer les grands modèles de raisonnement à la fois par des réponses numériques et par une vérification formelle en Lean 4.

L'essentiel

Imagine que les grands modèles de langage (les IA comme moi) sont des élèves brillants qui ont lu toute la bibliothèque du monde. Pendant un moment, on pensait qu'ils pouvaient résoudre n'importe quel problème de mathématiques. Mais en réalité, ils ont commencé à "tricher" : ils ont mémorisé les réponses des examens précédents plutôt que d'apprendre à raisonner.

C'est là qu'intervient cette nouvelle recherche, qui présente OlymMATH. Voici une explication simple de ce projet, avec quelques images pour mieux comprendre.

1. Le Problème : L'École a été "Hackée"

Imaginez que vous préparez un élève pour un examen de mathématiques très difficile (niveau Olympiades). Si vous lui donnez un livre d'exercices qui circule déjà sur Internet, il va simplement apprendre les réponses par cœur. Il aura l'air d'un génie, mais s'il rencontre un problème légèrement différent, il sera perdu.

Les chercheurs ont constaté que les benchmarks (les tests) actuels étaient comme ce livre d'exercices piraté : les IA les avaient déjà vus partout sur le web. Elles ne raisonnaient pas vraiment, elles "récitaient".

2. La Solution : OlymMATH, le "Nouveau Programme Secret"

Pour tester la vraie intelligence, les chercheurs ont créé OlymMATH. C'est comme si on avait créé un nouvel examen, secret, qui n'existe nulle part sur Internet.

• La Source : Au lieu de copier-coller des problèmes sur le web, ils sont allés chercher des exercices dans de vieux livres papier et des magazines spécialisés, que personne n'a encore numérisés. C'est comme si on avait fouillé dans des greniers poussiéreux pour trouver des énigmes que les IA n'ont jamais vues.
• La Double Épreuve : OlymMATH est unique car il teste les IA de deux manières, comme un examen qui vérifierait à la fois la réponse et la méthode :
  1. Le Résultat (OlymMATH-EASY/HARD) : L'IA doit donner le bon chiffre. C'est facile à vérifier, comme corriger un QCM.
  2. La Méthode (OlymMATH-LEAN) : C'est la partie géniale. L'IA doit écrire sa solution dans un langage informatique très strict (appelé Lean). C'est comme si l'élève devait non seulement donner la réponse, mais aussi écrire son devoir de manière que l'ordinateur puisse prouver mathématiquement que chaque étape est logique. Si l'IA triche ou devine, l'ordinateur dit "Erreur" et refuse de valider.

3. Le Test : Les IA sont-elles vraiment intelligentes ?

Les chercheurs ont lancé ce test contre les IA les plus puissantes du monde (comme celles d'OpenAI, Google ou DeepSeek).

• Le Résultat : C'est un désastre... pour les IA ! Même les modèles les plus avancés ont obtenu de très mauvaises notes. Par exemple, sur les problèmes les plus difficiles, les meilleures IA n'ont réussi qu'environ 30 à 50 % des questions.
• La Révélation : En regardant de plus près, les chercheurs ont découvert que les IA utilisaient souvent des "astuces". Parfois, elles devinaient la réponse en supposant que la figure était symétrique, sans vraiment le prouver. C'est comme un élève qui dit "La réponse est 5, parce que ça a l'air logique" sans montrer ses calculs.
  • Avec OlymMATH-LEAN, ces tricheries sont immédiatement démasquées, car l'ordinateur exige une preuve rigoureuse.

4. Une Surprise : La Barrière de la Langue

Une autre découverte intéressante : les IA réussissent beaucoup mieux en anglais qu'en chinois, même si elles sont censées comprendre les deux.

• L'Analogie : Imaginez un bilingue qui est excellent en mathématiques quand il lit un livre en anglais, mais qui commence à bégayer et à faire des erreurs quand le même livre est en chinois. Cela montre que les IA ont "mangé" beaucoup plus de données en anglais pendant leur apprentissage, et qu'elles sont moins à l'aise dans d'autres langues pour les tâches complexes.

En Résumé

OlymMATH est comme un nouveau garde-fou pour l'intelligence artificielle.

• C'est un examen secret (pas de triche possible).
• C'est un double test (réponse + preuve rigoureuse).
• Il nous apprend que nos IA sont encore loin d'être des génies : elles savent souvent "deviner" la réponse, mais elles peinent encore à faire de véritables raisonnements logiques, surtout dans des langues autres que l'anglais.

C'est un outil précieux pour aider les chercheurs à construire de vraies IA capables de penser, et pas seulement de réciter.

Résumé technique

1. Problématique et Contexte

L'avancement rapide des modèles de raisonnement (LLM) a saturé les benchmarks mathématiques existants (comme GSM8K, MATH, ou même AIME), rendant difficile l'évaluation des capacités réelles des modèles les plus avancés. Les benchmarks actuels souffrent de plusieurs limitations critiques :

• Contamination des données : De nombreuses suites de problèmes sont issues de sources en ligne (compétitions connues, AoPS), ce qui augmente le risque que les modèles aient déjà vu les problèmes lors de l'entraînement.
• Évaluation insuffisante : La plupart des benchmarks se basent uniquement sur la réponse finale (vérification par règles), ce qui ne permet pas de distinguer un raisonnement rigoureux d'une "devinette" heuristique ou d'une réponse correcte obtenue par hasard.
• Manque de formalisme : Peu de benchmarks intègrent la vérification formelle (preuves mathématiques vérifiables par machine) et la plupart sont monolingues (anglais), négligeant les capacités multilingues.

L'objectif de cet article est de combler ces lacunes en introduisant OlymMATH, un benchmark de niveau Olympiade rigoureusement conçu pour tester les limites du raisonnement mathématique des LLM.

2. Méthodologie et Construction du Benchmark

OlymMATH est une suite bilingue (Anglais et Chinois) composée de 350 problèmes uniques, issus de publications imprimées (livres et magazines spécialisés) pour minimiser la contamination des données. Le benchmark est divisé en trois sous-ensembles non chevauchants, unifiant deux paradigmes d'évaluation :

A. Évaluation par Langage Naturel (OlymMATH-EASY & HARD)

• Contenu : 200 problèmes computationnels (100 "Faciles", 100 "Difficiles").
• Format : Énoncés en anglais et chinois, nécessitant des réponses numériques précises.
• Vérification : Basée sur des règles (via sympy), permettant une évaluation objective et scalable.
• Spécificité : Les problèmes "HARD" sont conçus pour être hors de portée des modèles actuels, même avec des modes de réflexion lents. Certains problèmes comportent plusieurs réponses possibles, obligeant le modèle à les identifier toutes (somme des carrés, etc.).

B. Évaluation par Vérification Formelle (OlymMATH-LEAN)

• Contenu : 150 problèmes formalisés en Lean 4 (Mathlib v4.24.0).
• Objectif : Évaluer la capacité des modèles à générer des preuves mathématiques rigoureuses et vérifiables par machine, plutôt que de simples réponses numériques.
• Avantage : Élimine le risque de "devinette" heuristique. Une preuve incorrecte ou incomplète (utilisant sorry ou des hypothèses non justifiées) échouera à compiler.
• Processus : Les problèmes ont été traduits, formalisés et vérifiés par des agents IA (Claude Opus, DeepSeek V3) et des experts humains, avec une validation itérative via un serveur Lean.

C. Analyse de Contamination

Les auteurs ont utilisé une métrique de n-grammes pour comparer OlymMATH à des benchmarks existants (comme PolyMath). Les résultats montrent un risque de contamination significativement plus faible pour OlymMATH, confirmant sa fiabilité pour évaluer les capacités réelles des modèles.

3. Contributions Clés

1. Premier Benchmark Unifié Bilingue : OlymMATH est le premier benchmark de niveau Olympiade à intégrer simultanément l'évaluation par réponse numérique (langage naturel) et la vérification formelle (Lean 4) dans un cadre bilingue (Anglais/Chinois).
2. Rigueur et Pureté des Données : L'origine imprimée des problèmes et la vérification par des experts (médaille d'argent aux Olympiades chinoises) garantissent une faible contamination et une haute qualité.
3. Détection des "Devinettes" (Guessing) : En comparant les résultats entre les épreuves naturelles et formelles, le benchmark permet d'identifier les cas où les modèles obtiennent la bonne réponse sans raisonnement rigoureux (heuristiques, symétrie supposée sans preuve).
4. Ressources Open Source : Publication de 582 400 trajectoires de raisonnement issues de 28 modèles, d'un outil de visualisation interactif et de solutions d'experts.

4. Résultats Expérimentaux

Les auteurs ont évalué des modèles de pointe (DeepSeek-R1, o3-mini, Gemini 2.5 Pro, Qwen3, etc.) sur OlymMATH.

• Difficulté Extrême : Même les modèles les plus performants peinent sur la version "HARD".
  • DeepSeek-R1 : ~19.5% de précision sur OlymMATH-HARD (EN).
  • o3-mini (high) : ~31.2%.
  • Gemini 2.5 Pro Exp : ~58.4%.
  • Comparaison : Alors que ces modèles obtiennent >87% sur AIME 2024, leur chute drastique sur OlymMATH-HARD démontre la supériorité discriminative de ce nouveau benchmark.
• Écart Linguistique (Gap EN-ZH) : Tous les modèles obtiennent de meilleurs résultats en anglais qu'en chinois, soulignant un biais dans les données d'entraînement et la nécessité d'évaluations multilingues.
• Incohérence du Raisonnement : L'analyse Pass@k montre que si les modèles peuvent trouver la solution correcte avec de nombreux échantillons (Pass@64), ils échouent souvent à le faire de manière fiable (faible Consistency), indiquant une instabilité du raisonnement.
• Échec des Heuristiques : Dans l'évaluation Lean, les modèles obtiennent des scores très bas (~10% de réussite), révélant que les "raccourcis" heuristiques utilisés en langage naturel ne fonctionnent pas dans un cadre formel strict. Les erreurs fréquentes incluent l'échec d'extraction de code, des erreurs de compilation et l'utilisation abusive de sorry.

5. Signification et Impact

Ce travail marque une étape cruciale dans l'évaluation des LLM :

• Au-delà de la réponse finale : Il force la communauté à passer d'une évaluation basée sur le résultat (outcome-based) à une évaluation basée sur le processus (process-level), essentielle pour le développement de l'AGI.
• Détection des illusions de compétence : En révélant que les modèles utilisent souvent des "devinettes" pour réussir les benchmarks actuels, OlymMATH offre un moyen de filtrer les modèles qui ne possèdent pas de véritable capacité de raisonnement.
• Futur de la recherche : La disponibilité des trajectoires de raisonnement et des preuves formelles ouvre la voie à l'entraînement de modèles de récompense (Reward Models) basés sur la rigueur logique et à l'amélioration des capacités de raisonnement formel.

En conclusion, OlymMATH établit un nouvel étalon-or pour les mathématiques, démontrant que malgré les progrès récents, le raisonnement mathématique de niveau Olympiade reste un défi majeur pour l'intelligence artificielle actuelle.