💬 NLP

Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving

L'article présente KG-prover, un cadre novateur qui enrichit les modèles de langage de grande taille à usage général avec des graphes de connaissances extraits de textes mathématiques pour améliorer la preuve automatique de théorèmes, démontrant des gains de performance significatifs sur plusieurs jeux de données sans nécessiter de réglage fin supplémentaire.

Auteurs originaux : Vincent Li, Tim Knappe, Yule Fu, Kevin Han, Kevin Zhu

Publié 2026-05-26

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Vincent Li, Tim Knappe, Yule Fu, Kevin Han, Kevin Zhu

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

La Grande Idée : Offrir aux Modèles Mathématiques un « Copier-Coller »

Imaginez que vous essayez de résoudre une énigme mathématique très difficile. Vous avez un ami super-intelligent (un Modèle de Langage, ou LLM) qui connaît beaucoup de mathématiques, mais qui parfois reste bloqué parce qu'il ne se souvient pas d'une règle spécifique ou ne voit pas comment relier deux idées différentes.

Habituellement, pour rendre ces amis plus intelligents, il faut les renvoyer à l'école pendant des années de formation (fine-tuning). Cet article dit : « Pas besoin d'école supplémentaire ! » Au lieu de cela, nous pouvons simplement leur donner une meilleure carte et une meilleure bibliothèque pendant qu'ils travaillent sur le problème.

Les auteurs ont construit un système appelé KG-Prover. C'est comme donner à votre ami intelligent un immense réseau interconnecté de faits mathématiques (un Graphes de Connaissances) et lui permettre de « consulter » les bons indices en temps réel tandis qu'il tente de résoudre l'énigme.

Comment Ça Marche : L'Analogie du Détective

Imaginez l'IA comme un détective essayant de résoudre un crime (le théorème mathématique).

La Scène du Crime (Le Problème) : Le détective reçoit une affirmation qu'il doit prouver vraie.
La Bibliothèque (Le Graphe de Connaissances) : Les auteurs ont construit une bibliothèque massive à partir de ProofWiki (un site web rempli de preuves mathématiques). Ils ont transformé cette bibliothèque en une immense toile d'araignée où chaque concept mathématique est un nœud, et les lignes qui les relient montrent leurs relations (par exemple, « Le Théorème A utilise la Définition B »).
L'Enquête (La Recherche) :
- Au lieu de deviner, le détective observe la toile d'araignée.
- Il commence à la scène du crime et demande : « Qui est lié à cela ? »
- Il suit les lignes pour trouver des concepts similaires, des définitions et des preuves antérieures.
- S'il reste bloqué, il ne renonce pas ; il va plus profondément dans la toile, suivant davantage de lignes pour trouver des indices cachés. C'est ce qu'on appelle « l'augmentation du calcul au moment du test » — essentiellement, passer plus de temps et d'efforts pendant l'enquête pour trouver la réponse.
Le Brouillon (Preuve Informelle) : Le détective rédige un brouillon de la solution en anglais courant (langage naturel), en utilisant les indices qu'il a trouvés.
La Traduction (Formalisation) : Un traducteur spécialisé (une autre IA) prend ce brouillon en anglais et le transforme en code strict, lisible par ordinateur (Lean 4).
Le Juge (Vérification) : Un arbitre strict vérifie le code. S'il est erroné, le détective reçoit un indice sur ce qui a mal tourné, retourne à la toile d'araignée, trouve un nouvel indice, et réessaie.

Le « Truc » Qui Fonctionne

L'article affirme qu'en effectuant ce processus de « recherche et récupération », ils n'ont pas eu besoin de réentraîner les modèles d'IA. Ils ont simplement utilisé des modèles existants à usage général (comme GPT-4o-mini ou Llama 3) et leur ont permis d'utiliser la carte.

Les Résultats :

Meilleures Notes : Lorsqu'ils ont ajouté cette « carte en toile d'araignée », le taux de réussite de l'IA sur les problèmes mathématiques a augmenté de manière significative (de 2 % à 21 % selon le test).
L'Effet « Plongée Profonde » : Plus l'IA avait la permission de chercher plus profondément dans le graphe (en suivant davantage de connexions), mieux elle devenait à résoudre des problèmes difficiles. C'est comme dire : « Si tu ne peux pas résoudre cela en une minute, prends dix minutes et examine chaque livre connexe dans la bibliothèque. »
Pas de Formation Supplémentaire : Le plus grand avantage est qu'ils n'ont pas eu à dépenser des millions de dollars pour entraîner un nouveau modèle. Ils ont simplement donné aux anciens modèles un meilleur outil à utiliser pendant qu'ils travaillaient.

Les Limites (Où le Détective Reste Bloqué)

L'article est honnête sur les endroits où cette méthode échoue :

Le Fossé de Traduction : Parfois, le détective écrit une explication parfaite en anglais, mais le traducteur se trompe en la transformant en code strict. La logique mathématique était juste, mais la « grammaire » du langage informatique était fausse.
Indices Manquants : Si la réponse nécessite un fait mathématique très obscur qui ne se trouve pas dans leur bibliothèque (ProofWiki), le détective ne peut pas le trouver, peu importe la profondeur de sa recherche.
Trop de Bruit : Si la toile d'araignée est trop désordonnée, le détective peut se confondre avec des informations non pertinentes.

Résumé

Cet article présente un moyen de rendre les experts en mathématiques de l'IA plus intelligents sans les réentraîner. C'est comme donner à un étudiant génial un smartphone avec une encyclopédie parfaite et interconnectée et lui dire : « Prends ton temps, consulte chaque fait connexe dont tu as besoin, et écris la preuve. » En laissant l'IA « réfléchir plus fort » et chercher plus profondément dans son graphe de connaissances pendant le test, elle résout plus de problèmes correctement.

Résumé technique : Mise à l'échelle du calcul au moment de l'exécution basé sur des graphes en langage naturel pour la preuve de théorèmes automatisée

Énoncé du problème

Bien que les grands modèles de langage (LLM) aient démontré des capacités en raisonnement logique multi-étapes, la preuve de théorèmes automatisée reste un défi. Les obstacles spécifiques incluent l'identification précise des concepts mathématiques clés, la compréhension de leurs interrelations et la formalisation correcte des preuves au sein de langages naturels ou de systèmes formels. Les approches existantes reposent souvent sur un fine-tuning intensif, une itération par des experts ou un entraînement sur de grands volumes de données formelles (par exemple, Lean), ce qui peut être lourd en ressources et limiter la capacité du modèle à exploiter des connaissances mathématiques plus larges et informelles. De plus, les approches purement formelles peuvent peiner avec la flexibilité du raisonnement naturel, tandis que les approches purement en langage naturel font face à l'ambiguïté lors de la traduction vers des systèmes de vérification formelle.

Méthodologie : KG-Prover

Les auteurs introduisent KG-Prover, un cadre novateur qui enrichit les LLM à usage général avec un graphe de connaissances (KG) extrait de textes mathématiques réputés (spécifiquement ProofWiki) pour construire et formaliser des preuves. Le système fonctionne sans fine-tuning supplémentaire du LLM de base, s'appuyant plutôt sur la mise à l'échelle du calcul au moment de l'exécution et la génération augmentée par récupération.

Composants principaux

Construction du graphe de connaissances :
- Source : Le graphe est construit en analysant ProofWiki, en extrayant des nœuds depuis des espaces de noms tels que « Définition », « Axiome » et « Preuve ».
- Structure : Chaque nœud représente une assertion mathématique autonome (par exemple, une proposition de théorème ou une définition). Les arêtes représentent les hyperliens trouvés dans le texte, capturant les dépendances et les relations conceptuelles.
- Échelle : Le graphe résultant contient plus de 60 000 nœuds et 300 000 arêtes.
- Embeddings : Les nœuds sont enrichis de vecteurs d'embedding pré-calculés (utilisant text-embedding-3-large) pour faciliter la récupération sémantique.
Pipeline d'inférence :
- Récupération et parcours : Étant donnée une proposition $P$ , le système calcule son embedding et récupère les $k$ nœuds les plus similaires. Si la tentative de preuve initiale échoue, le système étend itérativement le contexte en parcourant le graphe jusqu'à une profondeur $d$ , en sélectionnant les $k$ voisins les plus pertinents des nœuds précédemment visités.
- Génération de preuve informelle : Le LLM génère une preuve informelle en langage naturel en utilisant le contexte récupéré. Cela exploite les capacités de raisonnement émergentes du modèle et le vaste corpus de preuves informelles disponibles dans le KG.
- Autoformalisation : Un modèle distinct (DeepSeek-Prover-V1.5) traduit la preuve informelle en code Lean 4.
- Vérification et raffinement : Le code Lean généré est vérifié à l'aide du prouveur de théorèmes Lean 4. Si la vérification échoue, les messages d'erreur sont renvoyés à l'autoformalisateur pour raffinement. Si la preuve échoue toujours, le système peut augmenter la profondeur de parcours du graphe ou employer des stratégies de recherche.
Stratégies de mise à l'échelle (calcul au moment de l'exécution) :
- Best-of-N : Le système génère $n$ preuves informelles indépendantes, les autoformalise, et utilise un modèle « juge » dédié pour les noter en fonction de leur exactitude et de leur clarté, sélectionnant le candidat le mieux noté.
- Recherche en faisceau (Beam Search) : Les candidats de preuve sont organisés dans un faisceau de largeur $w$ . À chaque étape, les candidats sont étendus en fonction des retours du vérificateur, notés, et les $k$ meilleurs sont conservés pour l'itération suivante. Cela équilibre l'exploration de diverses voies de preuve avec un raffinement guidé par la vérification.

Contributions clés

Cadre KG-Prover : Un système qui intègre la génération de preuves informelles en langage naturel avec un parcours itératif basé sur un graphe de connaissances et un mécanisme de LLM en tant que juge, éliminant le besoin d'un entraînement spécialisé ou d'une itération par des experts.
KG mathématique à grande échelle : La construction d'un graphe de connaissances à partir de ProofWiki avec plus de 60 000 nœuds et 300 000 arêtes, modélisant des relations complexes entre les concepts mathématiques.
Système de raffinement itératif : Une évaluation heuristique et un mécanisme de recherche en faisceau qui améliorent les performances jusqu'à 26,4 % par rapport aux lignes de base et de 21,8 % par rapport aux configurations KG-Prover sans mise à l'échelle.
Démonstration de la mise à l'échelle au moment de l'exécution : Des preuves indiquant que la modulation de la profondeur de parcours du graphe et l'emploi de stratégies de recherche (Best-of-N, Recherche en faisceau) augmentent considérablement les performances sans réentraîner les modèles sous-jacents.

Résultats expérimentaux

Le cadre a été évalué sur trois benchmarks : miniF2F-test, ProofNet et MUSTARDSAUCE.

Gains de performance :
- KG-Prover a systématiquement surpassé les systèmes de référence et la génération augmentée par récupération (RAG) standard sur tous les jeux de données.
- Les améliorations variaient de 2 % à 11 % par rapport aux lignes de base sur plusieurs modèles (Llama 3.1 8B, GPT-4o, o1-mini, etc.).
- Sur miniF2F-test, les LLM à usage général ont vu leurs performances augmenter jusqu'à 21 % lorsqu'ils étaient combinés avec KG-Prover.
- La configuration de KG-Prover avec o4-mini a atteint un taux de réussite de 50 % sur miniF2F-test.
- Dans la configuration de mise à l'échelle la plus élevée, les améliorations ont atteint 26,4 % par rapport aux lignes de base.
Effets de la mise à l'échelle :
- Profondeur de parcours : La précision a augmenté avec une profondeur de parcours ( $r$ ) plus grande, en particulier pour les modèles à plus petits paramètres comme Llama 3.1 8B. Les premières augmentations de profondeur ont produit les gains les plus significatifs.
- Stratégies de recherche : La combinaison du KG avec la recherche en faisceau et l'échantillonnage Best-of-N a encore amélioré la précision, atteignant jusqu'à 10,75 % sur ProofNet et 50,40 % sur MUSTARDSAUCE.
- Modèles fine-tunés : Même lorsqu'appliqués à des modèles déjà fine-tunés pour Lean (par exemple, TheoremLlama, DeepSeek-Prover-V1.5), KG-Prover a fourni des gains de performance supplémentaires (par exemple, +1,85 % par rapport à une ligne de base fine-tunée sur miniF2F).

Importance et affirmations

L'article postule que KG-Prover offre une approche prometteuse et évolutive pour la preuve de théorèmes automatisée qui ne nécessite ni fine-tuning supplémentaire ni itération intensive par des experts. En exploitant les capacités de raisonnement en langage naturel intégrées des LLM à usage général et en les enrichissant d'informations structurées récupérées via un graphe, le cadre comble efficacement le fossé entre le raisonnement informel et la vérification formelle.

Les auteurs soulignent que cette méthode permet aux modèles de base existants d'atteindre des performances comparables ou supérieures à celles des systèmes spécialisés et fine-tunés, simplement en injectant des concepts connexes lors de l'inférence. Le travail met en évidence le potentiel de la mise à l'échelle du calcul au moment de l'exécution — la modulation de la profondeur de parcours du graphe et l'emploi de stratégies de recherche — comme alternative viable à la mise à l'échelle des paramètres du modèle pour des tâches de raisonnement complexes. Bien que l'approche introduise des défis dans l'étape de traduction informel-vers-formel, le système à deux agents (génération + autoformalisation) soutenu par la récupération de graphes atténue avec succès ces problèmes, fournissant des traces de raisonnement interprétables et de nouvelles stratégies pour la génération de preuves.