VCoT-Bench: Can LLMs Reason Like Automated Theorem Provers for Rust Verification?¶

日期: 2026-03-18
arXiv: 2603.18334
领域: LLM推理/形式验证
关键词: 自动定理证明, Rust验证, 思维链, 形式推理, Verus, 评估基准

一句话总结¶

通过 VCoT-Lift 框架将 Z3 求解器的低层推理提升为高层 Verus 验证步骤，构造 1,988 道涵盖缺失度/类型/位置三维度的 VCoT 完成任务，评估 10 个 SOTA LLM 发现即使最强模型在 10% 缺失率下仅 ~77% 准确率，100% 缺失接近崩溃（~17%）。

领域现状: 现有 Rust 验证 LLM 工作（AlphaVerus、AutoVerus、SAFE、RagVerus、VeriStruct 等）仅评估二进制"验证成功/失败"，无法区分真实理解还是靠句法对齐碰巧成功。
现有痛点: Z3 证明的人类可读性极差——36 种规则，10K+ 行中 81.69% 是平凡推理（如 \(x=x\) 自反性），真正逻辑步骤被淹没。直接用于评估不可行。
核心矛盾: 二进制评估无法区分"真正理解验证逻辑"和"碰巧生成了可通过的代码"——一个猜对答案的学生和一个真正理解的学生得到相同分数。形式验证的严谨性需要更精细的评估维度。
切入角度: 类比 NLP 中的思维链（CoT）评估——不只看最终答案对不对，还要看推理过程是否正确。将此思路迁移到形式验证领域：暴露验证器的内部推理过程，构建"验证思维链"。
核心 idea: 受 NLP CoT 启发，将求解器推理暴露为显式的、人类可读的验证步骤（VCoT），构建形式验证版本的思维链评估基准——通过"挖洞"让模型补全缺失的验证步骤。

证明转换器 (Proof Transformer):
- 做什么：将 Z3 低层推理转换为 Verus 高层验证步骤
- 核心思路：引入 Z3 规则层次结构（8 条高层/12 条中层/16 条低层），引导 LLM 聚焦于高层规则（如 unit-resolution）中的语义信息性步骤，忽略低层平凡推理
- 设计动机：Z3 证明全局互连，无法简单分解——必须端到端处理，但规则层次结构显式引导注意力
证明检查器 (Proof Checker): 5 个专用 agent（lemma/theory-lemma/modus-ponens/quantifier/unit-resolution）做局部验证——按规则类别聚合 Z3 证明片段批量检查，既避免冗余 LLM 调用又保持完整性
转换-检查循环: 迭代直到检查器判定完整——每轮转换器生成 + 检查器验证，不完整处触发下一轮补全
证明修剪 + 修复: 移除冗余步骤（如平凡的 0=0 断言）+ Verus 编译器反馈迭代修复语法/语义错误——确保简洁性和正确性

缺失率	10%	20%	40%	60%	100%
平均准确率	63.4%	58.2%	42.1%	28.3%	8.7%