[LG]《Towards Verified Code Reasoning by LLMs》M Sistla, G Balakrishnan, P Rondon, J Cambronero... [University of Texas at Austin & Google DeepMind] (2025)
代码推理的信任难题如何破解？新研究用形式验证为大语言模型（LLM）推理护航，提升软件工程效率与安全。
• LLM擅长代码理解与推理，但易犯三类错误：错误的代码语义假设、未全面考虑问题细节、对库函数行为的无根据假设。
• 提出自动验证框架：将LLM回答转化为形式化谓词（AgentClaims），再用程序分析与形式验证工具验证推理正确性（VerificationCondition）。
• 针对未初始化变量错误，验证步骤成功确认13/20例；针对程序等价查询，准确捕获6/8错误推理，验证LLM输出的可靠性显著提高。
• 形式化谓词设计涵盖数据流、控制依赖、表达式与库函数调用，结合迭代生成缺失谓词，确保语义表达全面且精炼。
• 面对复杂代码，LLM辅助检索相关片段，进行“隐式切片”，降低静态分析保守性与复杂度。
• 验证器具备极高精准度，虽召回率有限，但可通过多次提取与迭代完善大幅提升验证覆盖率。
• 研究揭示：LLM推理虽强，但需要形式验证“后验把关”防止幻觉误导，实现更可信的代码辅助开发。
• 未来方向包括优化谓词设计、改进提示词、引入更强验证器、以及训练LLM生成更易验证的推理过程。
心得：
1. 代码语义的微妙差异常被忽视，形式化表达是避免误判的关键。
2. LLM具备高效语境切片能力，结合形式验证能大幅提升代码审查与等价判断的准确性。
3. 自动验证虽不能完全取代人类，但能显著降低人工复核成本，提升开发效率与软件质量。
了解详情🔗 arxiv.org/abs/2509.26546
大语言模型代码推理形式验证程序等价软件工程
