Résumé technique : FormInv, un protocole de mesure pour l'invariance sémantique dans les benchmarks de raisonnement mathématique

1. Énoncé du problème

Les benchmarks actuels pour le raisonnement mathématique dans les grands modèles de langage (LLM) reposent fortement sur des métriques d'exactitude agrégées calculées sur des formulations canoniques de problèmes. Cet article soutient que de telles métriques sont insuffisantes car elles supposent que la performance du modèle est indépendante de la manière dont une question est formulée. Les auteurs identifient un « écart de mesure » critique : les modèles affichent souvent une exactitude élevée sur les benchmarks standards, mais échouent à maintenir l'invariance sémantique — la capacité de produire des réponses cohérentes à travers des paraphrases logiquement équivalentes.

L'article souligne que les benchmarks standards (par exemple, GSM8K, MATH, MathCheck) manquent d'une vérification rigoureuse de l'équivalence sémantique des paraphrases. Par conséquent, les classements des benchmarks peuvent être des artefacts de formulations spécifiques plutôt que de véritables mesures de la capacité de raisonnement. Les auteurs s'appuient sur la théorie psychométrique, notamment le Fonctionnement Différentiel des Items (DIF) et la Théorie de la Généralisabilité, pour formaliser cette problématique. Ils postulent que si la réponse d'un modèle change en fonction de reformulations sémantiquement équivalentes, cela indique un échec de la compréhension mathématique authentique, reposant plutôt sur la reconnaissance de motifs de surface.

2. Méthodologie

2.1 Le protocole FormInv

Les auteurs proposent FormInv, un protocole de mesure conçu pour auditer et quantifier l'invariance sémantique. Le protocole se compose de trois composantes principales :

1. L'Écart d'Invariance (EI) et le Taux de Cohérence Sémantique (TCS) :

   • EI : Défini formellement comme l'écart-type des réponses binaires d'un modèle à travers une classe d'équivalence de paraphrases. Mathématiquement, $EI(f, [x]_\sim) = \sqrt{p(1-p)}$, où $p$ est la probabilité d'une réponse correcte au sein de la classe d'équivalence. Un EI de 0 implique une invariance parfaite.
   • TCS : La proportion de théorèmes pour lesquels le modèle répond correctement à travers toutes les formes de paraphrase. Contrairement à l'EI, qui mesure la variance, le TCS mesure l'intersection de la justesse et de l'invariance.
   • Test Q de Cochran : Utilisé comme test statistique d'homogénéité marginale à travers $k > 2$ familles de paraphrases pour déterminer si le taux d'échec d'un modèle varie significativement selon la famille.

2. La taxonomie de paraphrase à 8 familles :
   Le benchmark évalue les modèles à travers huit familles de transformations distinctes, catégorisées par leur rigueur de vérification :

   • T1 (Certifiable formellement) : Familles F4 (notation), F6 (ordre), F7 (dépaquetage) et F8 (équivalence). Celles-ci reposent sur des règles Lean4/FOL ou une vérification par Système d'Algèbre Informatique (CAS) (par exemple, SymPy).
   • T2 (Valide conditionnellement) : Familles F1 (syntaxique), F2 (quantificateur) et F3 (passif). Celles-ci dépendent du contexte de type et sont vérifiées via des modèles ou un CAS le cas échéant.
   • T3 (Heuristique) : Famille F5 (variation des connecteurs). Celles-ci reposent sur des heuristiques de langage naturel et nécessitent un examen par des experts du domaine.

3. Audit d'unanimité inter-modèles :
   Un mécanisme de contrôle qualité novateur où une paraphrase est signalée comme sémantiquement incorrecte si une supermajorité de modèles (par exemple, $\ge 6/9$) échouent à la paraphrase tout en réussissant la version canonique. Cela exploite l'hypothèse selon laquelle des erreurs systématiques dans la paraphrase elle-même, plutôt que dans le raisonnement du modèle, provoquent un échec universel.

2.2 Construction du benchmark

• Substrat : L'évaluation utilise 103 théorèmes soigneusement sélectionnés issus de Mathlib4 (vérifiés par Lean4), couvrant des domaines tels que la théorie des nombres, l'algèbre et l'analyse réelle.
• Jeu de données : Le jeu de données principal (FormInv v1) contient 760 éléments (103 théorèmes $\times$ ~7,4 paraphrases). Une évaluation étendue « Track B » utilise 100 théorèmes plus difficiles issus de ntp-mathlib (811 éléments).
• Vérification : Les paraphrases sont générées via GPT-4o et vérifiées via un protocole multi-étapes : CAS pour les familles algébriques, garanties de modèles pour les familles de surface, et examen à 100 % par des experts humains pour les familles définitionnelles (F7/F8).

2.3 Configuration expérimentale

L'étude évalue 9 modèles de pointe (incluant GPT-4o, Claude Sonnet/Haiku, DeepSeek V3/R1, Gemini 2.5 Flash et Llama 3.3 70B) sur les 366 à 811 éléments. Les modèles sont évalués en mode zéro-shot avec des contraintes strictes VRAI/FAUX.

3. Résultats clés

3.1 L'écart d'invariance versus l'exactitude

La découverte la plus significative est le décalage entre l'exactitude agrégée et la cohérence sémantique.

• Claude Haiku 4.5 atteint 86 % d'exactitude mais seulement 50 % de TCS, ce qui signifie que la moitié de ses réponses correctes sont incohérentes à travers les paraphrases.
• DeepSeek V3 atteint 96,4 % d'exactitude et 82 % de TCS.
• Un écart de 10 points en exactitude cache un écart de 32 points en TCS. L'article note que l'exactitude seule est « constitutionnellement aveugle » à cet échec structurel.
• Il existe une forte corrélation négative ($r = -0,965$) entre l'exactitude et l'EI moyen, suggérant que les modèles plus exacts sont généralement plus invariants, mais cette corrélation est entraînée algébriquement par la définition de l'EI et ne garantit pas l'invariance pour des familles spécifiques.

3.2 Inversions de classement et complémentarité

Les classements des modèles ne sont pas stables ; ils s'inversent en fonction de la famille de paraphrase :

• F6 (Ordre de comparaison) : GPT-4o échoue à 0,0 % des éléments, tandis que Claude Sonnet échoue à 16,7 %.
• F7 (Dépaquetage définitionnel) : Claude Sonnet échoue à ~6 %, tandis que GPT-4o échoue à 10,0 %.
• Ce modèle d'échec complémentaire implique qu'aucun modèle unique ne domine au sens de Pareto toutes les familles. Par conséquent, les concepteurs de benchmarks choisissent implicitement un pondération des familles qui détermine le gagnant. L'article formalise cela comme le corollaire « Pas de benchmark gratuit » : pour tout classement cible, il existe une pondération $\lambda$ sur les familles de paraphrases qui le réalise.

3.3 Résultats de l'audit de qualité

Le protocole d'unanimité inter-modèles a permis d'identifier avec succès des paraphrases sémantiquement incorrectes dans les benchmarks existants :

• Audit MathCheck : Appliqué à 129 groupes dans MathCheck, le protocole a signalé 4 paraphrases sémantiquement incorrectes (3,1 %). La suppression de ces erreurs a fait passer GPT-4o du rang 2 au rang 4, élevant Claude Haiku et DeepSeek V3.
• Audit FormInv v1 : Le protocole a identifié 11 erreurs dans les éléments générés par GPT-4o, notamment une surextension des biconditionnels, des inversions de voix passive et un dénuement de contexte de type. Ces erreurs étaient invisibles pour une évaluation mono-modèle mais ont été exposées par l'unanimité.

3.4 Dépendance au régime de difficulté

Dans l'évaluation « Track B » utilisant des théorèmes plus difficiles :

• La corrélation entre l'exactitude et l'invariance s'est affaiblie ($r = -0,415$, non significative).
• La difficulté spécifique de F5 (variation des connecteurs) s'est dissoute ; toutes les familles se sont regroupées autour de taux d'échec similaires (28–35 %).
• Les modèles de raisonnement (DeepSeek R1, o4-mini) ont montré l'EI le plus faible sur les théorèmes difficiles, suggérant que la délibération par Chaîne de Pensée réduit la sensibilité de surface uniquement lorsque les théorèmes exigent un raisonnement de haut niveau.

4. Contributions

1. Cadre d'invariance : Formalisation du TCS et de l'EI comme métriques principales pour l'invariance sémantique, fondées sur le théorème de l'espérance conditionnelle de Doob et la théorie du DIF. Il classe les familles de paraphrases en niveaux T1, T2 et T3 basés sur la rigueur de vérification.
2. Benchmark FormInv : Un jeu de données de plus de 760 éléments dérivés de théorèmes vérifiés par Lean4, évalué sur 9 modèles avec un audit rigoureux d'unanimité inter-modèles.
3. FormInvSelector : Un algorithme qui utilise les profils de TCS par famille pour recommander le modèle ayant le taux d'échec attendu le plus faible pour des régimes de tâches spécifiques (par exemple, sélectionner un modèle pour le raisonnement définitionnel versus des tâches de comparaison).
4. Audit de qualité des paraphrases : Démontre que l'unanimité inter-modèles ($\ge 6/9$ modèles échouant une paraphrase) est une méthode automatisée et peu coûteuse pour détecter des éléments de benchmark sémantiquement incorrects, séparant efficacement les erreurs de benchmark des erreurs de modèle.

5. Signification et affirmations

L'article affirme que FormInv est le premier protocole à appliquer la théorie de l'invariance de mesure et des métriques fondées sur le DIF au raisonnement mathématique formel. Sa signification réside dans trois domaines :

• Révélation de défauts cachés : Il expose que les métriques d'exactitude standards peuvent être trompeuses, masquant un « écart de 32 points » entre la performance de surface et la compréhension sémantique authentique.
• Intégrité du benchmark : Il fournit un outil aux concepteurs de benchmarks pour auditer leurs propres jeux de données avant publication, empêchant les classements d'être des artefacts de paraphrases défectueuses. Les auteurs affirment que « si vous générez des paraphrases de manière programmatique, vous ne savez pas combien sont erronées ».
• Évaluation consciente du régime : Il remet en question la notion d'un seul modèle « meilleur », démontrant que les classements dépendent du régime (variant selon la famille de paraphrase et la difficulté). L'article conclut que les concepteurs de benchmarks choisissent implicitement les gagnants en sélectionnant quelles familles inclure, et que FormInv rend ce choix explicite et auditable.

Les auteurs restent modestes concernant les limites, notant que la certification à grande échelle de toutes les paraphrases via Lean4 est un travail futur, et que l'étude actuelle repose sur un ensemble sélectionné de 103 théorèmes (bien qu'étendu à 100 autres plus difficiles dans Track B). Ils soulignent que FormInv est une métrique complémentaire destinée à compléter, et non à remplacer, les évaluations existantes basées sur l'exactitude.