Leveraging Large Language Models for Automated Proof Synthesis in Rust

2023-11-07 · Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui

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.

📄 PDF Abstract BibTeX arXiv:2311.03739

Code (0)

등록된 구현이 없습니다.

Methods 이 논문이 사용한 방법론

Attention 설명 없음

Label Smoothing Label Smoothing is a regularization technique that introduces noise for the labels. This accounts for the fact that datasets may have mistakes in them, so maximizing the…

Linear Layer A Linear Layer is a projection $\mathbf{XW + b}$.

Absolute Position Encodings Absolute Position Encodings are a type of position embeddings for [Transformer-based models] where positional encodings are…

Residual Connection 설명 없음

Multi-Head Attention 설명 없음

BPE Byte Pair Encoding, or BPE, is a subword segmentation algorithm that encodes rare and unknown words as sequences of subword units. The intuition is that various word…

Dropout Dropout is a regularization technique for neural networks that drops a unit (along with connections) at training time with a specified probability $p$ (a common value is…

Proof2Silicon: Prompt Repair for Verified Code and Hardware Generation via Reinforcement Learning

2025-09-07 · Manvi Jha, Jiaxin Wan, Deming Chen arxiv

Large Language Models (LLMs) have demonstrated impressive capabilities in automated code generation but frequently produce code that fails formal verification, an essential requirement for hardware and safety-critical do…

Reinforcement Learning Code Generation

Automated Proof Generation for Rust Code via Self-Evolution

2024-10-21 · Tianyu Chen, Shuai Lu, Shan Lu, Yeyun Gong 외

Ensuring correctness is crucial for code generation. Formal verification offers a definitive assurance of correctness, but demands substantial human effort in proof construction and hence raises a pressing need for autom…

Code Generation

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

2024-12-18 · Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher 외

Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual effort to write proofs. Recent work has …

Retrieval

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs

2025-08-21 · Terry Jingchen Zhang, Wenyuan Jiang, Rongchuan Liu, Yisong Wang 외 arxiv

Formal theorem proving (FTP) has emerged as a critical foundation for evaluating the reasoning capabilities of large language models, enabling automated verification of mathematical proofs at scale. However, progress has…

Automated Theorem Proving Arithmetic Reasoning

LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation

2025-05-17 · Junyu Lai, Jiakun Zhang, Shuo Xu, Taolue Chen 외

Recent advancements in large language models (LLMs) have sparked considerable interest in automated theorem proving and a prominent line of research integrates stepwise LLM-based provers into tree search. In this paper, …

Automated Theorem Proving Synthetic Data Generation