러스트에서 자동화된 증명 합성을 위한 대형 언어 모델 활용
Leveraging Large Language Models for Automated Proof Synthesis in Rust
November 7, 2023
저자: Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui
cs.AI
초록
형식 검증(formal verification)은 중요한 시스템 소프트웨어의 정확성을 수학적으로 보장할 수 있지만, 높은 증명 부담으로 인해 오랫동안 광범위한 채택이 어려웠다. 최근, 대규모 언어 모델(LLMs)이 코드 분석 및 합성 분야에서 성공을 거두고 있다. 본 논문에서는 Rust 기반의 형식 검증 프레임워크인 Verus를 위해 불변식(invariants), 단언문(assertions), 그리고 기타 증명 구조를 합성하기 위해 LLMs와 정적 분석(static analysis)을 결합한 방법을 제시한다. 소량의 예시만 제공하는 환경에서도 LLMs는 짧은 코드 조각을 분석할 때 특히 후조건(postconditions)과 루프 불변식(loop invariants)을 생성하는 데 있어 인상적인 논리적 능력을 보여준다. 그러나 LLMs는 전통적인 정적 분석의 강점인 컨텍스트 정보를 유지하고 전파하는 능력이 부족하다. 이러한 관찰을 바탕으로, 우리는 OpenAI의 GPT-4 모델을 기반으로 한 프로토타입을 개발했다. 이 프로토타입은 검증 작업을 여러 개의 작은 작업으로 분해하고, 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.