Avancées dans l'automatisation des preuves avec les LLMs

L'automatisation des preuves est un domaine super important en ingénierie logicielle. Ça aide à s'assurer que les logiciels fonctionnent comme il faut en vérifiant leurs propriétés avec des méthodes formelles. Les assistants de preuve interactifs (ITP) comme Coq, Isabelle et Lean sont des outils souvent utilisés pour ça. Même si ces outils peuvent garantir que le logiciel est correct, les utiliser demande souvent beaucoup d'expertise et d'efforts de la part des utilisateurs.

Récemment, les Grands Modèles de Langage (LLMs) ont montré qu'ils pouvaient générer des preuves informelles en langage naturel. Mais ils ont du mal à générer des preuves formelles adaptées aux ITP. Cet article explore les défis et les opportunités d'utiliser les LLMs pour l'automatisation des preuves.

#Le besoin d'automatisation des preuves

La correction est essentielle pour les systèmes logiciels, surtout dans des domaines critiques comme les compilateurs, les systèmes distribués et les systèmes d'exploitation. Les ITP permettent aux utilisateurs d'énoncer et de prouver des Théorèmes formels sur les logiciels. Ces preuves sont vérifiées mécaniquement pour garantir leur validité, ce qui donne une solide base pour la correction logicielle.

Cependant, créer des scripts de preuve pour les ITP exige souvent beaucoup de temps et d'efforts. Par exemple, la vérification du compilateur CompCert C a pris environ six années-homme pour développer un gros script de preuve. De tels investissements de ressources peuvent freiner l'adoption des méthodes formelles en développement logiciel.

#Défis avec les techniques actuelles d'automatisation des preuves

Plusieurs techniques ont été proposées pour aider à l'automatisation des preuves, principalement réparties en deux catégories : les méthodes symboliques et les méthodes d'apprentissage machine.

Les méthodes symboliques utilisent des théorèmes établis et des prouveurs de théorèmes automatisés (ATPs) pour aider à prouver de nouveaux théorèmes. Bien qu'elles soient efficaces, ces méthodes échouent souvent avec la logique d'ordre supérieur ou le raisonnement inductif, ce qui limite leur applicabilité.

Les méthodes d'apprentissage machine visent à prédire la prochaine étape d'une preuve en utilisant des modèles appris. Ces méthodes peuvent être puissantes mais nécessitent de grandes quantités de données d'entraînement pour bien fonctionner. En plus, les preuves générées peuvent ne pas être assez fiables pour des tâches de vérification formelle.

#Le rôle des grands modèles de langage

Les LLMs ont attiré l'attention pour leur capacité à générer des preuves en langage naturel. Ils offrent une alternative potentielle en fournissant un moyen de générer automatiquement des étapes de preuve. Cependant, même des modèles avancés comme GPT ne brillent pas dans la production de preuves formelles pour les ITP. Ils peuvent créer une structure de haut niveau pour une preuve mais peinent souvent avec les détails fins, qui sont cruciaux pour la vérification formelle.

Pour aborder ces limites, une étude a été menée pour analyser les erreurs commises par les LLMs lors de la génération de scripts de preuve. Plus de 500 erreurs de génération de preuve ont été examinées, révélant que bien que les LLMs puissent identifier la structure générale, elles échouaient souvent à obtenir les détails spécifiques corrects.

#Une nouvelle approche : Générer-puis-réparer

Basée sur les informations recueillies durant l'étude, une nouvelle approche d'automatisation des preuves a été développée. Cette méthode suit une stratégie de générer-puis-réparer, qui utilise d'abord un LLM pour générer une preuve initiale, puis applique des méthodes symboliques pour corriger les erreurs de cette preuve.

La nouvelle approche incorpore quatre mécanismes de réparation ciblant les erreurs courantes identifiées dans l'analyse. Si les réparations échouent, une procédure de retour en arrière est utilisée pour régénérer les étapes de preuve précédentes dans une tentative de corriger les erreurs.

#Évaluation de la nouvelle approche

La méthode nouvellement proposée a été évaluée en utilisant un grand ensemble de données contenant plus de 10 000 théorèmes. Les résultats ont montré une amélioration significative du nombre de théorèmes prouvés comparé aux approches existantes à la pointe de la technologie. La nouvelle méthode a prouvé plus de 1 200 théorèmes qui étaient auparavant hors de portée des technologies existantes.

#Informations de l'étude formative

L'étude formative a révélé plusieurs types d'erreurs courantes commises par les LLMs. Ces erreurs ont été classées en sept types, y compris des références de théorèmes incorrectes, des utilisations inappropriées de tactiques et des réécritures échouées qui ne correspondaient à aucune partie du but.

Une découverte majeure était que même si les LLMs généraient souvent des preuves avec la bonne structure de haut niveau, elles avaient du mal à fournir les bons détails de bas niveau. Beaucoup d'erreurs auraient potentiellement pu être corrigées avec des réparations simples plutôt qu'une régénération complète de la preuve.

#Le processus de construction de preuve

La preuve par des assistants de thèses interactifs implique généralement plusieurs étapes :

1. Énoncer des théorèmes : L'utilisateur définit un théorème en utilisant des mots-clés comme Théorème, Lemma ou Preuve.
2. Scripts de preuve : Les utilisateurs créent une série de tactiques qui détaillent comment prouver le théorème, avec ces tactiques guidant le processus de preuve.
3. États de preuve : Coq affiche l'état actuel de la preuve, montrant les objectifs qui n'ont pas encore été prouvés.
4. Tactiques : Les tactiques décomposent les obligations de preuve en parties plus simples, menant finalement à une preuve complète.

#Exemple de preuve dans Coq

Pour illustrer, prenons le théorème qui dit que l'addition des nombres naturels est commutative. La preuve implique d'utiliser des tactiques définies pour manipuler l'état actuel de la preuve et résoudre les sous-objectifs.

Le processus implique des tactiques comme intros pour introduire des variables et induction pour décomposer le problème. Chaque tactique modifie l'état de la preuve, menant à une série d'étapes qui finit par résoudre le théorème.

#Mécanismes de réparation

L'approche d'automatisation des preuves développée utilise plusieurs mécanismes de réparation pour corriger les erreurs courantes produites par les LLMs. Ces mécanismes traitent systématiquement des problèmes tels que des références non définies, des applications de tactiques incorrectes et un usage inapproprié des points.

#Gestion des références non définies

Quand un LLM génère un script de preuve qui utilise des références non définies, le mécanisme de réparation cherche des noms similaires dans le contexte local et le contexte global. Ça aide à trouver des remplacements appropriés et permet de continuer la preuve.

#Correction d'un usage inapproprié de tactiques

L'approche vérifie aussi les tactiques mal appliquées dans la preuve. Si un LLM essaie d'appliquer une tactique incorrectement, le mécanisme identifie l'erreur et effectue les ajustements nécessaires dans le script de preuve.

#Traitement d'un usage inapproprié des points

Les LLMs peuvent mal utiliser des points dans les preuves, soit en essayant de passer à l'objectif suivant trop tôt, soit en utilisant une syntaxe incorrecte pour les points. Le mécanisme de réparation rectifie ces erreurs en mettant à jour le script de preuve selon le format de point attendu.

#Procédure de retour en arrière

Quand les mécanismes de réparation ne peuvent pas résoudre une erreur donnée, la procédure de retour en arrière entre en jeu. Cette méthode évalue les tactiques de preuve précédentes pour déterminer si revenir à un état antérieur peut aider à résoudre les objectifs restants.

Ce processus est crucial car il évite de devoir régénérer une preuve depuis le début, permettant une résolution plus efficace des erreurs. Il garantit que tous les sous-objectifs réalisables sont prouvés consécutivement sans sauter d'étapes critiques.

#Résultats expérimentaux

L'efficacité de la nouvelle approche d'automatisation des preuves a été évaluée par rapport aux méthodes existantes. Les résultats ont montré qu'elle surpassait les techniques d'État de l'art précédentes, tant en termes de nombre de théorèmes prouvés qu'en matière de gestion de preuves plus complexes.

L'étude a aussi mis en lumière les améliorations en utilisant différents LLMs, démontrant que l'approche est adaptable et bénéfique à travers diverses architectures de modèles.

#Efficacité des composants

Une étude d'ablation a été réalisée pour analyser l'efficacité de chaque composant de la nouvelle approche. Les résultats ont confirmé que tous les éléments contribuent positivement à la performance globale du système d'automatisation des preuves.

En effectuant une réparation et un retour en arrière, l'approche a constamment permis de prouver beaucoup plus de théorèmes que ses homologues.

#Limitations et travaux futurs

Malgré ses forces, la nouvelle approche a des limitations. Son efficacité dépend de la qualité de la preuve initiale générée par le LLM. Si le script initial est largement mal orienté, les mécanismes de réparation pourraient avoir du mal à le sauver.

De plus, l'approche ne tire actuellement pas parti des tactiques définies par l'utilisateur de manière efficace, ce qui pourrait s'avérer vital dans certaines situations de preuve. Les améliorations futures pourraient se concentrer sur l'amélioration du récupérateur pour reconnaître et utiliser ces tactiques personnalisées.

Des avancées dans la conception des invites pourraient aussi donner lieu à des gains de performance supplémentaires. Des variations dans les stratégies de questionnement pourraient donner de meilleurs résultats, surtout avec les modèles à venir.

#Conclusion

L'intégration des LLMs et des méthodes symboliques dans l'automatisation des preuves présente des opportunités prometteuses pour l'avenir de la vérification formelle. Bien que des défis demeurent, les progrès réalisés dans la génération de scripts de preuve fiables offrent une voie pour améliorer l'efficacité de la vérification logicielle.

Alors que la technologie LLM continue d'évoluer, il y a un potentiel pour développer des méthodes d'automatisation des preuves encore plus sophistiquées. Cela pourrait conduire à une adoption plus large de la preuve par assistants de thèses interactifs en ingénierie logicielle, résultant finalement en des systèmes logiciels plus robustes et fiables.