Rust 程序验证的 LLM 能否像自动定理证明器一样推理？VCoT-Bench：通过验证链思考进行评估
软件工程
2026-03-20 v1 人工智能
机器学习
摘要
随着大语言模型（LLM）日益助力安全软件开发，其是否满足 Rust 程序验证所需的严格要求尚不明了。现有评估将 Rust 验证视为黑盒，仅通过二元通过/失败结果评估模型，这掩盖了模型是否真正理解验证非平凡 Rust 代码所需的逻辑推演。为弥合这一差距，我们提出 VCoT-Lift 框架，将低级求解器推理提升为高层次、人类可读的验证步骤。通过将求解器级推理作为显式的验证链思考（Verification Chain-of-Thought）显露，VCoT-Lift 为细粒度评估提供了具体基准。借助 VCoT-Lift，我们引入 VCoT-Bench，一个包含 1,988 个 VCoT 完成任务的综合基准，用于严格评估 LLM 对整个验证过程的理解。VCoT-Bench 沿三个正交维度衡量性能：对不同缺失证明程度的鲁棒性、不同证明类型的胜任力以及对证明位置的敏感性。十个最新模型的评估显示严重的脆弱性，表明当前 LLM 在自动定理证明器所展现的推理能力方面远远不及。
引用
@article{arxiv.2603.18334,
title = {Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought},
author = {Zichen Xie and Wenxi Wang},
journal= {arXiv preprint arXiv:2603.18334},
year = {2026}
}