AutoVerus: Automated Proof Generation for Rust Code

• URL: http://arxiv.org/abs/2409.13082v2
• Date: Sat, 08 Feb 2025 01:06:56 GMT
• Title: AutoVerus: Automated Proof Generation for Rust Code
• Authors: Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu,
• Abstract summary: AutoVerus uses large language model (LLM) to automatically generate correctness proof for Rust code. Our evaluation shows that AutoVerus can automatically generate correct proof for more than 90% of them.
• Score: 25.56534570237484
• License:
• Abstract: Generative AI has shown its values for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generation. In this paper, we present AutoVerus. AutoVerus uses LLM to automatically generate correctness proof for Rust code. AutoVerus is designed to match the unique features of Verus, a verification tool that can prove the correctness of Rust code using proofs and specifications also written in Rust. AutoVerus consists of a network of LLM agents that are crafted and orchestrated to mimic human experts' three phases of proof construction: preliminary proof generation, proof refinement guided by generic tips, and proof debugging guided by verification errors. To thoroughly evaluate AutoVerus and help foster future research in this direction, we have built a benchmark suite of 150 non-trivial proof tasks, based on existing code-generation benchmarks and verification benchmarks. Our evaluation shows that AutoVerus can automatically generate correct proof for more than 90% of them, with more than half of them tackled in less than 30 seconds or 3 LLM calls.

Related papers

• Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  We propose ProofAug, a novel theorem proving method that enjoys superior sample efficiency. Our method is validated on the miniF2F-test benchmark using the open-source deepseek-math-7b-base model and the Isabelle proof assistant.
  arXiv  Detail & Related papers  (2025-01-30T12:37:06Z)
• AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement [25.80131224070207]
  We aim to use formal verification to provide mathematical guarantees that the generated code is correct. generating formally verified code with LLMs is hindered by the scarcity of training data and the complexity of formal proofs. We introduce AlphaVerus, a self-improving framework that bootstraps formally verified code generation.
  arXiv  Detail & Related papers  (2024-12-09T03:22:35Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  We introduce SAFE, a novel framework that overcomes the lack of human-written proof to enable automated proof generation of Rust code. We demonstrate superior efficiency and precision compared to GPT-4o. This advancement leads to a significant improvement in performance, achieving a 70.50% accuracy rate in a benchmark crafted by human experts.
  arXiv  Detail & Related papers  (2024-10-21T08:15:45Z)
• Generating Unseen Code Tests In Infinitum [1.0674604700001968]
  We present a method for creating benchmark variations that generalize across coding tasks and programming languages. We implement one benchmark, called textitauto-regression, for the task of text-to-code generation in Python.
  arXiv  Detail & Related papers  (2024-07-29T08:11:20Z)
• AutoDetect: Towards a Unified Framework for Automated Weakness Detection in Large Language Models [95.09157454599605]
  Large Language Models (LLMs) are becoming increasingly powerful, but they still exhibit significant but subtle weaknesses. Traditional benchmarking approaches cannot thoroughly pinpoint specific model deficiencies. We introduce a unified framework, AutoDetect, to automatically expose weaknesses in LLMs across various tasks.
  arXiv  Detail & Related papers  (2024-06-24T15:16:45Z)
• Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models [54.14602121129874]
  We introduce AutoIF, the first scalable and reliable method for automatically generating instruction-following training data. AutoIF transforms the validation of instruction-following data quality into code verification.
  arXiv  Detail & Related papers  (2024-06-19T13:29:53Z)
• miniCodeProps: a Minimal Benchmark for Proving Code Properties [22.548472305010005]
  We present miniCodeProps, a benchmark of 201 program specifications in the Lean proof assistant. Despite its simplicity, miniCodeProps is sufficient to break current LLM-based provers.
  arXiv  Detail & Related papers  (2024-06-16T21:11:23Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  We present a holistic end-to-end solution for annotating the factuality of large language models (LLMs)-generated responses. We construct an open-domain document-level factuality benchmark in three-level granularity: claim, sentence and document. Preliminary experiments show that FacTool, FactScore and Perplexity are struggling to identify false claims.
  arXiv  Detail & Related papers  (2023-11-15T14:41:57Z)
• Teaching Large Language Models to Self-Debug [62.424077000154945]
  Large language models (LLMs) have achieved impressive performance on code generation. We propose Self- Debugging, which teaches a large language model to debug its predicted program via few-shot demonstrations.
  arXiv  Detail & Related papers  (2023-04-11T10:43:43Z)
• Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
  We use large language models, trained on natural language text and code and fine-tuned on proofs, to generate whole proofs for theorems at once. We combine this proof generation model with a fine-tuned repair model to repair generated proofs, further increasing proving power. We evaluate our method in a prototype, Baldur, and evaluate it on a benchmark of 6,336 Isabelle/HOL theorems and their proofs.
  arXiv  Detail & Related papers  (2023-03-08T22:00:15Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.