用可读的推理链评估大模型在Rust验证中的逻辑能力
Can LLMs Reason Like Automated Theorem Provers for Rust Verification? VCoT-Bench: Evaluating via Verification Chain of Thought
- 将底层求解器推理转化为人类可读的验证推理链
- 构建1988个任务的基准，多维度测试模型表现
- 发现现有大模型在复杂验证中严重脆弱，远不如自动定理证明器
随着大型语言模型在安全软件开发中日益普及，其是否能满足Rust程序验证的严格要求仍不明确。现有评估将Rust验证视为黑箱，仅通过证明提示的通过/失败二分类判断模型表现，掩盖了模型对非平凡Rust代码验证所需逻辑推导的真实理解。为此，我们提出VCoT-Lift框架，将低层求解器推理提升为高层、可读的验证步骤。通过显式呈现求解器级推理作为验证思维链（Verification Chain-of-Thought），VCoT-Lift提供了细粒度评估的可靠基准。基于此，我们构建VCoT-Bench，一个包含1,988个验证思维链补全任务的综合性基准，用于严谨评估大模型对完整验证过程的理解。该基准从三个正交维度衡量性能：对不同缺失证明程度的鲁棒性、对多种证明类型的能力覆盖、以及对证明位置变化的敏感性。对十种先进模型的评估显示，当前模型存在严重脆弱性，远未达到自动化定理证明器所展现的推理能力。
原文摘要 · Abstract (English)
As Large Language Models (LLMs) increasingly assist secure software development, their ability to meet the rigorous demands of Rust program verification remains unclear. Existing evaluations treat Rust verification as a black box, assessing models only by binary pass or fail outcomes for proof hints. This obscures whether models truly understand the logical deductions required for verifying nontrivial Rust code. To bridge this gap, we introduce VCoT-Lift, a framework that lifts low-level solver reasoning into high-level, human-readable verification steps. By exposing solver-level reasoning as an explicit Verification Chain-of-Thought, VCoT-Lift provides a concrete ground truth for fine-grained evaluation. Leveraging VCoT-Lift, we introduce VCoT-Bench, a comprehensive benchmark of 1,988 VCoT completion tasks for rigorously evaluating LLMs' understanding of the entire verification process. VCoT-Bench measures performance along three orthogonal dimensions: robustness to varying degrees of missing proofs, competence across different proof types, and sensitivity to the proof locations. Evaluation of ten state-of-the-art models reveals severe fragility, indicating that current LLMs fall well short of the reasoning capabilities exhibited by automated theorem provers.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。