VCoT-Lift

研究发现：大型语言模型在 Rust 验证方面的推理能力不及定理证明器

研究人员开发了 VCoT-Lift 框架，旨在评估大型语言模型（LLMs）在执行 Rust 程序验证方面的能力。该框架将低级求解器推理转化为人类可读的验证步骤，创建了明确的验证思维链。在此基础上，他们推出了 VCoT-Bench 基准测试，包含 1,988 个任务，用于评估 LLMs 在证明完整性和类型等多个维度上对整个验证过程的理解。对十个最先进模型的初步评估显示出显著的脆弱性，表明当前 LLMs 尚未具备在此任务上媲美自动定理证明…