Aproveitando Modelos de Linguagem de Grande Escala para Síntese Automática de Provas em Rust
Leveraging Large Language Models for Automated Proof Synthesis in Rust
November 7, 2023
Autores: Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui
cs.AI
Resumo
A verificação formal pode garantir comprovadamente a correção de softwares críticos de sistemas, mas a alta carga de provas tem dificultado sua ampla adoção. Recentemente, os Modelos de Linguagem de Grande Escala (LLMs) têm demonstrado sucesso na análise e síntese de código. Neste artigo, apresentamos uma combinação de LLMs e análise estática para sintetizar invariantes, asserções e outras estruturas de prova para um framework de verificação formal baseado em Rust chamado Verus. Em um cenário de poucos exemplos, os LLMs demonstram uma impressionante capacidade lógica na geração de pós-condições e invariantes de loop, especialmente ao analisar trechos curtos de código. No entanto, os LLMs carecem da capacidade de reter e propagar informações de contexto, uma vantagem da análise estática tradicional. Com base nessas observações, desenvolvemos um protótipo baseado no modelo GPT-4 da OpenAI. Nosso protótipo decompõe a tarefa de verificação em várias menores, consulta iterativamente o GPT-4 e combina sua saída com uma análise estática leve. Avaliamos o protótipo com um desenvolvedor no loop de automação em 20 programas de manipulação de vetores. Os resultados demonstram que ele reduz significativamente o esforço humano na escrita de código de prova de nível básico.
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.