Meta研究人员提出了一种名为“半形式化推理”（semi-formal reasoning）的结构化提示技术，可显著提升大语言模型在代码审查任务中的准确率——在某些情况下达到93%。这一方法不需要模型训练或额外工具，只需精心设计的提示模板。

为什么需要这项技术？

在代码库级别部署AI代理进行错误检测、补丁验证和代码审查面临重大技术障碍。主要瓶颈之一是需要为每个仓库设置动态执行沙箱，这既昂贵又计算繁重。

使用大语言模型推理而非执行代码正变得越来越流行，但它经常导致无根据的猜测和幻觉。

什么是半形式化推理？

半形式化推理介于非结构化猜测和过度严格的数学证明之间。它为LLM代理配备了任务特定的结构化推理模板。

这些模板作为强制性逻辑证书。要完成任务，代理必须：

  • 明确陈述前提：清楚地说明假设和已知条件
  • 追踪执行路径：针对特定测试用例逐步跟踪代码执行
  • 推导形式化结论：仅基于可验证证据得出结论

模板强制代理在做判断之前从代码库中收集证据。代理必须实际跟踪函数调用和数据流，而不是基于表面命名约定猜测行为。

实际效果如何？

研究人员在三个软件工程任务上评估了半形式化推理：

补丁等效性验证：判断两个补丁是否产生相同的测试结果（无需运行它们）

故障定位：精确定位导致错误的具体代码行

代码问答：测试对复杂代码库的细致语义理解

实验使用Claude Opus-4.5和Sonnet-4.5模型作为自主验证代理。结果显示：

  • 在补丁等效性任务中，准确率从标准推理的78%提升到88%
  • 在真实世界代理生成补丁评估中，Opus-4.5使用半形式化推理达到93%验证准确率
  • 超越非结构化单次基线（86%）和difflib基线（73%）

一个具体案例：Django日期格式Bug

论文通过一个真实案例展示了半形式化推理的价值。在Python Django仓库中，两个补丁尝试修复公元1000年之前日期的2位数年份格式Bug。

一个补丁在库内使用自定义format()函数，覆盖了Python标准函数。

标准推理模型：查看这些补丁，假设format()指的是Python标准内置函数，计算两个方法会产生相同的字符串输出，错误地声明补丁等效。

半形式化推理：代理追踪执行路径并检查方法定义。按照结构化模板，代理发现库文件中format()名称实际上被自定义的模块级函数遮蔽。代理正式证明：给定传递给代码的输入属性，这个补丁会使系统崩溃，而另一个会成功。

权衡与局限

虽然半形式化推理提供了显著的可靠性改进，但开发者需要考虑几个实际权衡：

计算和延迟权衡：半形式化推理需要更多API调用和token。在补丁等效性评估中，它需要大约标准非结构化推理2.8倍的执行步骤。

并非普遍改进：如果模型在特定任务上已经高度熟练，半形式化推理可能没有额外收益。在代码问答基准测试中，Sonnet-4.5的标准推理已经达到约85%的准确率，应用半形式化模板没有带来额外提升。

可能产生高度自信的错误答案：因为代理被迫构建精心设计的证明链，如果调查深入但不完整，它可能变得过度自信。在一个Python评估中，代理仔细追踪了五个不同的函数来发现有效的边缘情况，但完全错过了下游代码已经安全处理了那个确切场景。

边界问题：当分析底层源代码不可用的第三方库时，代理仍会基于函数名称猜测行为。

开发者如何使用？

这项技术的一大优势是开箱即用：

  • 不需要模型训练
  • 不需要特殊打包
  • 不需要代码执行环境
  • 只需在推理时支付更多计算，获得更高准确率

研究人员已将提示模板开源，可直接集成到应用中。

写在最后

在”提示工程已死”的讨论声中，这项技术展示了精心构建的提示还能从模型中挤出多少性能。

研究人员建议：”结构化代理推理可能提供经典静态分析工具的灵活替代方案——不需要在专用算法中编码分析逻辑，我们可以用任务特定的推理模板提示LLM代理，跨语言和框架泛化。”

对于希望提升AI代码审查可靠性的开发者团队，半形式化推理提供了一个零成本、立即可用的解决方案。