用AI自动验证数据结构模块，准确率超99%
VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
- 通过智能规划自动生成抽象、不变式和证明代码
- 在11个模块中成功验证128个函数（99.2%准确率）
- 适合形式化验证与Rust开发人员快速上手
我们提出VeriStruct，一个将AI辅助自动化验证从单个函数扩展到复杂数据结构模块的新框架。VeriStruct通过规划模块系统生成抽象、类型不变式、规范和证明代码。为解决大模型常误解Verus注解语法和验证语义的问题，VeriStruct在提示中嵌入语法引导，并引入修复阶段自动纠正注解错误。在11个Rust数据结构模块上的评估显示，VeriStruct在其中10个成功完成验证，总计128个函数中成功129个（99.2%），标志着迈向全自动AI辅助形式化验证的重要一步。
原文摘要 · Abstract (English)
We introduce VeriStruct, a novel framework that extends AI-assisted automated verification from single functions to more complex data structure modules in Verus. VeriStruct employs a planner module to orchestrate the systematic generation of abstractions, type invariants, specifications, and proof code. To address the challenge that LLMs often misunderstand Verus' annotation syntax and verification-specific semantics, VeriStruct embeds syntax guidance within prompts and includes a repair stage to automatically correct annotation errors. In an evaluation on eleven Rust data structure modules, VeriStruct succeeds on ten of the eleven, successfully verifying 128 out of 129 functions (99.2%) in total. These results represent an important step toward the goal of automatic AI-assisted formal verification.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。