LLM 能像自动定理证明器一样进行 Rust 验证推理吗？VCoT-Bench：通过验证思维链进行评估

随着大语言模型辅助安全软件开发，其满足 Rust 程序严格验证需求的能力尚不明确。现有评估将验证视为黑盒，仅关注二元结果，掩盖了模型对逻辑推导的理解程度。为此，本文提出 VCoT-Lift 框架，将底层求解器推理提升为人类可读的验证步骤，显式呈现“验证思维链”作为细粒度评估的真值基准。基于此构建的 VCoT-Bench 包含 1988 个任务，从证明缺失鲁棒性、证明类型能力及位置敏感性三个维度评估模型。结果显示当前 LLM 在此类推理任务上表现脆弱，远不及自动定理证明器。