Использование крупных языковых моделей для автоматического синтеза доказательств в Rust
Leveraging Large Language Models for Automated Proof Synthesis in Rust
November 7, 2023
Авторы: Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui
cs.AI
Аннотация
Формальная верификация может гарантировать корректность критически важного системного программного обеспечения, однако высокая сложность доказательств долгое время препятствовала её широкому внедрению. В последнее время крупные языковые модели (LLM) продемонстрировали успехи в анализе и синтезе кода. В данной статье мы представляем комбинацию LLM и статического анализа для синтеза инвариантов, утверждений и других структур доказательств в рамках системы формальной верификации на основе Rust под названием Verus. В условиях few-shot LLM демонстрируют впечатляющие логические способности в генерации постусловий и инвариантов циклов, особенно при анализе коротких фрагментов кода. Однако LLM не способны сохранять и распространять контекстную информацию, что является сильной стороной традиционного статического анализа. На основе этих наблюдений мы разработали прототип, использующий модель GPT-4 от OpenAI. Наш прототип разбивает задачу верификации на несколько более мелких, итеративно запрашивает GPT-4 и объединяет её вывод с лёгким статическим анализом. Мы оценили прототип с участием разработчика в цикле автоматизации на 20 программах, манипулирующих векторами. Результаты показывают, что он значительно сокращает усилия человека при написании базового кода доказательств.
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.