Nutzung großer Sprachmodelle zur automatisierten Beweissynthese in Rust

Leveraging Large Language Models for Automated Proof Synthesis in Rust

November 7, 2023

Autoren: Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui

cs.AI

Zusammenfassung

Formale Verifizierung kann die Korrektheit kritischer Systemsoftware nachweislich garantieren, doch die hohe Beweislast hat ihre breite Anwendung lange behindert. Kürzlich haben Large Language Models (LLMs) Erfolge in der Codeanalyse und -synthese gezeigt. In diesem Artikel präsentieren wir eine Kombination aus LLMs und statischer Analyse, um Invarianten, Assertions und andere Beweisstrukturen für ein Rust-basiertes formales Verifizierungsframework namens Verus zu synthetisieren. In einem Few-Shot-Setting zeigen LLMs beeindruckende logische Fähigkeiten bei der Generierung von Postconditions und Schleifeninvarianten, insbesondere bei der Analyse kurzer Codeausschnitte. Allerdings fehlt LLMs die Fähigkeit, Kontextinformationen zu behalten und weiterzugeben, eine Stärke der traditionellen statischen Analyse. Basierend auf diesen Beobachtungen entwickelten wir einen Prototyp auf Basis von OpenAIs GPT-4-Modell. Unser Prototyp zerlegt die Verifizierungsaufgabe in mehrere kleinere Teilaufgaben, fragt GPT-4 iterativ ab und kombiniert dessen Ausgabe mit einer leichten statischen Analyse. Wir evaluierten den Prototyp mit einem Entwickler im Automatisierungskreislauf an 20 vektormanipulierenden Programmen. Die Ergebnisse zeigen, dass er den menschlichen Aufwand beim Schreiben von einfachem Beweiscode erheblich reduziert.

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.