LLM2SMT: Building an SMT Solver with Zero Human-Written Code

Cet article présente LLM2SMT, une étude de cas démontrant qu'un agent codant basé sur un LLM peut construire entièrement, sans aucune ligne de code humain, un solveur SMT compétitif pour la logique QF_UF capable d'émettre des preuves formelles en Lean.

L'essentiel

Voici une explication simple et imagée de ce papier de recherche, conçue pour être comprise par tout le monde, même sans bagage technique.

🤖 Le Chef Cuisinier Robot : Comment un IA a construit un détective de logique sans aucune aide humaine

Imaginez que vous voulez construire une usine de détection de mensonges ultra-puissante. Cette usine doit pouvoir vérifier si des énoncés complexes sont vrais ou faux, même quand ils mélangent des mathématiques et de la logique. Traditionnellement, pour construire une telle usine, il faut des années d'études et des équipes d'ingénieurs humains.

Mais dans cette expérience, les chercheurs ont fait quelque chose de fou : ils ont demandé à une Intelligence Artificielle (un "agent de codage") de construire toute l'usine, seule, sans qu'un seul humain n'écrive une seule ligne de code.

Voici comment l'histoire se déroule, étape par étape, avec des analogies simples.

1. La Mission : Construire un "Détective de Logique"

Les chercheurs ont demandé à l'IA (nommée Claude) de créer un solveur SMT.

• L'analogie : Imaginez un détective privé très doué. Son travail est de prendre une liste d'indices (des équations, des égalités comme "A = B", "B = C") et de dire : "Est-ce que tout cela est possible en même temps ?" ou "Est-ce que c'est un mensonge ?".
• Le défi : L'IA devait écrire le code de ce détective en C++ (un langage informatique complexe), gérer les erreurs, et même prouver mathématiquement pourquoi elle a trouvé un mensonge.

2. Le Processus : Un Apprenti qui apprend en faisant des erreurs

Au début, l'IA a essayé de construire le détecte, mais comme un apprenti qui n'a jamais vu un marteau, elle a fait des bêtises :

• Elle a oublié comment gérer les "ou" et les "et" logiques.
• Elle a construit son propre petit détective au lieu d'utiliser les outils professionnels existants.
• Elle a laissé le détective travailler sans limite de temps, ce qui a failli faire planter l'ordinateur.

La solution des chercheurs : Ils n'ont pas écrit le code à sa place. Ils ont agi comme des chefs d'orchestre.

• Ils ont dit : "Non, utilise cet outil professionnel (CaDiCaL) pour la partie logique."
• Ils ont dit : "Attention, si ça tourne trop longtemps, coupe le courant !"
• Ils ont donné des exemples concrets d'échecs pour que l'IA comprenne où elle s'était trompée.

C'est comme si vous appreniez à quelqu'un à cuisiner un gâteau : vous ne faites pas le gâteau à sa place, mais vous lui dites : "Non, tu as mis trop de sel, essaie de mettre du sucre à la place" ou "N'oublie pas de préchauffer le four".

3. Les Astuces Magiques : Le "Pré-traitement"

L'une des plus belles découvertes de l'expérience est ce que l'IA a inventée toute seule pour résoudre des problèmes très difficiles (appelés "problèmes diamant").

• L'analogie : Imaginez que vous devez trouver un chemin dans un labyrinthe géant. Au lieu de courir dans tous les couloirs, l'IA a inventé une astuce : elle regarde les deux chemins possibles, voit ce qu'ils ont en commun, et trace une ligne directe entre les deux.
• Grâce à cette astuce, l'IA a résolu des problèmes en une fraction de seconde qui auraient pris des heures à un humain ou à d'autres logiciels. C'est comme si le détective trouvait un raccourci secret dans le labyrinthe que personne n'avait vu avant.

4. Le Certificat de Vérité : La Preuve en "Lean"

Le défi final était le plus dur : quand le détective dit "C'est un mensonge !", il doit pouvoir prouver qu'il a raison, comme un avocat devant un juge.

• L'IA devait écrire cette preuve dans un langage spécial appelé Lean (un langage utilisé par les mathématiciens pour vérifier les théorèmes).
• Le problème : L'IA avait du mal à comprendre que la preuve devait être structurée d'une manière très précise pour que le "juge" (le vérificateur Lean) accepte. Elle voulait parfois prouver des choses trop compliquées d'un coup.
• Le résultat : Après beaucoup d'essais, d'erreurs et de corrections, l'IA a réussi à produire des preuves valides. C'est comme si l'IA avait non seulement résolu l'énigme, mais avait aussi écrit le rapport officiel parfait pour le tribunal.

5. Le Verdict : Est-ce que ça marche ?

Les chercheurs ont mis leur création (nommée LLM2SMT) face à des géants du domaine comme Z3 et cvc5 (des logiciels créés par des humains experts).

• Résultat : L'IA a réussi à résoudre près de 99% des mêmes problèmes que les meilleurs logiciels du monde.
• La nuance : Elle est parfois un peu plus lente ou bloque sur certains cas très spécifiques, mais elle est compétitive.

🌟 Les Leçons à retenir

1. L'IA peut créer des outils de raisonnement : Oui, une IA peut écrire un logiciel qui sert à raisonner, même si c'est très complexe.
2. Mais elle a besoin d'un guide : L'IA ne fonctionne pas comme un magicien qui fait tout parfaitement du premier coup. Elle a besoin d'un humain pour lui donner des limites, corriger ses erreurs subtiles et lui montrer des exemples concrets. C'est ce qu'on appelle le "jagged intelligence" (une intelligence en dents de scie) : elle est brillante sur des tâches complexes mais peut échouer sur des détails bêtes (comme oublier de simplifier "A = A").
3. La preuve est difficile : Faire en sorte que l'IA écrive une preuve mathématique parfaite est beaucoup plus dur que de faire écrire le code du logiciel lui-même.

En résumé : Cette expérience montre que nous entrons dans une nouvelle ère où l'IA peut être un architecte de logiciels. Elle ne remplace pas encore l'humain (qui doit rester le chef d'orchestre pour vérifier la sécurité et la logique), mais elle peut construire des outils incroyablement puissants à partir de zéro, sans qu'un humain n'ait jamais touché un clavier pour écrire le code.

Résumé technique

Voici un résumé technique détaillé de l'article "LLM2SMT: Building an SMT Solver with Zero Human-Written Code" en français.

1. Problématique et Contexte

La question centrale de cette étude est de savoir si les Grands Modèles de Langage (LLM) sont capables de développer des outils de raisonnement automatisé complexes, et non pas seulement du code logiciel standard. Bien que les LLM soient utilisés pour la génération de code et la formalisation de preuves, leur capacité à créer un solveur SMT (Satisfiability Modulo Theories) complet, qui est lui-même un outil de raisonnement logique, reste largement inexplorée.

L'enjeu est double :

• Potentiel : Intégration rapide de fonctionnalités, expérimentation de nouvelles techniques et importation de méthodes issues de publications récentes.
• Risque : La propagation d'erreurs subtiles et difficiles à détecter. La correction (correctness) est primordiale : un LLM doit comprendre la logique sous-jacente pour produire un solveur fiable.

2. Méthodologie

Les auteurs ont mené une étude de cas où un agent de codage piloté par un LLM a construit un solveur SMT sans aucune ligne de code écrite par un humain.

• Modèle et Environnement : L'expérience a été réalisée avec le modèle Claude Sonnet 4.6 via l'interface Claude Code.
• Cible : Un solveur de style DPLL(T) pour la théorie des fonctions non interprétées sans quantificateurs (QF_UF). C'est une théorie fondamentale pour la plupart des solveurs modernes.
• Architecture du Solveur Généré :
  • Langage : C++20.
  • Parsing : Utilisation d'ANTLR avec la grammaire SMT-LIB v2.
  • Moteur SAT : Intégration de CaDiCaL via l'interface IPASIR-UP (après une tentative initiale infructueuse où l'agent avait écrit son propre solveur SAT rudimentaire).
  • Algorithme de Théorie : Implémentation de l'algorithme de fermeture de congruence de Nieuwenhuis-Oliveras.
  • Preuves : Émission de preuves formelles dans le langage Lean.
• Processus de Développement et Débogage :
  • Initialisation : Le LLM a reçu une description minimale et des références (algorithme de fermeture de congruence).
  • Correction des Bugs : L'agent a corrigé ses propres erreurs (ex: gestion des connecteurs booléens, traitement du XOR n-aire) lorsqu'on lui présentait des fichiers d'entrée échouant.
  • Outils d'Aide : Pour pallier les limites du débogage manuel par le LLM, les auteurs ont implémenté :
    • Un générateur de formules aléatoires (fuzzing).
    • Un script de test différentiel comparant le solveur LLM à un solveur de référence.
    • Des limites de temps strictes (timeout) pour éviter les processus infinis.
  • Prétraitement : Le LLM a conçu une technique de prétraitement pour résoudre les "problèmes diamant" (equational diamond problems), un cas difficile pour les solveurs paresseux (lazy SMT) car il nécessite d'inférer des littéraux non présents explicitement.

3. Contributions Clés

1. Preuve de Concept "Zéro Code Humain" : Démonstration qu'un agent LLM peut construire un solveur SMT fonctionnel et compétitif pour QF_UF sans intervention humaine directe dans l'écriture du code.
2. Implémentation de Techniques Avancées : Le solveur généré inclut non seulement la fermeture de congruence, mais aussi :
   • Des techniques de prétraitement sophistiquées (résolution des problèmes diamant en calculant la fermeture EUF de chaque branche de disjonction).
   • La génération de preuves Lean pour les instances insatisfiables.
3. Analyse des Défis du LLM : Identification de la "jagged intelligence" (intelligence irrégulière) : le LLM excelle dans des tâches complexes mais échoue sur des simplifications triviales (ex: t = t simplifié en true) sans guidance explicite.
4. Stratégie de Certification : Mise en place d'un pipeline de vérification où les modèles satisfiables sont validés par un solveur de référence, et les instances insatisfiables sont converties en preuves Lean (utilisant les tactiques grind et bv_decide).

4. Résultats Expérimentaux

Les performances ont été évaluées sur les benchmarks SMT-LIB QF_UF (non incrémentaux) et comparées à Z3 et cvc5.

• Résolution de Problèmes :
  • Z3 : 7 500 instances résolues.
  • cvc5 : 7 494 instances résolues.
  • LLM2SMT : 7 468 instances résolues.
  • Le solveur généré par LLM est compétitif, résolvant presque autant d'instances que les solveurs matures, bien qu'il soit légèrement moins performant en termes de "victoires" (temps de résolution inférieur de moins de 1s).
• Impact du Prétraitement et de la Propagation :
  • La version sans prétraitement (llm2smt-no-prepro) a résolu moins d'instances (7 355), confirmant l'efficacité de la technique de prétraitement développée par le LLM.
  • De manière surprenante, la désactivation de la propagation de théorie a légèrement amélioré les performances globales sur ces benchmarks spécifiques, suggérant que le surcoût de la propagation n'est pas toujours justifié sans une planification intelligente.
• Certification (Preuves Lean) :
  • La génération de preuves a été la tâche la plus difficile. Sur 285 instances certifiées, de nombreuses tentatives ont échoué (dépassement de temps, débordement de pile, échec de la tactique grind).
  • Aucune preuve erronée n'a été trouvée parmi celles qui ont réussi, ce qui valide la logique du solveur, même si le taux de réussite de la certification est faible en raison des limites de ressources de Lean.

5. Signification et Conclusion

Conclusion : La réponse à la question "Les LLM peuvent-ils développer des outils de raisonnement automatisé ?" est un "Oui, sous conditions".

Conditions de succès (Scaffolding) :

• Spécifications d'entrée très précises (SMT-LIB v2).
• Limites de ressources explicites (timeout).
• Utilisation systématique d'outils de test (fuzzing, delta-debugging).
• Fourniture d'exemples concrets et de cas d'échec pour guider le débogage.

Limites et Défis :

• Fiabilité : La correction ne peut pas être supposée ; des erreurs subtiles (comme la confusion entre propositions et termes booléens) persistent sans fuzzer.
• Génération de Preuves : C'est le point de blocage majeur. Le LLM peine à comprendre la complexité des preuves formelles et les attentes des vérificateurs (Lean), nécessitant une guidance humaine significative pour structurer la preuve.

Perspectives :
Les auteurs concluent que si un agent peut écrire un solveur compétitif à partir de zéro, l'avenir réside dans une analyse plus rigoureuse du code écrit pour suggérer des améliorations ciblées, plutôt que dans une autonomie totale. Ce travail ouvre la voie à l'utilisation d'agents LLM pour l'exploration rapide de nouvelles techniques de résolution SMT, à condition d'être encadré par des processus de validation stricts.