🤖 AI

Formally Solving Answer-Construction Problems in Lean

Cet article introduit ECP, un cadre neuro-symbolique dans Lean qui combine des LLM généraux assistés par des outils pour énumérer des réponses candidates avec des LLM de preuve pour générer des preuves vérifiées par machine, comblant ainsi efficacement l'écart dans la résolution formelle de problèmes mathématiques de construction de réponses.

Auteurs originaux : Jialiang Sun, Yuzhi Tang, Ao Li, Chris J. Maddison, Kuldeep S. Meel

Publié 2026-06-02

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Jialiang Sun, Yuzhi Tang, Ao Li, Chris J. Maddison, Kuldeep S. Meel

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 participiez à un concours de mathématiques très difficile. Il y a deux types de questions auxquelles vous pourriez être confronté :

La question « Prouvez-le » : Le juge vous donne une affirmation comme « Le ciel est bleu » et vous demande : « Pouvez-vous prouver que c'est vrai ? » Vous devez simplement rédiger un argument logique.
La question « Construisez-le » : Le juge vous demande : « Trouvez le plus petit nombre qui satisfait ces règles étranges. » Vous devez d'abord inventer le nombre, puis prouver qu'il fonctionne.

Ce document traite de ce second type : la Construction de Réponse (Answer-Construction). C'est la différence entre être un avocat qui argumente un cas connu et être un architecte qui doit concevoir un bâtiment à partir de zéro avant de prouver qu'il ne s'effondrera pas.

Le Problème : Un décalage d'outils

Les auteurs ont remarqué une lacune dans la manière dont l'Intelligence Artificielle (IA) gère ces tâches.

L'IA Générale (Le « Grand Cerveau ») : Considérez cela comme un professeur brillant et bavard. Il est excellent pour le brainstorming, deviner des nombres ou faire des calculs approximatifs. Mais si vous lui demandez d'écrire une preuve formelle et parfaite pour une machine, il devient souvent paresseux, invente des faits ou écrit du code qui ne compile pas. Il est aussi très coûteux à embaucher.
L'IA de Preuve (L'« Éditeur Strict ») : Considérez cela comme un petit robot hyper-focalisé, entraîné uniquement à écrire des preuves formelles. Il est bon marché et excellent pour vérifier la logique, mais il est incapable de deviner quelle pourrait être la réponse. Si vous lui demandez de « Trouver le nombre », il pourrait simplement fixer le mur ou deviner un nombre au hasard qui ne fonctionne pas.

Le Piège :
Si vous demandez simplement à l'« Éditeur Strict » de résoudre un problème de type « Construisez-le », il pourrait tricher. Il pourrait dire : « La réponse est "le plus petit nombre qui satisfait les règles". » Techniquement, c'est une réponse valide aux yeux d'un ordinateur, mais dans un vrai concours de mathématiques, c'est une triche circulaire. Vous avez besoin d'un nombre spécifique, comme 245. L'ordinateur doit être forcé d'arrêter de tricher et de réellement trouver le vrai nombre.

La Solution : ECP (Énumérer-Conjecturer-Prouver)

Les auteurs ont construit un nouveau système appelé ECP (Énumérer-Conjecturer-Prouver). Il agit comme une équipe de trois personnes travaillant ensemble pour résoudre ces problèmes de type « Construisez-le » dans un langage appelé Lean (un assistant de preuve informatique).

Voici comment l'équipe travaille, en utilisant une analogie de détective :

1. Le Détective (L'IA Générale + Outils Python)

Rôle : C'est le professeur au « Grand Cerveau », mais cette fois, il possède une calculatrice et un ordinateur pour exécuter du code.
Action : Au lieu de simplement deviner, le Détective écrit un programme Python pour chercher des indices par force brute. Il exécute des boucles pour tester des milliers de petits nombres afin de voir lesquels respectent les règles.
La « Conjecture » : Sur la base des données, le Détective fait une supposition éduquée : « Je parie que la réponse est 245. » Il rédige son raisonnement en langage courant.

2. Le Gardien (Le Vérificateur d'Admissibilité)

Rôle : C'est le videur à l'entrée du club.
Action : Avant que la conjecture du Détective ne soit autorisée à progresser, le Gardien la vérifie.
- Est-ce un vrai nombre ? (Oui, 245 est un nombre).
- Est-ce de la triche ? (Le Détective a-t-il simplement dit « la réponse est la réponse » ? Non.)
- Utilise-t-il des mots interdits ? (A-t-il utilisé des symboles mathématiques complexes qui ne sont pas autorisés dans le concours ? Non.)
Si la conjecture échoue à ce contrôle, le Gardien la renvoie au Détective pour qu'il essaie à nouveau.

3. Le Juge (L'IA de Preuve + Automatisation Lean)

Rôle : C'est le robot « Éditeur Strict ».
Action : Une fois que le Gardien a approuvé la conjecture (245), le Juge prend le relais. Le Juge ignore la partie « comment nous l'avons trouvé » et se concentre entièrement sur la partie « pourquoi c'est vrai ». Il utilise la logique formelle pour prouver, au-delà de tout doute, que 245 est bien la bonne réponse.
Si la preuve échoue, le Juge le renvoie au Détective pour qu'il essaie un autre nombre.

Les Résultats : Cela a-t-il fonctionné ?

Les auteurs ont testé cette équipe sur deux ensembles de données mathématiques célèbres : PutnamBench (mathématiques de niveau universitaire) et MathArena (compétitions de niveau lycée comme l'AIME).

L'Ancienne Méthode : Si vous demandiez simplement à l'« Éditeur Strict » de résoudre ces problèmes, il échouait la plupart du temps ou trichait en donnant des réponses circulaires. Si vous demandiez au « Grand Cerveau » de tout faire, il restait bloqué sur la partie de la preuve formelle.
La Méthode ECP : En divisant le travail, le système a résolu 17 des 346 problèmes universitaires difficiles et 18 des 75 problèmes de niveau lycée.
Pourquoi c'est important : Il ne s'agit pas seulement d'obtenir le bon nombre ; il s'agit d'obtenir une preuve vérifiée par machine qui démontre que le nombre est correct et que la réponse n'est pas une triche.

Résumé

Voyez l'ECP comme une chaîne de montage d'usine pour les problèmes mathématiques :

Le Travailleur A (IA Générale) utilise des outils pour creuser à la recherche de la réponse.
L'Inspecteur B (Le Gardien) s'assure que la réponse est un nombre réel et non une triche.
Le Travailleur C (IA de Preuve) construit le pont de logique incassable pour prouver que ce nombre est correct.

Cette approche comble le fossé entre « deviner la réponse » et « prouver la réponse », permettant à l'IA de résoudre des problèmes mathématiques qui nécessitent à la fois de la créativité et une logique rigoureuse.

Résumé Technique : Résoudre Formellement les Problèmes de Construction de Réponses dans Lean

Définition du Problème
Les problèmes de compétition mathématique se divisent généralement en deux catégories : la démonstration de théorèmes (vérifier un énoncé donné) et la construction de réponses (construire un objet spécifique satisfaisant une propriété). Bien que les progrès récents des grands modèles de langage (LLM) aient considérablement amélioré la démonstration formelle de théorèmes, la construction formelle de réponses reste sous-explorée. Un écart critique existe entre les systèmes de raisonnement informels, qui sont forts pour conjecturer mais faibles pour la vérification formelle, et les LLM de preuve formelle, qui sont optimisés pour les preuves mais peinent à découvrir les témoins nécessaires pour éliminer les quantificateurs existentiels.

Un défi spécifique de la formalisation de la construction de réponses est l'admissibilité. Les vérificateurs de preuves Lean standards vérifient qu'un terme de preuve possède le bon type, mais n'imposent pas intrinsèquement que le témoin construit soit une réponse canonique et sous forme close. Par exemple, une preuve peut satisfaire un énoncé existentiel $\exists x, P(x)$ en retournant un terme non canonique comme sInf PropertySet (l'infimum de l'ensemble défini) plutôt qu'un nombre naturel explicite (par exemple, 245). De tels témoins « circulaires » ou non sous forme close sont mathématiquement valides au sein de la logique, mais inadmissibles en tant que réponses de concours.

Méthodologie : Énumération-Conjecture-Preuve (ECP)
Pour relever ces défis, les auteurs introduisent Énumération-Conjecture-Preuve (ECP), un cadre neuro-symbolique conçu pour la construction de réponses de bout en bout avec des preuves formelles dans Lean 4. ECP sépare le processus en étapes distinctes tout en maintenant une boucle de vérification formelle :

Formalisation du Problème et Vérification de l'Admissibilité :
- Les problèmes sont formalisés comme des tâches de synthèse fonctionnelle : trouver une fonction $\Psi$ telle que $\forall X, P(X) \to Q(X, \Psi(X))$ .
- Un vérificateur d'admissibilité est implémenté pour s'assurer que la réponse synthétisée n'utilise qu'un « vocabulaire admissible » prédéfini (par exemple, des constantes spécifiques, des opérateurs arithmétiques et des constructeurs standards). Il extrait structurellement les constantes sémantiques du terme Lean et filtre les constantes administratives (comme les instances de classes de types ou les artefacts générés par le compilateur) ainsi que les définitions non canoniques (comme sInf).
Étape d'Énumération (Exploration assistée par outils) :
- Un LLM généraliste (par exemple, GPT-5.4) est doté de capacités d'exécution d'outils Python.
- Le LLM écrit et exécute du code Python pour effectuer une énumération bornée sur de petits domaines afin de trouver des tuples satisfaisant les contraintes du problème.
- Ces traces d'exécution servent de preuves empiriques pour identifier des motifs, des invariants et des formes fonctionnelles.
Étape de Conjecture (Synthèse de la Réponse) :
- En utilisant les preuves de l'étape d'Énumération, le même LLM généraliste synthétise une fonction de réponse candidate $\Psi'$ .
- La candidate est soumise à deux filtres avant de procéder :
  - Vérification Syntaxique : Le terme doit compiler dans Lean avec le type correct.
  - Vérification d'Admissibilité : Le terme ne doit utiliser que des constantes issues du vocabulaire autorisé.
- Si une candidate échoue, le système itère en incluant le message d'erreur dans le prompt.
Étape de Preuve (Vérification Formelle) :
- Une fois une candidate $\Psi'$ valide construite, le système tente de prouver le théorème instancié $Stmt(T)|_{\Psi=\Psi'}$ .
- Boucle de Réfutation : Avant de tenter une preuve, le système tente de réfuter la candidate en prouvant la négation. Si la réfutation réussit, la candidate est rejetée et le système revient à l'étape de Conjecture.
- Génération de Preuve : Si la réfutation échoue, le système tente de prouver l'énoncé positif en utilisant une combinaison de l'automatisation intégrée de Lean (tactiques comme simp, aesop, ring, norm_num) et d'un LLM de preuve spécialisé (par exemple, Goedel-Prover-V2). Si l'automatisation échoue, le LLM de preuve est invoqué avec une boucle de réparation pour générer ou corriger la preuve.

Contributions Clés

Cadre pour la Construction de Réponses : ECP est le premier cadre qui sépare explicitement la construction de la réponse de la génération de la preuve tout en imposant des contraintes d'admissibilité dans une boucle de vérification formelle.
Imposition de l'Admissibilité : L'article introduit une méthode structurelle pour filtrer les témoins non canoniques (ex: définitions circulaires) que les vérificateurs Lean standards accepteraient autrement, garantissant que la sortie correspond aux exigences des concours.
Intégration Neuro-Symbolique : Le cadre combine efficacement le raisonnement exploratoire des LLM généraux avec l'exécution d'outils Python et les capacités de preuve rigoureuses des LLM de preuve spécialisés.
Benchmarks et Autoformalisation : Les auteurs ont auto-formalisé 75 problèmes des compétitions de réponses finales MathArena 2026 (AIME, HMMT, APEX) et 346 problèmes de construction de réponses de PutnamBench, créant une nouvelle norme d'évaluation pour ce type de problème.

Résultats Expérimentaux
Le système a été évalué sur MathArena 2026 (75 problèmes) et PutnamBench (346 problèmes) par rapport à des bases de référence incluant des LLM de génération de preuve directe (GPT-5.4, Goedel-Prover-V2).

Performance de Bout en Bout : ECP a surpassé les bases de référence de génération de preuve directe.
- MathArena : ECP a résolu 18/75 problèmes (Pass@32), contre 13/75 pour la meilleure base de référence LLM seule (GPT-5.4).
- PutnamBench : ECP a résolu 17/346 problèmes (Pass@32), contre 8/346 pour GPT-5.4 et 7/346 pour Goedel-Prover-V2-32B.
Précision de la Réponse Seule : La construction de réponses assistée par outils a considérablement amélioré la précision des LLM généraux dans la génération de candidates correctes. Pour GPT-5.4, l'utilisation d'outils a augmenté la construction de réponses correctes sur PutnamBench de 290/346 à 303/346.
Impact de l'Admissibilité : L'analyse a révélé que beaucoup de preuves générées par les bases de référence étaient compilables dans Lean mais contenaient des réponses inadmissibles (ex: témoins circulaires). Le contrôle d'admissibilité explicite d'ECP a été crucial pour les filtrer.
Études d'Ablation :
- Supprimer l'étape de correction par le LLM de preuve a réduit la performance sur MathArena (18 $\to$ 16) et PutnamBench (17 $\to$ 16).
- Supprimer l'automatisation de Lean a eu un impact sévère sur MathArena (18 $\to$ 11) mais moins sur PutnamBench lors de l'exécution spécifique, suggérant que les problèmes de MathArena dépendent davantage des tactiques d'automatisation tandis que PutnamBench repose davantage sur la capacité du prouveur.
- L'utilisation d'un prouveur plus petit (8B) a maintenu la performance de MathArena mais a considérablement fait chuter les résultats de PutnamBench (17 $\to$ 7), indiquant que les problèmes de Putnam sont plus limités par la recherche de preuve.

Signification et Revendications
L'article affirme qu'ECP parvient à combler le fossé entre la génération de réponses informelles et la démonstration de théorèmes formelle. En gérant explicitement la phase de « construction de réponse » et en imposant l'admissibilité, ECP résout des instances qui sont actuellement insolubles pour les approches de génération de preuve directe. Les auteurs soulignent que leur approche est particulièrement efficace pour les problèmes nécessitant la construction d'un témoin spécifique (quantification existentielle) plutôt que la simple vérification d'une conclusion fixe.

Ce travail met en évidence le fait que les benchmarks formels actuels omettent souvent la difficulté de la construction de réponses, se concentrant plutôt sur les versions de problèmes « avec réponse ». ECP démontre que combiner les LLM généraux avec l'exécution d'outils pour l'énumération, suivis de LLM de preuve spécialisés pour la vérification, est une voie viable pour résoudre des problèmes mathématiques complexes et ouverts dans les systèmes formels. Les auteurs notent les limites concernant la nature heuristique de l'étiquetage du vocabulaire admissible et le potentiel d'explosion combinatoire dans l'étape d'énumération pour les problèmes de combinatoire très complexes.