Meta发布半形式化推理技术提升大语言模型代码审查准确率

Meta研究人员开发了一种结构化提示技术，使大语言模型能够在不执行代码的情况下验证代码补丁，测试准确率高达93%。

这种被称为半形式化推理的方法可以帮助减少对当前自动化代码验证所需的资源密集型沙盒环境的依赖。

随着组织希望在代码库规模的任务（如错误检测和补丁验证）中部署智能体AI，这一发展应运而生。传统的基于执行的方法往往难以在大型、异构代码库中进行扩展。

该技术不是使用可能导致幻觉的自由形式推理，而是引入了结构化逻辑证书。这些证书要求模型在得出结论之前明确陈述假设并跟踪执行路径。

研究人员在三个关键任务中评估了这种方法，包括补丁等价性验证、故障定位和代码问答，发现半形式化推理在所有任务中都提高了准确性。

研究人员在论文中表示："对于补丁等价性，在精选示例上准确率从78%提高到88%，在真实世界智能体生成的补丁上达到93%，接近无执行强化学习奖励信号所需的可靠性。"

在代码问答方面，半形式化推理达到87%的准确率，比标准智能体推理提高了9个百分点。在故障定位方面，与标准方法相比，Top 5准确率提高了5个百分点。

半形式化推理介于非结构化对话和严格形式验证之间。虽然标准推理允许模型在没有证明的情况下提出声明，但这种方法使用预定义模板，要求逐步过程。

研究人员表示："我们不是训练专门的模型或形式化语义，而是用结构化推理模板提示智能体，要求为每个声明提供明确证据。"

他们补充说，"模板充当证书：智能体必须陈述前提，跟踪相关代码路径，并提供正式结论。结构化格式自然鼓励过程间推理，因为跟踪程序路径要求智能体跟随函数调用而不是猜测其行为。"

在实践中，这迫使模型像开发人员逐行检查代码一样行为。

研究人员表示，在一个涉及Django框架的案例中，结构化方法揭示了模块级函数遮蔽了Python的内置format()函数。虽然标准推理错过了这个细节，但半形式化分析正确识别了代码会失败。

分析师表示，半形式化推理标志着从辅助AI向更负责任的软件工程AI的转变，这种区别可能重塑企业处理代码审查的方式。

Greyhound Research首席分析师Sanchit Vir Gogia表示："像GitHub Copilot这样的工具已经让开发人员习惯于将AI作为快速、流畅的建议引擎进行交互。你提问，它生成，你接受或调整。系统优化速度和可信度，但它不优化证明。"

半形式化推理改变了这种动态。它不是奖励模型听起来正确，而是要求它们通过跟踪逻辑和基础结论来证明正确性。对开发人员来说，这将焦点从审查输出转移到评估其背后的推理。

Gogia说："更深层的含义是代码审查本身开始演进。历史上，代码审查一直是与知识传递和设计验证以及错误检测相关的人为瓶颈。实际上，它往往无法捕获关键问题，同时减慢集成速度。我们现在看到的是机器主导验证层的早期形态，系统跟踪逻辑，人类验证结果。"

然而，这种转变并非没有权衡。结构化推理引入了额外的计算和工作流开销，引发了如何在真实世界开发环境中部署的问题。

Gogia说："更多步骤，更多Token，更多延迟。在受控实验中，这可以通过更高的准确性来证明。在真实开发环境中，这转化为更慢的构建、更长的反馈周期和增加的基础设施支出。如果不加区别地应用这种方法，开发人员将绕过它。不是因为他们不同意，而是因为它妨碍了工作。"

还存在技术风险。研究人员指出，虽然结构化格式减少了猜测，但也可能产生"自信但错误"的答案。在这些情况下，AI构建了一个详细但不完整的推理链，将不正确的结论包装在令人信服、高度结构化的格式中，人类可能难以快速反驳。

Q&A

Q1：什么是半形式化推理技术？

A：半形式化推理是Meta开发的一种结构化提示技术，它使大语言模型能够在不执行代码的情况下验证代码补丁。该技术引入结构化逻辑证书，要求模型明确陈述假设并跟踪执行路径，迫使模型像开发人员逐行检查代码一样进行分析。

Q2：半形式化推理技术的准确率如何？

A：测试显示该技术在多个任务中都有显著提升：补丁等价性验证准确率从78%提高到88%，在真实世界智能体生成的补丁上达到93%；代码问答准确率达到87%，比标准智能体推理提高9个百分点；故障定位的Top 5准确率提高了5个百分点。

Q3：半形式化推理技术有什么局限性？

A：该技术存在两个主要局限：一是增加了计算和工作流开销，导致更慢的构建、更长的反馈周期和增加的基础设施支出；二是可能产生"自信但错误"的答案，AI可能构建详细但不完整的推理链，将错误结论包装成令人信服的格式，难以快速识别。