💻 computer science

Benchmarking Testing in Automated Theorem Proving

Cet article présente « T », un cadre novateur qui évalue la correction sémantique des théorèmes formels générés par l'IA en vérifiant si les théorèmes successeurs dépendants se compilent avec succès, révélant ainsi un écart significatif entre les capacités de génération de théorèmes des grands modèles de langage actuels et les méthodes d'évaluation traditionnelles, qu'elles soient lexicales ou manuelles.

Auteurs originaux : Jongyoon Kim, Hojae Han, Seung-won Hwang

Publié 2026-04-28

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Jongyoon Kim, Hojae Han, Seung-won Hwang

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous embauchiez une équipe d'architectes pour concevoir un nouveau pont.

L'ancienne méthode de test (Compilation)
Par le passé, lors de l'évaluation de ces architectes (qui, dans cet article, sont des modèles d'IA), nous ne vérifions que si leurs plans étaient « grammaticalement corrects ». Nous demandions : Le plan respecte-t-il les règles de grammaire ? Les lignes se connectent-elles ? L'ordinateur dit-il « Syntaxe OK » ?

Si le plan semblait parfait sur le papier, nous supposions que le pont tiendrait. Mais voici le problème : un architecte pourrait dessiner un plan indiquant « Ce pont est fait d'or massif », et l'ordinateur répondrait « Syntaxe OK ! » car la phrase est grammaticalement correcte. Cependant, si le plan était censé être pour un « pont suspendu en acier », l'architecte aurait échoué à sa véritable tâche, même si la grammaire était parfaite.

Dans le monde des mathématiques et du code informatique, cela s'appelle la Compilation. L'IA écrit un théorème (une affirmation mathématique), et l'ordinateur vérifie s'il se compile (s'exécute sans erreurs). L'article soutient que c'est une terrible façon de juger si l'IA a réellement compris les mathématiques.

La nouvelle méthode de test (Cadre T2)
Les auteurs de cet article proposent une nouvelle méthode appelée T2 (Test de Théorème). Au lieu de simplement vérifier la grammaire du plan, ils demandent : Ce plan fonctionne-t-il réellement lorsque nous essayons de construire le reste de la ville autour de lui ?

Ils utilisent un concept appelé Test d'Intégration. Imaginez que le pont n'est qu'une partie d'une ville massive.

La Cible : L'IA est invitée à prouver un théorème spécifique (par exemple, « L'addition est commutative », ce qui signifie $a + b = b + a$ ).
Les Successeurs : En mathématiques réelles, une fois qu'un petit fait est prouvé, d'autres mathématiciens utilisent ce fait pour prouver des choses plus grandes et plus complexes. L'article examine tous les autres théorèmes qui dépendent de la réponse de l'IA.
Le Test : La réponse de l'IA est intégrée dans ces preuves « en aval ».
- Si l'IA a donné une réponse « fausse » (comme une tautologie toujours vraie mais sans utilité), les preuves en aval s'effondreront. Elles échoueront à se compiler car elles reposaient sur un sens spécifique que l'IA n'a pas fourni.
- Si l'IA a donné la bonne réponse, les preuves en aval s'exécuteront sans heurts.

La grande découverte
Les auteurs ont construit une vaste suite de tests utilisant 2 206 problèmes mathématiques réels issus du langage de programmation « Lean ». Ils ont testé 18 des modèles d'IA les plus intelligents disponibles (y compris des modèles de Google, OpenAI et Anthropic).

Voici ce qu'ils ont découvert, en utilisant notre analogie du pont :

Le piège de la « Grammaire » : La plupart des IA étaient excellentes pour passer l'ancien test. Elles écrivaient des plans qui semblaient parfaits et se compilaient sans erreurs. Sur l'ancien test, elles obtenaient environ 80 % de réussite.
Le test de réalité : Lorsque les auteurs ont appliqué le nouveau test d'« Intégration de la Ville », les scores ont chuté. La meilleure IA n'a obtenu environ que 39 % de bonnes réponses.
Le fossé : Cela signifie que pour chaque 100 ponts que l'IA prétendait construire, environ 60 s'effondreraient dès que quelqu'un essaierait de construire une route dessus. L'IA était bonne pour imiter l'apparence des mathématiques, mais mauvaise pour leur sens.

Pourquoi cela compte
L'article montre que les méthodes actuelles de mesure des compétences mathématiques des IA nous mentent.

Similarité lexicale (BLEU) : Vérifier si les mots de l'IA ressemblent aux mots humains est inutile. L'IA peut écrire du charabia qui ressemble à des mathématiques et passer quand même.
Modèles spécialisés : Même les modèles spécifiquement entraînés pour être des « experts en mathématiques » ne s'en sont pas beaucoup mieux sortis que les chatbots généraux. Ils sont simplement devenus meilleurs pour imiter la syntaxe.
La solution : La seule façon de savoir si une IA comprend vraiment les mathématiques est de voir si son travail tient bon lorsque d'autres preuves tentent de s'appuyer dessus.

En résumé
L'article introduit un nouveau « test de résistance » pour les mathématiques de l'IA. Il cesse de demander : « Cette phrase ressemble-t-elle à des mathématiques ? » et commence à demander : « Ces mathématiques fonctionnent-elles réellement lorsque nous essayons de les utiliser pour résoudre des problèmes plus grands ? » Le résultat est un test de réalité brutal : les meilleurs modèles d'IA d'aujourd'hui ont encore du mal à faire de vraies mathématiques significatives, même s'ils semblent les faire parfaitement.

1. Énoncé du problème

Les progrès rapides des grands modèles de langage (LLM) ont amélioré leur capacité à générer des preuves formelles dans des systèmes comme Lean. Cependant, les méthodes d'évaluation actuelles souffrent d'un défaut critique : elles confondent la validité syntaxique avec la correction sémantique.

La limitation de la compilation : Les benchmarks existants (par exemple, MiniF2F, ProofNet) évaluent principalement les modèles en vérifiant si un théorème généré compile. Bien que la compilation vérifie que le code est syntaxiquement valide et logiquement cohérent de manière isolée, elle ne garantit pas que le théorème capture le sens mathématique intended.
Le problème de la "tautologie" : Un modèle peut générer une tautologie triviale (par exemple, $a + b = a + b$ ) qui compile avec succès mais échoue à prouver l'énoncé non trivial visé (par exemple, la commutativité $a + b = b + a$ ).
L'insuffisance des proxies : Les tentatives existantes pour mesurer la correction sémantique reposent sur des proxies peu fiables tels que le chevauchement lexicique (scores BLEU) par rapport à des références annotées par des humains ou une inspection manuelle. Ces méthodes sont soit bruyantes, soit nécessitent un travail humain coûteux, soit échouent à distinguer les significations sémantiques correctes des incorrectes.

2. Méthodologie

Les auteurs proposent un changement de paradigme inspiré par les tests d'intégration en génie logiciel. Au lieu d'évaluer un théorème de manière isolée, ils l'évaluent en fonction de la manière dont il interagit avec le reste de la base de code.

Concept central : Test de théorème (T2)

S'appuyant sur la correspondance de Curry-Howard (où les preuves correspondent à des programmes), les auteurs traitent un théorème généré comme une fonction et les théorèmes qui en dépendent comme des "cas de test".

Graphe de dépendance : Ils construisent un graphe de dépendance où un théorème cible ( $t_{GT}$ ) possède des prédécesseurs (définitions/lemmes qu'il utilise) et des successeurs (théorèmes qui l'invoquent ou s'appuient sur lui).
Logique de test d'intégration : Si un théorème généré ( $t_{fl}$ ) est sémantiquement incorrect (par exemple, il définit une tautologie au lieu de la propriété visée), tout théorème successeur qui s'y fie échouera à compiler.
Analogie de l'élimination des coupes : Le processus est formellement ancré dans le principe logique de l'élimination des coupes. Si une chaîne de preuves ( $X \to Y \to Z \to W$ ) échoue lorsque le lemme intermédiaire ( $Y$ ) est remplacé par un candidat généré, le candidat est sémantiquement incorrect.

Le benchmark T2

Les auteurs ont construit un benchmark à grande échelle, T2, pour faciliter cette évaluation :

Source : Extrait de 5 dépôts Lean 4 réels (couvrant l'algèbre, la topologie, la théorie des nombres, etc.).
Échelle : 2 206 problèmes, chacun apparié à une moyenne de 41 théorèmes successeurs.
Sous-ensemble difficile : Un sous-ensemble de 389 problèmes "Hard" où le modèle doit générer à la fois la proposition (énoncé) et la preuve, plutôt que de simplement compléter une preuve pour un énoncé donné.
Automatisation : Le pipeline d'extraction est entièrement automatisé, ne nécessitant aucune annotation humaine pour la structure de dépendance. Les descriptions en langage naturel (NL) ont été générées par un LLM puissant (Claude Sonnet 4.5) et vérifiées manuellement sur un échantillon.

La métrique : Précision des tests (TA)

Le papier introduit la Précision des tests (TA) comme métrique d'évaluation principale :
$TA = E_{P \sim D} \left[ \prod_{i=1}^{k} \text{compiles}(t^{(i)}_{succ} \mid t_{fl}) \right]$
Un théorème généré ne passe que si tous ses théorèmes successeurs dépendants compilent avec succès lorsque le théorème original est remplacé par le généré.

3. Contributions clés

Benchmark T2 : Le premier benchmark à grande échelle, riche en dépendances, pour la preuve de théorèmes formels qui va au-delà des problèmes isolés pour atteindre des contextes de dépôts réels.
Précision des tests (TA) : Une métrique nouvelle, automatique et sans référence qui vérifie directement la correction sémantique par la compilation de modules dépendants.
Analyse de l'écart empirique : Évaluation complète de 18 modèles de pointe (à la fois open source et closed source) révélant un décalage massif entre le succès de la compilation et la correction sémantique.
Insights contextuels : Démonstration que fournir des théorèmes successeurs comme contexte améliore significativement la correction sémantique, tandis que fournir uniquement des preuves en langage naturel ne le fait pas.

4. Résultats expérimentaux

Les auteurs ont évalué 18 modèles (y compris GPT-5, Claude-Sonnet-4.5, Llama-3.1 et des modèles mathématiques spécialisés comme DeepSeek-Prover) sur le benchmark T2.

L'écart sémantique :
- Précision de compilation : Les modèles ont atteint des taux de compilation élevés (par exemple, Claude-Sonnet-4.5 : 80,3 % sur l'ensemble complet).
- Précision des tests (TA) : Les mêmes modèles ont obtenu des scores TA drastiquement plus faibles (par exemple, Claude-Sonnet-4.5 : 38,9 % sur l'ensemble complet ; 4,5 % sur l'ensemble Hard).
- Faux positifs : Jusqu'à 93,1 % des théorèmes compilables se sont révélés sémantiquement incorrects lorsqu'ils ont été testés contre les successeurs.
Échec des métriques existantes :
- BLEU : Une forte similarité lexicale (scores BLEU) n'a montré presque aucune corrélation avec la correction sémantique (Corrélation : 0,123). Les modèles pouvaient générer des preuves textuellement similaires mais logiquement erronées.
- Modèles spécialisés : Les modèles affinés spécifiquement pour la preuve de théorèmes ont souvent atteint des taux de compilation plus élevés mais ont performé plus mal ou de manière similaire aux modèles à usage général sur la TA, suggérant qu'ils surajustent à la syntaxe plutôt qu'à la sémantique.
Impact du contexte :
- Fournir des théorèmes successeurs comme contexte d'entrée a systématiquement amélioré la TA (par exemple, +4,9 % pour Claude-Sonnet-4.5).
- Fournir uniquement des preuves en NL sans successeurs n'a pas amélioré les performances et les a parfois dégradées.
- Le few-shot prompting et le raffinement itératif (utilisant les retours du compilateur) ont produit des améliorations négligeables sur l'ensemble Hard, indiquant que la difficulté réside dans le raisonnement sémantique profond, et non simplement dans le formatage de la tâche.

5. Signification et conclusion

Ce papier remet fondamentalement en question l'état actuel de l'évaluation de la preuve de théorèmes automatisée (ATP).

Redéfinition du succès : Il prouve que la "compilation" est une condition nécessaire mais insuffisante pour la génération de théorèmes. Un modèle peut être syntaxiquement parfait mais sémantiquement inutile.
Fiabilité : Le benchmark T2 et la métrique TA offrent un moyen rigoureux et automatique d'évaluer si un LLM comprend véritablement les concepts mathématiques ou s'il se contente d'halluciner un code syntaxiquement valide.
Orientation future : Le travail suggère que les futurs systèmes ATP doivent être évalués sur leur capacité à s'intégrer dans des bases de code existantes (génération consciente des dépendances) plutôt que sur la résolution de puzzles isolés. Il met également en évidence que fournir la "suite de tests" (théorèmes successeurs) au modèle pendant la génération est une stratégie cruciale pour améliorer l'alignement sémantique.

En résumé, le papier soutient que les tests d'intégration sont le maillon manquant dans l'évaluation des LLM pour les mathématiques formelles, révélant que les modèles actuels de pointe sont loin d'atteindre une correction sémantique fiable dans la preuve de théorèmes.