部署 AI 代理进行代码库级别的任务——漏洞检测、补丁验证、代码审查——面临重大技术障碍。主要瓶颈之一是需要为每个代码库设置动态执行沙箱，成本高昂且计算繁重。使用大语言模型推理替代代码执行虽然流行，但经常导致无根据的猜测和幻觉。

Meta 研究人员提出”半形式化推理”（semi-formal reasoning），一种结构化提示技术，要求 AI 代理在回答前填写逻辑证书：明确陈述前提、追踪具体执行路径、推导形式化结论。

填补空白：介于猜测与证明之间

当前执行无关代码验证主要有两种方法。第一种是使用非结构化 LLM 评估器，让模型直接验证代码或训练专门的奖励模型近似测试结果。主要缺陷是依赖非结构化推理，允许模型做出自信的主张而无需明确论证。

第二种是形式化验证，将代码或推理翻译为 Lean、Coq 或 Datalog 等形式化数学语言进行自动证明检查。虽然严谨，但对于跨越多框架多语言的企业代码库来说完全不切实际。

Meta 的半形式化推理填补了这一空白。结构化模板作为强制性逻辑证书，代理必须在做出判断前从代码库收集证据，实际跟随函数调用和数据流逐步追踪，而非仅凭函数名称等表面模式猜测。

实验验证：显著提升准确性

研究人员在三个软件工程任务上评估了半形式化推理：补丁等效验证（判断两个补丁是否产生相同测试结果）、故障定位（精确定位导致漏洞的代码行）和代码问答（测试复杂代码库的语义理解）。

实验使用 Claude Opus-4.5 和 Sonnet-4.5 模型作为自主验证代理。在补丁等效任务中，半形式化推理将挑战性样本的准确率从标准推理的 78% 提升至 88%。在真实世界代理生成补丁评估中，Opus-4.5 模型达到 93% 的验证准确率，超越非结构化单次基线的 86% 和 difflib 基线的 73%。

论文通过一个真实案例展示了半形式化推理的价值：在 Python Django 仓库中评估两个修复公元 1000 年前两位数年份格式错误的补丁。标准推理模型假设 format() 指的是 Python 内置函数，错误判定两个补丁等效；半形式化推理代理追踪执行路径后发现，库文件中 format() 名称被自定义模块级函数覆盖，正确识别出一个补丁会导致崩溃。

权衡与局限

虽然半形式化推理显著提升可靠性，但企业开发者需考虑几个实际权衡：

计算与延迟成本增加。半形式化推理需要更多 API 调用和 token，在补丁等效评估中，执行步骤约为标准非结构化推理的 2.8 倍。

对模型已高度擅长的任务提升有限。当 Sonnet-4.5 在代码问答基准上使用标准推理已达到约 85% 准确率时，应用半形式化模板没有额外收益。

结构化推理可能产生高度自信的错误答案。代理可能构建详尽但完整的证据链，却因调查深入但不完整而得出错误结论。

当代码库边界触及第三方库时，系统仍需依赖函数名称猜测行为。

开箱即用，无需训练

这项技术的关键优势是可直接使用，无需模型训练或特殊封装。研究人员建议，结构化代理推理可能提供”经典静态分析工具的灵活替代方案：无需将分析逻辑编码为专门算法，只需用任务特定的推理模板提示 LLM 代理，即可跨语言和框架泛化。”

研究团队已公开提示模板，可立即集成到应用中。在大量讨论提示工程已死的背景下，这项技术展示了精心设计的提示仍能挖掘多少性能潜力。