💻 computer science

Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation

L'article présente **Diffusion-Proof**, le premier cadre appliquant les grands modèles de langage basés sur la diffusion à la démonstration formelle de théorèmes, qui surpasse les bases traditionnelles autorégressives en exploitant le débruitage itératif pour la cohérence à longue portée et la correction locale, atteignant des améliorations significatives sur les benchmarks et résolvant un problème de l'IMO que les modèles de pointe n'avaient pas pu résoudre.

Auteurs originaux : Ruida Wang, Rui Pan, Pengcheng Wang, Shizhe Diao, Tong Zhang

Publié 2026-06-19

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Ruida Wang, Rui Pan, Pengcheng Wang, Shizhe Diao, Tong Zhang

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

L'Idée Générale : Réparer la « Rue à Sens Unique » des Mathématiques de l'IA

Imaginez que vous essayez de résoudre un casse-tête mathématique très complexe, comme une preuve dans un langage formel appelé Lean. Ce langage est comme un code informatique strict où chaque étape doit être logiquement parfaite. Si vous faites une seule petite erreur, toute la preuve s'effondre.

Pendant des années, les meilleurs modèles d'IA pour cette tâche ont été des modèles Auto-Régressifs (AR). Considérez ces modèles comme une personne écrivant une histoire un mot à la fois, strictement de gauche à droite. Ils ne peuvent pas voir ce qu'ils sont sur le point d'écrire, et ils ne peuvent pas facilement revenir en arrière pour changer un mot écrit il y a cinq minutes sans réécrire toute la phrase.

Le Problème :
Dans les preuves mathématiques longues, cette approche de « rue à sens unique » cause deux problèmes majeurs :

L'Effet Domino : Si l'IA commet une petite erreur au début, elle continue de construire sur cette erreur, aggravant le problème jusqu'à ce que la preuve ne soit plus que du charabia.
L'Impossibilité de « Regarder en Arrière » : Si l'IA se rend compte à mi-chemin que la première étape était fausse, elle ne peut pas facilement corriger uniquement cette première étape. Elle doit soit recommencer, soit essayer maladroitement de colmater la fin de la phrase pour qu'elle corresponde au début.

La Solution : L'Approche par « Diffusion »

Les auteurs de ce papier proposent une nouvelle façon de construire une IA pour les mathématiques appelée Diffusion-Proof. Au lieu d'écrire mot par mot, ils utilisent un Modèle de Langage de Diffusion (dLLM).

L'Analogie : Le Sculpteur vs Le Scribe

L'Ancienne Méthode (Modèle AR) : Imaginez un scribe écrivant une lettre. Une fois l'encre sèche, il ne peut plus la changer. S'il fait une faute d'orthographe, il doit la rayer et écrire une note désordonnée à côté.
La Nouvelle Méthode (Modèle de Diffusion) : Imaginez un sculpteur travaillant sur un bloc d'argile. Il ne se contente pas d'ajouter de l'argile ; il part d'un amas brut et bruité et le affine de manière itérative. Il peut regarder la forme globale à la fois, lisser une bosse sur le côté gauche tout en regardant la courbe sur le côté droit, et corriger les erreurs en « débruitant » l'ensemble de l'image jusqu'à ce qu'elle soit parfaite.

En termes techniques, le modèle de diffusion génère du texte par blocs (groupes de mots) plutôt que par mots isolés. Il peut regarder le début et la fin d'une phrase simultanément pour déterminer ce qui convient au milieu.

Comment fonctionne Diffusion-Proof : L'Équipe de Duo

Le papier introduit une équipe en deux parties pour résoudre ces problèmes mathématiques :

1. L'Architecte (dLLM-Prover-7B)

C'est le constructeur principal. Parce qu'il utilise la méthode du « sculpteur » (diffusion par blocs), il est bien meilleur pour la planification à longue portée.

Pourquoi c'est important : En construisant une preuve longue, l'Architecte peut voir la « vue d'ensemble ». Il sait que l'étape finale nécessite une condition spécifique, donc il prépare le début de la preuve pour qu'il corresponde parfaitement à cette condition. Il ne se perd pas au milieu car il peut « voir » tout le bloc de texte à la fois.

2. L'Inspecteur (dLLM-Corrector-7B)

Même le meilleur Architecte fait des erreurs. Parfois, la preuve semble correcte, mais une étape spécifique est erronée.

L'Ancienne Méthode : Si un modèle AR fait une erreur, il essaie souvent de la corriger en écrivant plus de texte après l'erreur, ce qui aggrave généralement la situation.
La Nouvelle Méthode : L'Inspecteur est un modèle spécial entraîné pour remplir les blancs. Si la preuve échoue, le système prend la partie défectueuse, la recouvre d'un « masque » (comme un espace vide) et demande à l'Inspecteur de réécrire juste ce bloc spécifique.
Le Superpouvoir : Parce que l'Inspecteur utilise la méthode de diffusion, il peut regarder le texte avant l'erreur et le texte après l'erreur pour comprendre exactement quelle pièce manquante doit s'y insérer. C'est comme un éditeur qui lit la phrase avant et la phrase après une faute de frappe pour deviner le mot correct, plutôt que de simplement deviner en se basant sur le mot précédent.

Les Résultats : Battre les Géants

Les chercheurs ont testé ce nouveau système sur deux benchmarks mathématiques célèbres :

MiniF2F : Une collection de problèmes de mathématiques de niveau lycée et de compétition.
ProofNet : Une collection de problèmes de mathématiques de niveau universitaire.

Le Tableau des Scores :

Le nouveau système Diffusion-Proof a battu les meilleurs modèles traditionnels (Auto-Régressifs) entraînés sur les mêmes données.
Il a résolu 6,14 % de problèmes en plus sur le test MiniF2F.
Il a résolu 1,61 % de problèmes en plus sur le test ProofNet.

Le Moment « IMO » :
Le résultat le plus excitant concerne un problème spécifique des Olympiades Internationales de Mathématiques (IMO). Un modèle d'IA très avancé et célèbre nommé DeepSeek-Prover-V2 (qui utilise le raisonnement par « Chaîne de Pensée » ou Chain of Thought) n'a pas réussi à résoudre ce problème. Diffusion-Proof l'a résolu.

Pourquoi ? Le modèle DeepSeek s'est retrouvé bloqué dans une boucle tentant de corriger son propre plan, car il ne pouvait pas percevoir la connexion à longue portée entre le début et la fin de la preuve. Le modèle de Diffusion, grâce à sa capacité à regarder l'ensemble du « bloc » de la preuve à la fois, a trouvé le chemin correct.

Résumé

Le papier affirme qu'en passant de « l'écriture d'un mot à la fois » à la « sculpture de blocs de texte », l'IA peut devenir bien meilleure en mathématiques formelles. Cela crée un système qui planifie mieux sur de longues distances et peut corriger ses propres erreurs en regardant l'ensemble du contexte, et non seulement le passé immédiat. Cela permet de résoudre des problèmes mathématiques difficiles que les modèles d'IA précédents ne pouvaient tout simplement pas résoudre.

Résumé Technique : Diffusion-Proof

Énoncé du Problème

La démonstration formelle de théorèmes nécessite de maintenir une cohérence à longue portée et une consistance logique à travers des séquences complexes de raisonnement. Bien que les modèles de langage à grande échelle (LLM) aient progressé de manière significative dans ce domaine, les approches de pointe actuelles reposent largement sur des modèles auto-régressifs (AR). Ces modèles génèrent du texte de manière séquentielle de gauche à droite, en prédisant le jeton suivant en se basant uniquement sur les jetons précédents. Cette architecture souffre de limitations intrinsèques, notamment :

Accumulation d'erreurs : De petites erreurs dans les premiers jetons peuvent se propager de manière exponentielle sur de longues séquences, menant à des incohérences logiques.
Manque de cohérence à longue portée : Les modèles AR peinent à maintenir un plan global cohérent pour une preuve, échouant souvent à aligner les tactiques intermédiaires avec l'objectif final.
Incapacité à effectuer du "in-filling" : Les modèles AR ne peuvent pas naturellement effectuer de corrections par "in-filling" (modifier une section centrale d'une preuve tout en préservant le contexte environnant), ce qui est crucial pour corriger des erreurs locales sans réécrire l'intégralité de la preuve.

Bien que les LLM de diffusion (dLLM) aient montré des promesses dans le codage et la génération de texte générale en utilisant le débruitage itératif et un contexte bidirectionnel, leur application au raisonnement mathématique formel reste largement inexplorée.

Méthodologie

Les auteurs proposent Diffusion-Proof, le premier cadre conçu pour entraîner et appliquer des dLLM spécifiquement pour la démonstration de théorèmes formels. Le cadre opère au sein de l'environnement Lean4 et utilise une architecture à double modèle : dLLM-Prover-7B et dLLM-Corrector-7B.

1. Collecte et Prétraitement des Données

Jeu de données : Les auteurs ont collecté 5,5 millions d'enregistrements de démonstration de théorèmes provenant de travaux antérieurs.
Nettoyage : Ils ont standardisé les données à l'aide de méthodes basées sur des règles pour séparer les énoncés en Langage Naturel (NL), les énoncés en Langage Formel (FL) et les preuves en FL.
Jeu de données SFT : 300 000 enregistrements ont été sélectionnés pour créer un jeu de données de réglage fin supervisé (SFT), maintenant un ratio de 1:2 entre les preuves Lean pures et celles avec annotations en langage naturel.
Données du Correcteur : Un sous-ensemble de données présentant une décomposition de sous-objectifs (marqués par des mots-clés have) a été traité. Les blocs de preuve ont été remplis de jetons de substitution (placeholders) pour créer des données d'entraînement pour les corrections par "in-filling".

2. Architecture du Modèle et Entraînement

Le cadre est construit sur Fast-dLLM-V2-7B, un modèle de diffusion basé sur des blocs. Contrairement aux dLLM traditionnels qui masquent les jetons de manière indépendante, ce modèle divise les séquences en blocs de taille $B$ avec une attention bidirectionnelle restreinte à chaque bloc, tout en préservant les relations causales entre les blocs.

dLLM-Prover-7B :
- Objectif : Effectuer la génération de la preuve complète avec une utilisation de tactiques cohérente à longue portée.
- Entraînement : Réglage fin sur le jeu de données SFT de 300k en utilisant un cadre texte-vers-texte standard.
- Stratégie : Emploie l'apprentissage par curriculum, organisant les données d'entraînement par complexité de preuve (augmentation de la longueur de la preuve) pour stabiliser la courbe de perte. La taille du bloc de diffusion est fixée à 32.
dLLM-Corrector-7B :
- Objectif : Effectuer la correction locale de preuves en utilisant l'information bidirectionnelle.
- Entraînement : Réglage fin sur le jeu de données de décomposition de sous-objectifs de 128k.
- Innovation : Introduit une méthode de Large Block Correction (Correction par Grand Bloc). La taille du bloc de diffusion est étendue de 32 à 512. Le modèle est entraîné pour remplacer les preuves de sous-objectifs erronées par une séquence de jetons masqués, puis pour régénérer le bloc en utilisant le contexte étendu (préfixe et suffixe) afin d'effectuer des corrections par in-filling.

3. Pipeline d'Inférence

Génération : Le dLLM-Prover-7B génère une preuve complète pour un énoncé de théorème donné en utilisant la génération par diffusion de blocs.
Vérification : La preuve est vérifiée par Lean.
Correction : Si la preuve échoue à la vérification mais que le squelette de haut niveau (énoncés de sous-objectifs) est correct, le dLLM-Corrector-7B est invoqué. Il remplace les preuves de sous-objectifs erronées par des jetons masqués et les régénère en utilisant un bloc de diffusion de 512 jetons, exploitant le contexte bidirectionnel pour corriger les erreurs locales tout en maintenant la cohérence globale.

Principales Contributions

Premier cadre dLLM pour la démonstration de théorèmes : Diffusion-Proof est le premier cadre adaptant les modèles de diffusion pour la démonstration de théorèmes formels, répondant aux défis spécifiques de la cohérence à longue portée et de la correction d'erreurs dans le raisonnement mathématique.
Entraînement par Large Block Correction : Les auteurs introduisent une nouvelle méthode d'entraînement qui exploite de grands blocs de diffusion (512 jetons) et l'information bidirectionnelle pour permettre des corrections par in-filling efficaces, une capacité native aux modèles de diffusion mais absente des modèles AR.
Synergie de Double Modèle : Le cadre démontre une approche synergique où un prouveur gère la planification globale et un correcteur gère le raffinement local, surpassant les bases à modèle unique.

Résultats Expérimentaux

Le cadre a été évalué sur MiniF2F-Test (244 problèmes) et ProofNet-Test (186 problèmes) en utilisant la métrique pass@32.

Gains de Performance : Comparé à un modèle de base AR (Qwen-2.5-Lean-SFT-7B) entraîné sur le même jeu de données :
- MiniF2F-Test : Diffusion-Proof a atteint 50,00 % de précision, soit une amélioration absolue de 6,14 % par rapport à la base (43,85 %).
- ProofNet-Test : Diffusion-Proof a atteint 7,53 % de précision, soit une amélioration absolue de 1,61 % par rapport à la base (5,91 %).
Analyse par Type de Problème : Le modèle a montré des gains significatifs dans les catégories difficiles, particulièrement les problèmes de l'IMO (Olympiades Internationales de Mathématiques), où il est passé de 5,00 % à 15,00 %.
Étude de Cas : Notamment, Diffusion-Proof a réussi à résoudre le problème IMO imo_1962_p2, que le modèle plus avancé DeepSeek-Prover-V2-7B (équipé de raisonnement Long Chain-of-Thought) n'a pas pu résoudre sous pass@32. L'analyse a indiqué que le modèle AR peinait avec les dépendances à longue portée et la planification de tactiques cohérentes requises, tandis que le correcteur de diffusion a utilisé avec succès le contexte bidirectionnel pour résoudre la preuve.
Études d'Ablation :
- Le retrait du correcteur a réduit la performance de 1,64 % sur MiniF2F, confirmant la valeur de l'étape de correction.
- Même sans le correcteur, le dLLM-Prover seul a surpassé la base AR de 4,51 %, validant l'avantage inhérent de l'architecture de diffusion pour le raisonnement formel.

Signification et Revendications

L'article affirme que Diffusion-Proof met en évidence les avantages uniques des modèles de diffusion dans la démonstration de théorèmes formels, spécifiquement leur capacité à maintenir une cohérence à longue portée et à effectuer des corrections par in-filling bidirectionnel.

Avantage Architectural : Les résultats suggèrent que le paradigme de génération par diffusion offre un avantage structurel par rapport aux modèles AR pour les tâches exigeant une consistance logique rigoureuse sur de longues séquences, comme en témoignent les distributions de perte de validation plus faibles et les taux de réussite plus élevés sur les preuves complexes.
Potentiel Futur : Les auteurs positionnent ce travail comme une étape fondamentale, démontant que les dLLM peuvent surpasser les bases AR même sans Apprentissage par Renforcement (RL) ou raisonnement Long CoT. Ils notent que bien que les limites actuelles incluent l'échelle de calcul et l'absence d'intégration du RL, le cadre offre une direction prometteuse pour la recherche future sur les modèles dotés de capacités de raisonnement améliorées.

Les auteurs soulignent que leur objectif principal était d'étudier le potentiel architectural des dLLM plutôt que d'atteindre des performances de pointe par un passage à l'échelle massive ou le RL, faisant des améliorations observées un indicateur fort de l'efficacité du paradigme de diffusion pour le raisonnement formel.