💬 NLP

DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems

Le papier présente DRIFT, un nouveau cadre qui améliore la formalisation automatique des énoncés mathématiques par les modèles de langage en les décomposant en sous-composantes pour un ciblage précis des prérequis et l'ajout d'exemples illustratifs, surpassant ainsi les méthodes de récupération baselines sur plusieurs benchmarks.

Auteurs originaux : Meiru Zhang, Philipp Borchert, Milan Gritta, Gerasimos Lampouras

Publié 2026-04-08

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Meiru Zhang, Philipp Borchert, Milan Gritta, Gerasimos Lampouras

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

🧠 DRIFT : Le Guide de Voyage pour les Mathématiques

Imaginez que vous voulez construire une maison très complexe (un théorème mathématique) en utilisant des briques très précises et une langue très stricte appelée Lean (le langage des ordinateurs pour les maths).

Le problème, c'est que les grands modèles de langage (les IA) sont comme des architectes géniaux qui parlent très bien le français ou l'anglais, mais qui ne connaissent pas bien les règles de construction de la maison Lean. Ils savent ce qu'est un "mur", mais ils ne savent pas exactement comment appeler la brique "mur" dans le manuel de construction officiel (la bibliothèque Mathlib), ni comment l'assembler sans que tout s'effondre.

Jusqu'à présent, on demandait à l'IA : "Voici la maison, trouve-moi les plans !". L'IA cherchait dans la bibliothèque, mais elle se perdait souvent car la demande était trop vague ou trop complexe.

DRIFT est une nouvelle méthode qui change la donne. Au lieu de demander tout d'un coup, elle utilise une stratégie en 4 étapes, comme un guide touristique très organisé.

🗺️ Les 4 Étapes de DRIFT (Le Voyage)

1. DÉCOMPOSER (Decompose) : Le Chef d'Orchestre

Au lieu de donner à l'IA une phrase mathématique géante et confuse (ex: "Montrer que si p est un nombre premier de forme 4t+3, alors..."), DRIFT lui dit : "Arrête-toi ! Découpe cette phrase en petits morceaux."

L'analogie : Imaginez que vous devez cuisiner un gâteau complexe. Au lieu de donner la recette entière à un cuisinier qui panique, le chef (DRIFT) lui dit : "D'abord, on s'occupe juste des œufs. Ensuite, juste de la farine. Ensuite, juste du four."
Le résultat : L'IA transforme une phrase difficile en plusieurs petites questions simples et précises.

2. RETROUVER (Retrieve) : Le Chasseur de Trésor

Maintenant que l'IA a ses petites questions simples, elle va chercher dans la bibliothèque de maths (Mathlib) les définitions exactes pour chaque morceau.

L'analogie : C'est comme si, pour chaque ingrédient (œufs, farine), on envoyait un chasseur de trésor chercher exactement la bonne marque de farine dans un immense supermarché, au lieu de chercher "un gâteau" en entier.
Le gain : On trouve les bonnes "briques" (définitions) beaucoup plus facilement car on ne cherche plus une aiguille dans une botte de foin, mais plusieurs petites aiguilles dans des petits tas.

3. ILLUSTRER (Illustrate) : Le Manuel de Montage

C'est l'étape la plus intelligente de DRIFT. Trouver les bonnes briques ne suffit pas. Il faut savoir comment les assembler. DRIFT va chercher 3 exemples de maisons similaires qui ont déjà été construites avec ces mêmes briques.

L'analogie : Vous avez trouvé les bonnes vis et les bons clous. Mais comment les visser ? DRIFT vous montre une photo d'un meuble IKEA déjà monté avec les mêmes pièces. Il dit : "Regarde, pour ce type de vis, il faut la tourner comme ça, pas comme ça."
Le but : Cela évite à l'IA de faire des erreurs de syntaxe (comme mettre une vis dans le mauvais trou).

4. FORMALISER (Formalize) : La Construction Finale

Maintenant, l'IA a tout ce qu'il faut :

Les petites questions claires.
Les bonnes définitions trouvées.
Les exemples de montage.

Elle assemble le tout pour écrire le théorème final en langage Lean.

🏆 Pourquoi est-ce une révolution ?

Les chercheurs ont testé DRIFT sur plusieurs bancs d'essai (des examens de maths pour ordinateurs).

Résultat : DRIFT a presque doublé la capacité de l'IA à trouver les bonnes définitions par rapport aux anciennes méthodes.
Le cas difficile : Sur des maths très nouvelles et complexes (que l'IA n'a jamais vues avant), DRIFT a fait des miracles, améliorant les résultats de plus de 40 %.
La leçon : L'IA est très forte pour comprendre le sens, mais elle a besoin d'aide pour la structure. DRIFT agit comme un scaffolding (échafaudage) : il soutient l'IA là où elle est faible, sans la faire travailler à sa place.

En résumé

DRIFT, c'est comme passer d'un étudiant qui doit apprendre un chapitre entier de mémoire d'un coup, à un étudiant qui :

Découpe le chapitre en résumés.
Cherche les définitions clés dans le dictionnaire.
Regarde des exemples de devoirs corrigés.
Et enfin, rédige son propre devoir parfait.

C'est une méthode qui rend les mathématiques formelles (ce langage difficile pour les ordinateurs) beaucoup plus accessibles et fiables pour les intelligences artificielles.

1. Le Problème : Les Limites de l'Autoformalisation Actuelle

L'autoformalisation consiste à traduire des énoncés mathématiques en langage naturel vers des statements formels vérifiables par machine (par exemple en Lean 4). Bien que les Grands Modèles de Langage (LLM) aient progressé dans le raisonnement mathématique informel, ils échouent souvent à l'autoformalisation "off-the-shelf" en raison de deux limitations majeures des méthodes de récupération augmentée (RAG) actuelles :

Complexité des requêtes monolithiques : Les énoncés informels sont denses et multifacettes. Les méthodes actuelles utilisent l'énoncé complet comme requête de recherche pour interroger des bibliothèques formelles (comme Mathlib). Cela crée un goulot d'étranglement sémantique où les détails nuancés sont perdus, rendant la récupération des définitions atomiques précises (prémisses) inefficace.
Manque de contexte d'utilisation : Même lorsque les bonnes définitions formelles sont récupérées, les modèles manquent souvent de connaissances contextuelles sur la façon de les utiliser syntaxiquement (ex: comment déclarer une variable, gérer les coercitions de types, ou structurer les arguments implicites). Les définitions brutes ne suffisent pas à guider la génération de code correct.

2. Méthodologie : Le Framework DRIFT

Les auteurs proposent DRIFT (Decompose, Retrieve, Illustrate, then Formalize Theorems), un cadre en quatre étapes conçu pour surmonter ces obstacles en adaptant la décomposition de requêtes et l'augmentation de contexte.

Étape 1 : Décomposer (Decompose)

Au lieu de traiter l'énoncé entier comme une requête unique, un LLM (le "Décomposeur") décompose l'énoncé informel en une série de sous-requêtes atomiques ( $Q$ ).

Chaque sous-requête cible un seul concept mathématique.
Pour chaque concept, le modèle génère une description en langage naturel et une représentation formelle prédite (ex: p : ℕ avec Nat.Prime p).
Cette prédiction formelle sert d'ancrage syntaxique pour améliorer la précision de la récupération, même si la prédiction est imparfaite.

Étape 2 : Récupérer (Retrieve)

Un récupérateur dense (basé sur BGE-M3 et finetuné sur la tâche de récupération de dépendances) identifie les prémisses formelles correspondantes pour chaque sous-requête.

Contrairement aux approches monolithiques qui récupèrent les $k$ meilleurs résultats pour une seule requête, DRIFT récupère le meilleur résultat pour chaque sous-requête atomique.
Les résultats sont agrégés et dédupliqués pour former l'ensemble des prémisses dépendantes ( $R_{DRIFT}$ ).

Étape 3 : Illustrer (Illustrate)

Pour combler le fossé entre la définition et l'usage, DRIFT sélectionne un petit ensemble de théorèmes illustratifs ( $T$ ).

Ces théorèmes sont choisis de manière à démontrer l'utilisation pratique des prémisses récupérées.
Un algorithme glouton sélectionne les théorèmes qui maximisent la couverture des prémisses récupérées, tout en étant sémantiquement proches de l'énoncé original.
Cela fournit au modèle des exemples concrets de syntaxe et de motifs d'application (ex: comment utiliser ZMod ou IsPrimitiveRoot dans un contexte réel).

Étape 4 : Formaliser (Formalize Theorems)

Un formalisateur (LLM) génère l'énoncé formel final ($FS$) en se basant sur un contexte complet ( $C$ ) qui concatène :

Les instructions de formalisation.
L'ensemble des prémisses récupérées ( $R_{DRIFT}$ ).
Les théorèmes illustratifs ( $T$ ).
L'énoncé informel original ($IF$).

3. Contributions Clés

Cadre de décomposition piloté par la récupération : DRIFT transforme la récupération monolithique en un processus aligné sur la structure de dépendance des mathématiques formelles, comblant le fossé entre la définition formelle et son usage syntaxique.
Nouvel état de l'art (SOTA) : Les expériences établissent de nouvelles performances sur les benchmarks ProofNet (in-distribution) et ConNF (out-of-distribution), surpassant les méthodes de récupération par dépendance existantes (comme RAutoformalizer) et les baselines zero-shot.
Analyse des limites des modèles : L'étude révèle que l'efficacité de la récupération dépend fortement des frontières de connaissances spécifiques à chaque modèle. Elle met en évidence la nécessité de stratégies de récupération adaptatives qui évaluent quand la connaissance externe complète réellement les capacités du modèle.

4. Résultats Expérimentaux

Les évaluations ont été menées sur trois benchmarks : ProofNet (maths universitaires, dépendances élevées), MiniF2F-test (olympiades, dépendances faibles) et ConNF (théorie des ensembles, hors distribution).

Récupération de dépendances : DRIFT améliore considérablement le score F1 de récupération par rapport à la baseline DPR (récupération directe). Sur ProofNet, le score F1 est presque doublé (passant de ~13,77% à ~27,68% avec Claude-Opus-4).
Autoformalisation (ConNF - Hors Distribution) : C'est ici que DRIFT brille le plus. Sur ConNF, où les modèles n'ont pas vu les objets formels lors de l'entraînement :
- Avec GPT-4.1, DRIFT améliore le score BEq+@10 de 55,57% par rapport au zero-shot, surpassant même la baseline "Oracle*" (qui fournit les dépendances parfaites mais sans contexte d'usage).
- Avec DeepSeek-V3.1, l'amélioration est de 43,18%.
- Cela démontre que les théorèmes illustratifs sont cruciaux pour guider l'usage des prémisses dans des domaines inconnus.
MiniF2F-test : Sur ce benchmark à faible dépendance, l'ajout de contexte peut parfois agir comme une distraction. Cependant, DRIFT reste compétitif, bien que l'analyse montre que pour les problèmes très simples, la récupération peut parfois dégrader la performance si elle introduit du bruit.
Modèles Spécialisés (Goedel-V2-8B) : DRIFT permet à un modèle spécialisé de doubler ses performances en BEq+ sur ConNF en lui fournissant le contexte syntaxique nécessaire, là où il échouait à utiliser ses connaissances paramétriques seules.

5. Signification et Conclusion

Le papier DRIFT démontre que l'autoformalisation ne dépend pas uniquement de la capacité d'un modèle à "connaître" les définitions, mais surtout de sa capacité à comprendre comment les utiliser dans un contexte syntaxique strict.

Synergie Décomposition-Illustration : L'ablation study montre que la décomposition seule peut introduire du bruit diversifié. L'étape "Illustrate" agit comme un échafaudage (scaffold) essentiel pour aider le modèle à naviguer dans cette information diversifiée et à appliquer correctement les prémisses.
Au-delà de la simple récupération : Le fait que DRIFT surpasse la baseline "Oracle*" (qui a les bonnes définitions mais pas les exemples d'usage) prouve que la structure contextuelle et les motifs d'application sont aussi critiques que la précision des définitions elles-mêmes.
Avenir : Les auteurs suggèrent que les futurs systèmes devraient intégrer des stratégies de récupération dynamiques et adaptatives (décidant quand récupérer ou non) et des cadres agentiques capables d'itérer sur la base des retours du compilateur.

En résumé, DRIFT propose une approche robuste et généralisable qui transforme l'autoformalisation d'une tâche de traduction directe en un processus de raisonnement structuré, combinant décomposition sémantique, récupération précise et apprentissage par l'exemple.