Sfruttare i Modelli Linguistici di Grande Scala per la Sintesi Automatica di Dimostrazioni in Rust
Leveraging Large Language Models for Automated Proof Synthesis in Rust
November 7, 2023
Autori: Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui
cs.AI
Abstract
La verifica formale può garantire in modo dimostrabile la correttezza del software critico di sistema, ma l'elevato onere di dimostrazione ha a lungo ostacolato la sua ampia adozione. Recentemente, i Large Language Models (LLM) hanno dimostrato successo nell'analisi e nella sintesi del codice. In questo articolo, presentiamo una combinazione di LLM e analisi statica per sintetizzare invarianti, asserzioni e altre strutture di prova per un framework di verifica formale basato su Rust chiamato Verus. In un contesto few-shot, gli LLM dimostrano un'impressionante capacità logica nella generazione di postcondizioni e invarianti di ciclo, specialmente quando analizzano brevi frammenti di codice. Tuttavia, gli LLM mancano della capacità di conservare e propagare informazioni contestuali, un punto di forza dell'analisi statica tradizionale. Sulla base di queste osservazioni, abbiamo sviluppato un prototipo basato sul modello GPT-4 di OpenAI. Il nostro prototipo scompone il compito di verifica in più sotto-compiti, interroga iterativamente GPT-4 e combina il suo output con un'analisi statica leggera. Abbiamo valutato il prototipo con uno sviluppatore nel ciclo di automazione su 20 programmi che manipolano vettori. I risultati dimostrano che riduce significativamente lo sforzo umano nella scrittura di codice di prova di livello base.
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.