Gebruikmaken van Grote Taalmodellen voor Geautomatiseerde Bewijssynthese in 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

Samenvatting

Formele verificatie kan de correctheid van kritieke systeemsoftware aantoonbaar garanderen, maar de hoge bewijslast heeft de brede adoptie ervan lange tijd belemmerd. Recentelijk hebben Large Language Models (LLMs) succes getoond in code-analyse en -synthese. In dit artikel presenteren we een combinatie van LLMs en statische analyse om invarianten, beweringen en andere bewijsstructuren te synthetiseren voor een op Rust gebaseerd formeel verificatieframework genaamd Verus. In een few-shot setting tonen LLMs indrukwekkend logisch vermogen in het genereren van postcondities en lusinvarianten, vooral bij het analyseren van korte codefragmenten. LLMs missen echter het vermogen om contextinformatie te behouden en door te geven, een sterk punt van traditionele statische analyse. Op basis van deze observaties hebben we een prototype ontwikkeld gebaseerd op OpenAI's GPT-4-model. Ons prototype verdeelt de verificatietaak in meerdere kleinere taken, bevraagt GPT-4 iteratief en combineert de uitvoer ervan met lichte statische analyse. We hebben het prototype geëvalueerd met een ontwikkelaar in de automatiseringlus op 20 programma's die vectoren manipuleren. De resultaten tonen aan dat het de menselijke inspanning aanzienlijk vermindert bij het schrijven van instapniveau bewijscode.

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.