Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers

Ce papier présente Strat2Rocq, une méthode qui extrait et formalise les stratégies de preuve des grands modèles de langage en lemmas Rocq pour améliorer significativement l'efficacité des prouveurs symboliques comme CoqHammer, tout en bénéficiant également aux agents de preuve basés sur les LLM.

L'essentiel

🧠 Le Grand Magicien et le Mécanicien de Précision

Imaginez deux personnages très différents qui travaillent dans un atelier de réparation de voitures (ce sont nos logiciels) :

1. Le Grand Magicien (le Modèle de Langage ou LLM) : C'est un génie créatif qui a lu des millions de livres. Il peut deviner la solution d'un problème complexe d'un seul coup d'œil, comme par magie. Il dit : "Ah, c'est évident ! Il faut faire ça !". Mais il a deux gros défauts : il est très lent (il faut beaucoup d'électricité pour le faire fonctionner) et il ne veut pas travailler dans votre garage privé (vos données sont confidentielles, vous ne pouvez pas les envoyer sur Internet).
2. Le Mécanicien de Précision (le Démonstrateur Symbolique) : C'est un robot très rigoureux, rapide et sûr. Il suit des règles strictes, pas de place pour l'imagination. Il est parfait pour travailler dans votre garage privé, mais il est parfois un peu "bête" : s'il ne connaît pas une règle précise, il ne peut pas avancer, même si la solution est simple.

Le problème : Le Magicien est trop cher et risqué à utiliser en permanence. Le Mécanicien est sûr, mais il bloque souvent sur des problèmes difficiles.

💡 L'Idée Géniale : "Strat2Rocq"

Les chercheurs de l'Université de Pékin se sont posé une question simple : Et si on pouvait apprendre au Mécanicien les "trucs de magicien" du Grand Magicien, sans avoir besoin de le faire travailler ?

C'est là qu'intervient Strat2Rocq. C'est comme un traducteur de secrets.

📚 Comment ça marche ? (L'histoire en 3 étapes)

Étape 1 : L'Observation (La phase "Hors ligne")
Imaginez que vous filmez le Grand Magicien en train de résoudre des milliers de problèmes de logique.

• Le Magicien ne dit pas : "J'ai appliqué la règle A, puis la règle B". Il dit : "Regarde, c'est évident que A + B = C".
• Strat2Rocq regarde ces réponses magiques et se dit : "Attends, il a sauté une étape. Il a utilisé un raccourci mental. Je vais écrire ce raccourci sur un petit papier officiel."
• Ce "petit papier", c'est ce qu'on appelle un lemme (une petite règle mathématique). Le système transforme l'intuition floue du Magicien en une règle mathématique précise que le Mécanicien peut comprendre.

Étape 2 : L'Entraînement (Le "Stockage")
Une fois que le Magicien a travaillé sur des milliers de problèmes, on a une énorme bibliothèque de ces "petits papiers" (les lemmes). On ne garde pas le Magicien, on garde juste ses astuces écrites.

Étape 3 : La Réparation (La phase "En ligne")
Quand un nouveau problème arrive dans votre garage privé :

• Le Mécanicien de Précision (CoqHammer) reçoit le problème.
• Avant de commencer, on lui glisse dans la main la bibliothèque de "petits papiers" extraits du Magicien.
• Soudain, le Mécanicien voit une règle qu'il ne connaissait pas : "Ah ! Si je fais ça, le problème devient facile !". Il résout le problème en quelques secondes, sans avoir besoin d'appeler le Magicien.

🎁 Les Résultats Surprenants

Les chercheurs ont testé cette idée sur de vrais projets informatiques (comme un compilateur C certifié). Voici ce qu'ils ont découvert :

1. Le Mécanicien devient un surhomme : Grâce aux astuces du Magicien, le robot a réussi à résoudre 13,41 % de problèmes de plus qu'avant. C'est énorme !
2. Le Magicien s'améliore aussi : Paradoxalement, si on donne ces "petits papiers" à un nouveau Magicien pour l'aider, il réussit aussi mieux (de 4 %). C'est comme si le Magicien apprenait à mieux s'organiser en voyant ses propres idées écrites proprement.
3. Sécurité et Économie : On n'a plus besoin d'envoyer vos données confidentielles au cloud. Tout se passe sur votre ordinateur, avec un robot rapide et peu coûteux.

🌟 L'Analogie Finale

Imaginez que vous voulez apprendre à jouer au piano.

• Le Magicien est un virtuose qui joue par cœur, mais il ne sait pas expliquer comment il fait.
• Le Mécanicien est un élève qui lit la partition note par note, mais il est très lent.

Strat2Rocq, c'est comme un professeur qui écoute le virtuose, écrit les "accords magiques" sur une partition simplifiée, et les donne à l'élève. L'élève n'a pas besoin de devenir un génie, il a juste besoin d'avoir les bons accords sous les doigts pour jouer la symphonie parfaitement.

En résumé : Cette recherche montre qu'on peut capturer l'intelligence "magique" des IA modernes pour rendre les outils de sécurité actuels beaucoup plus puissants, tout en restant rapides, sûrs et peu coûteux.

Résumé technique

Voici un résumé technique détaillé de l'article "Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers" (Extraction de stratégies de preuve à partir des LLM pour améliorer les prouveurs symboliques), rédigé en français.

1. Problématique

L'article aborde le défi de l'automatisation des preuves dans le cadre de la vérification logicielle par preuve interactive de théorèmes (ITP). Bien que les prouveurs symboliques (comme CoqHammer) soient efficaces, sécurisés et peu coûteux, ils peinent souvent à prouver des théorèmes complexes sans intervention humaine. Récemment, les Grands Modèles de Langage (LLM) ont démontré une grande capacité à générer des preuves, mais leur utilisation directe présente des limites majeures :

• Coût et ressources : L'exécution en ligne de LLMs est coûteuse et gourmande en calcul.
• Sécurité : L'envoi de bases de code confidentielles vers des services LLM externes pose des risques de fuite d'informations.
• Dépendance : Les agents de preuve hybrides actuels nécessitent une interaction continue avec le LLM, ce qui empêche une automatisation purement locale et sécurisée.

L'objectif de la recherche est de répondre à la question suivante : Peut-on extraire les stratégies de preuve internes des LLMs pour améliorer les capacités des prouveurs symboliques, sans dépendre du LLM lors de la phase de preuve ?

2. Méthodologie : Strat2Rocq

Les auteurs proposent Strat2Rocq, un cadre de travail en deux étapes conçu pour extraire les connaissances des LLMs sous forme de lemmes formels réutilisables. Le système fonctionne sur l'hypothèse que les LLMs, entraînés sur des données humaines, adoptent des stratégies de preuve similaires (inférences directes basées sur des règles implicites) que l'on peut formaliser.

Étape 1 : Extraction de Lemmes (Hors ligne / Offline)

Cette phase se déroule une seule fois sur un ensemble d'entraînement (corpus de théorèmes) :

1. Génération de preuves en langage naturel (NL) : Pour chaque théorème, un LLM (ex: Claude 3.7 Sonnet) est invité à générer une preuve étape par étape en langage naturel, en fournissant le contexte (définitions de types, fonctions, script Coq).
2. Généralisation et Formalisation : Le LLM est ensuite sollicité pour :
   • Identifier les étapes clés de la preuve NL.
   • Généraliser ces étapes en lemmes abstraits.
   • Formaliser ces lemmes dans le langage Rocq (Coq) et générer leurs preuves formelles.
3. Agent de Preuve de Réparation : Un agent itératif vérifie les lemmes générés. En cas d'erreur, il utilise des modules de réparation spécialisés pour corriger le LLM jusqu'à obtenir un lemme valide ou atteindre une limite d'itérations.

Étape 2 : Preuve de Théorèmes (En ligne / Online)

Lors de la preuve d'un nouveau théorème :

• Les lemmes extraits lors de l'étape 1 sont injectés dans le contexte de preuve.
• Le prouveur symbolique CoqHammer (le prouveur d'état de l'art pour Rocq) utilise ces nouveaux lemmes comme connaissances supplémentaires.
• Point clé : Le LLM n'est plus utilisé pendant cette phase. La preuve est effectuée exclusivement par le prouveur symbolique, garantissant sécurité et faible coût.

3. Contributions Clés

1. Nouveau problème de recherche : L'extraction hors ligne des stratégies de preuve des LLMs pour les intégrer dans des prouveurs symboliques.
2. Approche d'extraction : Une méthode innovante transformant les preuves en langage naturel (générées par LLM) en lemmes formels vérifiés, comblant ainsi le fossé entre l'intuition des LLMs et la rigueur des prouveurs symboliques.
3. Implémentation et validation : Développement de Strat2Rocq et validation empirique sur des projets Rocq open-source, démontrant une amélioration significative des performances.

4. Résultats Expérimentaux

L'évaluation a été menée sur un jeu de données de 2 394 théorèmes issus de projets majeurs (CompCert, Ext-Lib, Coq-Art, Vfa) en utilisant une validation croisée 3-fold.

• Amélioration des Prouveurs Symboliques (RQ2) :

  • L'ajout des lemmes extraits par Strat2Rocq a augmenté le taux de réussite de CoqHammer de 13,41 % en moyenne.
  • L'amélioration est particulièrement notable sur CompCert (+17,75 %), prouvant l'efficacité sur des projets industriels réels.
  • Mécanisme d'amélioration : Les lemmes extraits permettent souvent d'éviter l'induction (difficile pour les prouveurs symboliques purs) en fournissant des équivalences directes, et améliorent la sélection de lemmes pertinents.

• Robustesse et Généralisation (RQ3) :

  • La méthode fonctionne avec différents LLMs backend (Claude 3.7 Sonnet et o3-mini).
  • La combinaison des lemmes extraits de deux LLMs différents améliore encore davantage les résultats, suggérant que les stratégies internes des LLMs sont complémentaires et non redondantes.

• Impact sur les Agents LLM (RQ5) :

  • De manière inattendue, les lemmes extraits améliorent également les performances des agents de preuve basés sur LLM (augmentation de 4,00 % du nombre de théorèmes prouvés).
  • Cela réduit également la consommation de tokens (moins d'appels LLM nécessaires car CoqHammer résout plus de problèmes seul).

• Analyse Ablative (RQ4) :

  • L'étape de génération de preuve en langage naturel est cruciale. Sans elle (génération directe de lemmes formels), le nombre de lemmes extraits chute de 63,56 %, confirmant que le langage naturel sert de pont essentiel pour capturer la logique du LLM.

5. Signification et Conclusion

Ce travail marque une avancée significative dans l'intersection entre l'IA générative et la vérification formelle :

• Sécurité et Efficacité : Il permet de bénéficier de l'intelligence des LLMs tout en conservant les avantages des systèmes symboliques (sécurité des données, exécution locale, coût réduit).
• Compréhension des LLMs : En formalisant les stratégies de preuve des LLMs sous forme de lemmes vérifiés, Strat2Rocq offre une fenêtre sur le "raisonnement" interne des modèles, contribuant à la recherche sur l'interprétabilité des LLMs.
• Futur : La méthode est adaptable à d'autres assistants de preuve (Lean, Isabelle) et ouvre la voie à des prouveurs symboliques enrichis par l'apprentissage, capables de rivaliser avec les agents hybrides complexes.

En résumé, Strat2Rocq démontre que l'on peut "distiller" l'expertise des LLMs dans des systèmes formels légers et sécurisés, transformant les LLMs d'outils d'assistance coûteux en sources de connaissances permanentes pour les prouveurs symboliques.