用智能体提升大模型验证Rust系统代码正确性的能力
VeruSAGE: A Study of Agent-Based Verification for Rust Systems
- 设计智能体系统匹配不同大模型特性，提升代码验证效率
- 最优组合完成超80%的验证任务，部分未完成任务也超90%
- 适合对系统安全和形式化验证感兴趣的开发者与研究者
大语言模型在理解和编写代码方面表现出色，但在严格推理和证明代码正确性方面仍存疑。本文系统研究了大模型在Rust系统软件上构建正确性证明的能力。我们构建了一个新的系统验证基准集VeruSAGE-Bench，包含从8个已用Verus验证的Rust系统中提取的849个证明任务。针对o4-mini、GPT-5、Sonnet 4和Sonnet 4.5等不同大模型，设计适配其特性的智能体系统。研究表明，需根据不同模型特性配置相应工具与智能体设置。最佳组合在VeruSAGE-Bench上完成超过80%的任务，并在一组未被人类专家完成的系统证明任务中完成超过90%。结果表明，大模型辅助开发可验证系统软件具有巨大潜力。
原文摘要 · Abstract (English)
Large language models (LLMs) have shown impressive capability to understand and develop code. However, their capability to rigorously reason about and prove code correctness remains in question. This paper offers a comprehensive study of LLMs' capability to develop correctness proofs for system software written in Rust. We curate a new system-verification benchmark suite, VeruSAGE-Bench, which consists of 849 proof tasks extracted from eight open-source Verus-verified Rust systems. Furthermore, we design different agent systems to match the strengths and weaknesses of different LLMs (o4-mini, GPT-5, Sonnet 4, and Sonnet 4.5). Our study shows that different tools and agent settings are needed to stimulate the system-verification capability of different types of LLMs. The best LLM-agent combination in our study completes over 80% of system-verification tasks in VeruSAGE-Bench. It also completes over 90% of a set of system proof tasks not part of VeruSAGE-Bench because they had not yet been finished by human experts. This result shows the great potential for LLM-assisted development of verified system software.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。