智能体代码推理：通过半形式化结构化推理提升无执行语义代码分析 Agentic Code Reasoning
提出半形式化推理模板，无需执行代码即可完成补丁验证、故障定位和代码问答。
前置知识
智能体代码推理（Agentic Code Reasoning）
智能体代码推理是指 LLM 智能体在不执行代码的前提下，通过浏览代码仓库、追踪依赖关系、迭代收集上下文信息，对代码进行深度语义分析的能力。与传统的单次推理不同，智能体可以主动探索代码库，读取文件、搜索定义、追踪函数调用链，逐步构建对代码行为的理解。这种能力对于代码审查、补丁验证、bug 检测等场景至关重要，因为相关上下文往往分散在多个文件中。智能体通常配备 bash 工具，可以在最大步数限制内（本文设为 100 步）自由探索仓库。
这是本文研究的核心能力定义，理解智能体与单次推理的区别是理解后续所有实验设计和结果对比的基础。
半形式化推理（Semi-formal Reasoning）
半形式化推理是本文提出的核心方法，它介于完全非结构化推理和完全形式化验证之间。具体来说，它通过在 prompt 中嵌入结构化模板，要求智能体按步骤填写：首先列出显式前提（Premises），然后针对每个测试用例追踪执行路径（Execution Traces），最后得出形式化结论（Formal Conclusion）。模板充当“证书”的角色——智能体不能跳过任何步骤或做出未经证据支持的声明。这种方法不需要将代码翻译成 Lean 或 Coq 等形式化语言，而是在自然语言框架内引入结构约束，迫使智能体在得出结论前收集充分证据。
这是论文的技术核心创新，理解半形式化推理的机制和它与标准推理、完全形式化验证的区别，是理解所有实验结果为何显著提升的关键。
补丁等价验证（Patch Equivalence Modulo Tests）
补丁等价验证定义为：给定两个针对同一任务规范的代码补丁，判断它们是否产生相同的测试结果。形式化地说，两个补丁在测试意义下等价，当且仅当对两个补丁分别执行仓库的测试套件（包括 F2P 和 P2P 测试），产生的通过/失败结果完全一致。其中 F2P（Fail-to-Pass）测试是随 bug 修复引入的测试，在修复前失败、修复后通过；P2P（Pass-to-Pass）是回归测试，确保修复不破坏已有功能。这个问题之所以重要，是因为它提供了无需人工标注的客观真值（通过测试执行确定），同时具有实际应用场景。
这是论文的主要评估任务，理解其定义和评估方式是理解实验设计和结果解读的核心。
SWE-bench-Verified
SWE-bench-Verified 是一个广泛使用的软件工程基准测试集，包含来自真实世界开源项目的 bug 修复实例。每个实例包括问题描述、代码补丁、测试补丁和执行结果。社区贡献了大量智能体轨迹、生成的补丁和测试执行结果。本文从中构建评估数据集，利用其测试执行结果作为补丁等价性的真值标注。
这是论文补丁等价验证任务的主要数据来源，理解其构成有助于评估实验结果的可靠性和代表性。
RubberDuckBench
RubberDuckBench 是一个代码理解基准，包含 15 个跨 Python、Java 和 C++ 仓库的代码理解问题，每个问题配有专家编写的评分标准（rubric）。与补丁等价不同，代码问答需要自由形式的答案，通过 LLM 评分器（Gemini-3-Pro 和 GPT-5.2）基于评分标准进行评估，评分器间一致性达到 85%。
这是论文三个评估任务之一，理解其评估方式有助于对比不同任务间的推理效果差异。
Defects4J
Defects4J 是一个来自真实世界 Java 项目的可复现 bug 集合，广泛用于评估故障定位和程序修复技术。每个 bug 包含有 bug 和修复后的代码版本，以及至少一个暴露该 bug 的失败测试。故障定位任务是在仅有失败测试的情况下，不借助堆栈跟踪、错误信息或执行信息，定位精确的 bug 代码行。评估指标为 Top-N 准确率：bug 的所有 ground-truth bug 行是否被包含在前 N 个预测中。
这是论文的另一个重要评估基准，理解其任务设定和评估指标对理解故障定位实验结果至关重要。
研究动机
现有代码验证方法存在一个根本性矛盾：无执行验证方法依赖非结构化推理，允许模型在没有明确证据支持的情况下对代码行为做出断言。例如，SWE-RM 训练奖励模型来近似测试结果，Agentic Rubrics 将验证分解为 LLM 生成的标准，CodeJudge 直接使用 LLM 作为评估器——但这些方法都使用非结构化推理，模型可以跳过情况或做出未经验证的声明。另一方面，完全形式化验证（如 Lean、Coq、Datalog）虽然能提供自动化证明检查，但需要形式化语言语义，这对于跨多个框架和语言的任意仓库代码来说是不切实际的。Sultan 等人的研究明确指出这一差距：LLM 可以以有竞争力的准确率预测程序属性（如终止性），但往往无法提供有效证明。此外，现有方法往往是任务特定的，需要为每个问题域单独设计架构或训练。
本文的目标是本文的具体目标是研究 LLM 智能体能否在不执行代码的情况下，通过探索代码库来对代码语义进行推理。作者将这种能力称为“智能体代码推理”，并希望找到一种通用的方法来提升这种推理能力，使其在补丁等价验证、故障定位和代码问答三个不同任务上都表现更好。更具体地说，对于补丁等价验证，目标是实现接近可用于 RL 训练流水线中作为无执行奖励信号的可靠性水平，从而避免昂贵的沙箱执行开销。
与已有工作不同的是，本文的独特切入角度是引入“半形式化推理”——一种结构化的提示方法，要求智能体构建显式前提、追踪执行路径并得出形式化结论。与非结构化思维链推理不同，半形式化推理充当“证书”：智能体不能跳过情况或做出未经支持的声明。与完全形式化方法不同，它不需要翻译代码到形式化语言，而是保持在自然语言框架内。这种“中间路线”的核心洞察是：通过结构化推理过程（而不仅仅是输出格式），迫使智能体在得出结论前收集证据，防止非约束推理中常见的过早判断。实验表明，这种结构化自然促进了过程间推理，因为智能体必须追踪函数调用来证明其声明。
核心方法
方法的整体思路是通过在 prompt 中嵌入任务特定的结构化模板，约束 LLM 智能体的推理过程，使其必须遵循严格的步骤：首先声明前提条件，然后逐步追踪执行路径，最后给出形式化结论。直觉上，这就像给一个学生一份结构化的解题模板——你不能直接跳到答案，必须先写出已知条件、推理过程和结论。技术路线上，作者设计了三种任务特定的模板（补丁等价、故障定位、代码问答），每个模板都包含 DEFINITIONS（定义）、PREMISES（前提）、ANALYSIS（分析）和 FORMAL CONCLUSION（形式化结论）等强制部分。智能体使用 SWE-agent 的 bash 工具接口在最多 100 步内探索代码仓库，但不能执行仓库代码或运行测试套件——只能进行静态分析（允许运行独立 Python 脚本探究通用语言行为）。
核心创新点在于将结构化施加在推理过程而非仅仅输出格式上。已有方法如 Chain-of-Thought 关注中间推理步骤，ReAct 将推理与行动结合，CodeAct 使用可执行代码动作——但这些都没有对推理内容施加结构约束。半形式化推理的本质区别是：模板充当“证书”，强制智能体按指定格式填充每个字段，从而确保推理的完备性。在 Django django-13670 的例子中，标准推理假设 format() 是 Python 内置函数，直接得出两个补丁等价的错误结论；而半形式化推理要求追踪函数定义，发现 format 被模块级函数遮蔽，期望 datetime 而非 int 参数，从而发现补丁 1 会抛出 AttributeError。这种“不能跳步”的约束是与已有方法的根本区别。
方法步骤详情
方法分为三个层次：（1）智能体设置：使用最小化 SWE-agent 配置，配备 bash 工具，最大步数 100 步，不能执行仓库代码或运行测试，禁用 Git 命令以防止查看提交历史，但允许运行独立 Python 脚本探究通用语言行为。（2）标准推理基线：智能体收到最小化 prompt，要求判断等价性，无结构约束，用自然语言解释推理后以 YES/NO 结论。（3）半形式化推理：智能体收到包含结构化证书模板的 prompt，模板要求填写：DEFINITIONS（定义关键概念）、PREMISES（声明每个补丁的修改内容和测试行为）、ANALYSIS OF TEST BEHAVIOR（对每个测试追踪执行路径并比较结果）、COUNTEREXAMPLE（如不等价则提供具体代码追踪证据）、FORMAL CONCLUSION（基于定义和分析得出结论）。模板中每个方括号字段都必须用从代码库收集的证据填充。三个任务的模板结构相同但内容任务特定：补丁等价关注测试行为追踪，故障定位关注可疑代码区域和失败原因分析，代码问答关注函数追踪表、数据流分析和语义属性。
技术新颖性
技术新颖性体现在多个层面。首先，这是首个系统研究“智能体代码推理”能力的工作——将智能体的代码探索能力与语义推理能力结合评估。其次，半形式化推理作为一种结构化提示方法，与已有工作的区别在于它对推理过程施加约束而非仅仅结构化输出。与 SWE-RM（训练奖励模型）、Agentic Rubrics（LLM 生成评判标准）、CodeJudge（LLM 作为评判器）等无执行验证方法不同，本文不需要额外训练或专用架构。与 Lean、Coq 等完全形式化方法不同，本文保持在自然语言层面，无需形式化语言语义。此外，方法的通用性也是新颖之处——同一套结构化推理范式在三个差异很大的任务上都带来一致提升，表明这种方法捕捉了某种更深层的推理改进机制。
实验结果
实验结果表明半形式化结构化推理在所有三个任务上都带来了一致且显著的提升。在补丁等价验证（精选数据集，170 个困难样本）上，Opus-4.5 的准确率从标准推理的 78.2% 提升到半形式化的 88.8%，错误减少近一半，非等价准确率 82.9%，等价准确率 93.0%，但需要约 2.8 倍的步数（28.17 vs 10.08）。在真实世界智能体生成补丁的验证中，Opus-4.5 配合半形式化推理达到 93.0% 准确率，超过单次调用的 86.0% 和 difflib 的 73%，接近可作为无执行 RL 奖励信号的可靠性水平。在 RubberDuckBench 代码问答上，Opus-4.5 从标准推理的 78.3% 提升到半形式化的 87.0%（+8.7pp），但 Sonnet-4.5 的提升较小（84.2% to 84.8%），表明结构化推理的收益可能随模型能力提升而饱和。在 Defects4J 故障定位上，半形式化推理在全部命中指标下 Top-5 准确率提升 +12pp（小规模 50 bug）和 +5pp（大规模 100 bug），在任意命中指标下 Top-5 达到 88.4%。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 补丁等价验证（精选数据集） | 整体准确率 | 88.8%（Opus-4.5 半形式化） | 78.2%（Opus-4.5 标准推理） | +10.6pp，错误减少近一半 |
| 补丁等价验证（真实世界补丁） | 验证准确率 | 93.0%（Opus-4.5 半形式化） | 86.0%（Opus-4.5 单次调用）；73%（difflib） | +7pp vs 单次调用；+20pp vs difflib |
| 代码问答（RubberDuckBench） | 准确率 | 87.0%（Opus-4.5 半形式化） | 78.3%（Opus-4.5 标准推理）；76.2%（单次） | +8.7pp vs 标准推理；+10.8pp vs 单次 |
| 故障定位（Defects4J，小规模 43 bugs） | Top-5 All 准确率 | 72.1%（Opus-4.5 半形式化 + 智能体） | 60.5%（Opus-4.5 标准推理 + 智能体） | +11.6pp |
| 故障定位（Defects4J，大规模 90 bugs） | Top-5 All 准确率 | 47.8%（Opus-4.5 半形式化） | 43.3%（Opus-4.5 标准推理） | +4.5pp |
局限与改进
论文坦承了多个局限性。在补丁等价验证中，19 个错误案例的主要原因是非等价情况下遗漏执行差异——智能体声称补丁等价，但实际上只有一个能通过测试，通常因为未能追踪所有相关代码路径或遗漏测试中的断言。在故障定位中，识别了四类主要失败模式：（1）间接 bug——bug 不在测试直接调用的类中（如 Csv_12 的 bug 在配置类 CSVFormat.withHeader() 中而非 CSVParser.parse()）；（2）多文件 bug——跨越多个文件的 bug 需要同时识别所有位置；（3）领域特定 bug——需要专门知识的算法 bug（如 Math_81 的特征值分解）超出模型领域专长；（4）超过 5 个修复区域的 bug。数据污染问题也被承认——SWE-bench 实例可能出现在 LLM 训练语料中，但作者指出主要结论基于相对比较（相同模型不同推理格式的消融），污染对所有配置影响相同。此外，93% 的准确率虽高但仍不完美，作为 RL 奖励信号仍可能引入噪声。从独立观察来看，方法的计算成本（2.8 倍步数增加）在大规模应用中可能成为瓶颈，且模板设计需要针对每个新任务定制，泛化到全新任务类型需要额外工作。
独立分析的弱点
论文存在几个值得关注的弱点。首先，计算开销显著——半形式化推理需要约 2.8 倍的步数（精选数据集中从 10.08 步增加到 28.17 步），在真实世界验证中从 19.7 步增加到 37.82 步，这在大规模部署（如 RL 训练流水线中作为奖励信号）时可能导致严重的成本和延迟问题，改进方向包括研究模板压缩或自适应结构化程度。其次，模板设计是手工的且任务特定的，每个新任务需要领域专家设计合适的模板结构，改进方向包括自动模板生成或学习最优结构。第三，Sonnet-4.5 在代码问答上未从半形式化推理获益（84.2% to 84.8%），表明方法效果依赖模型能力，较弱模型可能无法有效利用结构化约束。第四，故障定位在大规模评估中提升较小（+5pp），可能因为模板对复杂间接 bug 的帮助有限。第五，评估仅覆盖三种任务类型，对安全漏洞检测、API 误用检测等其他静态分析任务的效果未知。
未来方向
作者提出了三个明确的未来方向：（1）代码推理后训练——微调模型以内化半形式化模板结构，可能在消除 prompt 开销的同时进一步提升准确率；（2）扩展到其他静态分析任务——半形式化推理方法可应用于安全漏洞检测、代码异味识别、API 误用检测等；（3）混合验证——将 LLM 推理与轻量级形式化方法或符号执行结合，在保持灵活性的同时提供更强保证。基于现有成果，还可延伸出以下方向：（4）动态难度自适应——根据代码复杂度自动调整推理模板的详细程度，在简单案例中节省步数、在复杂案例中加强约束；（5）多智能体协作——多个智能体分别负责不同推理阶段（前提收集、执行追踪、结论验证），可能提升推理质量；（6）跨语言泛化研究——系统评估方法在不同编程语言和框架上的效果差异；（7）将 93% 的验证准确率与执行验证结合，形成混合验证流水线，仅在模型不确定时触发实际执行。
复现评估
论文提供了足够的信息支持复现。实验基于公开可用的数据集（SWE-bench-Verified、Defects4J、RubberDuckBench）和开源智能体框架（SWE-agent），prompt 模板在附录中给出。然而，使用了闭源模型（Opus-4.5、Sonnet-4.5、Gemini-3-Pro、GPT-5.2），开源模型的复现效果需要额外验证。数据集构建过程描述清晰（从 SWE-bench-Verified 中按相似度评分和平衡策略抽取 170 个困难样本），但精选数据集本身未公开发布。Defects4J 评估中通过限制 token 数（100K）确保代码在上下文窗口内，这提供了可复现的条件。总体而言，方法复现难度中等——核心是 prompt 工程，不需要额外训练或专用基础设施，但闭源模型 API 访问和数据集构建的随机性可能影响精确结果复现。
论文图表
展示了 Django 中一个补丁等价验证的动机示例。两个补丁都试图修复年份格式化问题：补丁 1 使用 format(self.data.year, '04d')[-2:]，补丁 2 使用 '%02d' % (self.data.year % 100)。标准推理错误地假设 format() 是 Python 内置函数，得出两个补丁等价的结论。半形式化推理追踪了实际函数定义，发现 format 被 Django dateformat.py 中的模块级函数遮蔽，该函数期望 datetime 对象而非整数，导致补丁 1 抛出 AttributeError 而补丁 2 成功。
这张图是理解半形式化推理核心价值的关键——它直观展示了标准推理如何因假设而犯错，以及结构化推理如何通过追踪实际代码定义来发现隐藏的语义差异。