Exploiter les modèles de langage à grande échelle pour la synthèse automatisée de preuves en Rust
Leveraging Large Language Models for Automated Proof Synthesis in Rust
November 7, 2023
Auteurs: Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui
cs.AI
Résumé
La vérification formelle peut garantir de manière prouvable la correction des logiciels systèmes critiques, mais la charge de preuve élevée a longtemps entravé son adoption généralisée. Récemment, les modèles de langage de grande taille (LLMs) ont montré des succès dans l'analyse et la synthèse de code. Dans cet article, nous présentons une combinaison de LLMs et d'analyse statique pour synthétiser des invariants, des assertions et d'autres structures de preuve pour un cadre de vérification formelle basé sur Rust appelé Verus. Dans un contexte de few-shot, les LLMs démontrent une capacité logique impressionnante à générer des postconditions et des invariants de boucle, en particulier lors de l'analyse de courts extraits de code. Cependant, les LLMs manquent de la capacité à retenir et à propager les informations contextuelles, une force de l'analyse statique traditionnelle. Sur la base de ces observations, nous avons développé un prototype basé sur le modèle GPT-4 d'OpenAI. Notre prototype décompose la tâche de vérification en plusieurs sous-tâches plus petites, interroge GPT-4 de manière itérative, et combine sa sortie avec une analyse statique légère. Nous avons évalué le prototype avec un développeur dans la boucle d'automatisation sur 20 programmes manipulant des vecteurs. Les résultats démontrent qu'il réduit significativement l'effort humain dans l'écriture de code de preuve de niveau d'entrée.
English
Formal verification can provably guarantee the correctness of critical system
software, but the high proof burden has long hindered its wide adoption.
Recently, Large Language Models (LLMs) have shown success in code analysis and
synthesis. In this paper, we present a combination of LLMs and static analysis
to synthesize invariants, assertions, and other proof structures for a
Rust-based formal verification framework called Verus. In a few-shot setting,
LLMs demonstrate impressive logical ability in generating postconditions and
loop invariants, especially when analyzing short code snippets. However, LLMs
lack the ability to retain and propagate context information, a strength of
traditional static analysis. Based on these observations, we developed a
prototype based on OpenAI's GPT-4 model. Our prototype decomposes the
verification task into multiple smaller ones, iteratively queries GPT-4, and
combines its output with lightweight static analysis. We evaluated the
prototype with a developer in the automation loop on 20 vector-manipulating
programs. The results demonstrate that it significantly reduces human effort in
writing entry-level proof code.