💻 computer science

Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study

Cette étude révèle que les prouveurs de théorèmes Lean entraînés par RL souffrent d'un effondrement de mode à l'inférence, qui peut être efficacement atténué en appliquant un calendrier fixe de squelettes de tactiques diversifiés pour retrouver des gains de performance significatifs, tandis que le paraphrasage des invites et les commentaires non pertinents s'avèrent inefficaces ou préjudiciables.

Auteurs originaux : Zachary Burton

Publié 2026-05-19

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Zachary Burton

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 un étudiant brillant formé pour résoudre des énigmes mathématiques très difficiles en utilisant un langage informatique spécial appelé Lean. Cet étudiant, appelons-le « DeepSeek », est incroyablement intelligent mais a une étrange habitude : lorsqu'on lui demande de résoudre une énigme, il reste bloqué dans une ornière mentale.

Ce document est un rapport de diagnostic expliquant pourquoi cela se produit et comment y remédier. Voici l'histoire de ce que les chercheurs ont découvert, racontée en termes courants.

1. Le Problème : L'Effet « Disque Rayé »

Les chercheurs ont remarqué que lorsqu'ils demandaient à DeepSeek de résoudre la même énigme mathématique encore et encore (juste avec des graines aléatoires légèrement différentes, comme lancer des dés), l'étudiant continuait d'essayer exactement la même première étape.

L'Analogie : Imaginez que vous essayez d'ouvrir une porte verrouillée. Vous essayez la clé dans la serrure. Ça ne marche pas. Vous réessayez. Ça ne marche toujours pas. Vous essayez une troisième fois, et une centième fois. Même si vous essayez 64 fois, vous enfoncez simplement la même clé dans la même serrure de la même manière. Vous n'explorez pas d'autres clés ni d'autres façons d'ouvrir la porte.
Le Résultat : Dans l'étude, doubler le nombre de tentatives de 32 à 64 n'a pas résolu une seule nouvelle énigme. L'étudiant avait « effondré son mode » : il était coincé sur un chemin étroit et ne pouvait rien imaginer d'autre.

2. La Solution : Donner un Indice de « Première Étape »

Les chercheurs ont réalisé que l'étudiant n'était pas paresseux ; il était simplement trop coincé dans sa routine. Alors, ils ont essayé un nouveau tour : avant de demander à l'étudiant de résoudre l'énigme, ils lui ont donné une instruction spécifique sur la façon de commencer.

L'Analogie : Au lieu de simplement dire « Résolvez cette énigme », les chercheurs ont dit « Commencez par simplifier les nombres » ou « Commencez par introduire une nouvelle variable ». C'est comme donner à l'étudiant une clé spécifique à essayer en premier, plutôt que de le laisser deviner.
Le Résultat : Ce simple encouragement a brisé l'ornière. L'étudiant a soudainement commencé à résoudre beaucoup plus d'énigmes. L'« ornière » n'était pas due au fait que l'étudiant était mauvais en mathématiques ; c'était parce qu'il était trop rigide dans sa façon de commencer.

3. Le « Pourquoi » : C'est un Problème de Formation, Pas de Cerveau

Les chercheurs voulaient savoir : l'étudiant est-il naturellement mauvais en mathématiques, ou est-ce la formation qui l'a rendu rigide ?

L'Expérience : Ils ont testé l'étudiant avant qu'il ne reçoive la formation mathématique spéciale (le modèle « Base »).
La Découverte : L'étudiant non formé ne pouvait résoudre aucune énigme du tout. Il abandonnait simplement ou répétait la question.
La Conclusion : La formation spéciale (Apprentissage par Renforcement) est ce qui a appris à l'étudiant à résoudre des énigmes dès le départ. Mais, cette même formation est aussi ce qui l'a rendu rigide et coincé dans une ornière. La formation a créé la compétence, mais elle a aussi créé le problème du « disque rayé ».

4. Qui D'autre a Ce Problème ?

Les chercheurs ont testé d'autres « étudiants » (différents modèles d'IA) pour voir si c'était un problème universel.

L'Étudiant « SFT » : Un étudiant avait été formé différemment (Affinage Supervisé). Cet étudiant était en fait meilleur pour résoudre des énigmes dans l'ensemble, mais il ne souffrait pas du problème d'« ornière ». Lorsque les chercheurs lui donnaient des indices, cela le rendait en fait légèrement pire. Il était déjà assez flexible pour trouver son propre chemin.
Les Étudiants « RL » : Les étudiants formés avec la méthode spéciale d'« Apprentissage par Renforcement » (comme DeepSeek) étaient ceux qui restaient bloqués. Ils avaient besoin des indices de « première étape » pour sortir de leur pensée étroite.

5. La Preuve du « Premier Coup »

Pour prouver qu'il ne s'agissait pas d'un simple hasard, les chercheurs ont examiné les véritables « premiers coups » que les étudiants faisaient.

La Découverte : Sur 64 tentatives pour une seule énigme, l'étudiant « coincé dans une ornière » utilisait exactement le même premier coup dans presque la moitié des cas. Il était incroyablement prévisible.
La Métaphore : Si vous demandiez à un humain d'écrire une histoire 64 fois, il pourrait commencer par « Il était une fois », « Le soleil brillait » ou « C'était une nuit sombre ». Mais cet étudiant en IA commencerait par « Il était une fois » 32 fois, et « Le soleil brillait » 30 fois. Il n'avait presque aucune variété dans son ouverture.

Résumé

Le document conclut que l'Apprentissage par Renforcement (une méthode spécifique de formation de l'IA) crée une arme à double tranchant :

Il apprend à l'IA comment résoudre des preuves mathématiques formelles (ce qu'elle ne pouvait pas faire auparavant).
Mais il rend aussi l'IA si focalisée sur quelques stratégies « gagnantes » qu'elle cesse d'en explorer de nouvelles.

La solution n'est pas de donner à l'IA plus de puissance de calcul ou plus de temps pour réfléchir ; c'est de lui fournir un guidage structurel — un simple encouragement sur la façon de commencer la preuve. Cela force l'IA à briser sa routine et à explorer de nouveaux chemins, débloquant des solutions qu'elle était auparavant trop obstinée à trouver.

Résumé technique : Diversité au moment de l'inférence dans les prouveurs de théorèmes Lean entraînés par RL

Énoncé du problème

Les prouveurs de théorèmes neuronaux récents, en particulier ceux entraînés par apprentissage par renforcement (RL) avec des récompenses vérifiables (RLVR), ont obtenu de solides performances sur des benchmarks de preuves formelles comme miniF2F. L'hypothèse prédominante est qu'un entraînement RL suffisant et une augmentation de la puissance de calcul au moment de l'inférence (via un échantillonnage i.i.d.) permettent aux modèles d'intérioriser les priors structurels nécessaires aux preuves formelles.

Cet article remet en cause cette hypothèse, diagnostiquant un phénomène de collapse de modes au moment de l'inférence chez les prouveurs Lean entraînés par RL. Plus précisément, les auteurs observent que l'augmentation du budget d'échantillonnage ( $k$ ) produit des rendements décroissants bien plus tôt que prévu. Sur le benchmark miniF2F-test avec DeepSeek-Prover-V1.5-RL, le doublement du budget d'échantillonnage de $k=32$ à $k=64$ ne produit aucun théorème résolu supplémentaire (bloqué à 42/244). Le modèle converge vers un ensemble restreint de stratégies de preuve et échoue à explorer des alternatives, même lorsqu'il dispose d'échantillons stochastiques supplémentaires.

Méthodologie

L'étude emploie un cadre de diagnostic contrôlé utilisant DeepSeek-Prover-V1.5-RL et sa variante de base non-RL, ainsi que des comparaisons inter-modèles avec DeepSeek-Prover-V2-7B (RL) et Goedel-Prover (SFT uniquement).

1. L'intervention par calendrier de squelettes

Pour tester si le plateau est dû à un manque de diversité structurelle plutôt qu'à un manque de puissance de calcul, les auteurs introduisent un calendrier fixe et déterministe de 15 squelettes de tactiques.

Structure : Une grille $15 \times 8 = 120$ combinant 15 squelettes de tactiques Lean sélectionnés à la main (par exemple simp, intro, constructor, aesop) avec 8 commentaires d'indices sur l'objectif (suggestions en langage naturel).
Exécution : Pour un budget $k$ , le modèle tente les $k$ premières entrées de cette grille. Cela force le modèle à démarrer les preuves avec des ouvertures stratégiques spécifiques plutôt que de s'appuyer sur un échantillonnage aléatoire.
Ablations : Pour isoler la source de l'amélioration, les auteurs comparent :
- B-RL (Squelette) : Le calendrier structuré de 15 squelettes.
- C1 (Paraphrase) : 16 paraphrases sémantiquement équivalentes des instructions (sans structure de tactique).
- C2 (Commentaires non pertinents) : 16 commentaires Lean sans contenu.
- C3 (NL uniquement) : Une condition dédiée utilisant uniquement des indices en langage naturel sans préfixes de tactiques.

2. Stratification de la difficulté

Les auteurs définissent un score empirique de difficulté de formalisation ( $\sigma$ ) utilisant une construction leave-one-out. Pour un théorème cible, $\sigma$ compte combien d'autres modèles de référence (Goedel-Prover, V2-7B) le résolvent sans intervention. Cela stratifie les théorèmes en catégories : Frontière (non résolus par les autres), Difficile, Moyen, Facile et Trivial.

3. Mesure distributionnelle directe

Pour dépasser les plateaux comportementaux, les auteurs analysent la diversité de la tête de première tactique sur 13 159 échantillons stochastiques. Ils comptent le nombre d'identifiants de tactiques principales distincts (par exemple have, rw, norm_num) générés par théorème.

Résultats clés

1. Briser le plateau par un guidage structurel

Collapse de base : DeepSeek-Prover-V1.5-RL avec échantillonnage i.i.d. résout 38 théorèmes à $k=16$ , 42 à $k=32$ , et reste à 42 à $k=64$ .
Efficacité des squelettes : Le calendrier fixe de squelettes brise ce plateau, résolvant 55 théorèmes à $k=16$ (+45 % d'amélioration relative) et continuant à trouver de nouvelles preuves jusqu'à $k=64$ (60 au total).
Résultats des ablations :
- Structure vs Diversité : Les paraphrases d'instructions (C1) produisent le même pass@16 que la base (38/244), tandis que les commentaires non pertinents (C2) dégradent les performances à 25/244. Cela confirme que les gains sont pilotés par un guidage structurel, et non par une simple diversité de prompts.
- NL vs Tactiques : La condition NL uniquement (C3) résout 48/244, un résultat intermédiaire entre la base et les squelettes complets. Cela indique que les indices en langage naturel récupèrent environ 58 % de l'écart, tandis que les préfixes de tactiques littéraux contribuent pour le reste.

2. Localisation du gain

Le gain structurel est concentré dans les catégories Facile et Trivial (théorèmes solubles par d'autres prouveurs open-source mais manqués par l'échantillonnage i.i.d. de V1.5-RL).

Dans la colonne combinée Facile+Trivial, l'intervention par squelettes produit un gain net de +15, tandis que les paraphrases produisent 0 et les commentaires non pertinents produisent -14.
Aucune perturbation ne débloque la catégorie « Frontière » (théorèmes non résolus par aucune base), suggérant que l'intervention remédie à une sous-exploration de problèmes connus comme solubles plutôt qu'à une expansion de la frontière des capacités.

3. Spécificité du RL du collapse de modes

Contraste avec le modèle de base : DeepSeek-Prover-V1.5-Base (non-RL) ne prouve aucun théorème dans aucune condition (i.i.d. ou squelettes). Cela établit que le RL est le lieu à la fois de la capacité de preuve et du collapse de modes subséquent. Le modèle de base manque de la capacité de générer des preuves valides ; l'étape RL crée cette capacité mais la collapse dans une politique étroite.
Contraste inter-modèles :
- V2-7B (RL) : Montre un gain agrégé plat (+1) mais débloque +3 théorèmes de frontière inaccessibles par toute base i.i.d.
- Goedel-Prover (SFT) : Montre un gain négatif (-10,0 $\pm$ 4,4) avec les squelettes. Les modèles entraînés par SFT semblent déjà explorer un large ensemble de racines de tactiques, rendant le calendrier fixe de squelettes redondant ou restrictif.

4. Preuve directe du collapse

L'analyse distributionnelle révèle que le théorème médian ne reçoit que 2 têtes de première tactique distinctes sur 64 échantillons, avec 49 % du benchmark recevant une ouverture stratégique unique déterministe. L'entropie de Shannon observée est $\le 8\%$ de la capacité théorique, confirmant un collapse de modes sévère.

Signification et revendications

L'article reformule le récit de « les squelettes de tactiques améliorent les performances » en « les prouveurs entraînés par RL sous-explorent sévèrement l'espace des tactiques au moment de l'inférence ».

RL comme agent dual : Les auteurs revendiquent que le RL joue un double rôle : c'est l'étape qui crée la capacité de preuve (car le modèle de base n'en a aucune) et simultanément l'étape qui collapse cette capacité sur une politique étroite.
Mise à l'échelle au moment de l'inférence : Les résultats suggèrent que la simple mise à l'échelle de la puissance de calcul d'inférence via un échantillonnage i.i.d. produit des rendements décroissants bien plus tôt que supposé. La diversité structurelle (variation des stratégies de preuve via des prompts) est un axe de mise à l'échelle plus efficace.
Réparabilité : Le collapse de modes est spécifique aux modèles entraînés par RL. Les modèles entraînés par SFT ne présentent pas le même collapse récupérable via des indices structurels ; en fait, ils en souffrent. Cela implique que les interventions futures (régularisation de l'entropie au moment de l'entraînement ou récupération de squelettes au moment de l'inférence) doivent naviguer le compromis entre la création de capacité et le maintien de la diversité.

L'étude conclut que le « collapse de modes » est un phénomène réel, contingent au pipeline, inhérent au processus de fine-tuning par RL dans les domaines de vérification formelle, et que des interventions structurelles fixes peuvent efficacement récupérer l'exploration perdue sans nécessiter d'entraînement supplémentaire.