让每一项优秀工作，被更多人看见：点击进入投稿通道

• 论文标题：Agentic Code Reasoning
• 论文链接：https://arxiv.org/pdf/2603.01896

TL;DR

今天解读一篇来自 Meta 的论文《Agentic Code Reasoning》。该研究探讨了一个核心问题：大模型（LLM）智能体能否在不执行代码的情况下，通过探索代码库来推理代码的语义？研究提出了一种名为 半形式化推理（Semi-formal Reasoning） 的结构化提示方法。该方法要求智能体构建明确的前提，追踪执行路径，并推导出形式化结论，以此作为推理的“证书”（Certificate）。

实验表明，这种方法在补丁等价性验证（Patch Equivalence）、故障定位（Fault Localization）和代码问答（Code QA）三个任务上均有一致的准确率提升。特别是在补丁等价性任务中，该方法在真实世界生成的补丁上达到了 93% 的验证准确率，接近作为强化学习（RL）奖励信号所需的可靠性，且无需昂贵的沙盒执行环境。

1. 引言

在软件工程领域，尤其是涉及大型代码库的场景中，验证代码的正确性通常依赖于测试套件的执行。然而，执行代码存在诸多限制：需要配置复杂的环境、安装依赖、运行时间长，且存在安全风险。对于基于强化学习（RL）的代码生成智能体训练而言，若每次迭代都通过沙盒执行测试来获取奖励信号，计算成本极高。

因此，Agentic Code Reasoning（智能体代码推理） 应运而生。这指的是智能体在不执行代码的前提下，通过自主导航文件、追踪依赖关系和迭代收集上下文，进行深度语义分析的能力。这种能力对于漏洞检测、代码审查和补丁验证至关重要。

然而，现有的非执行验证方法存在两极分化：

1. 非结构化推理（Unstructured Reasoning）： 传统的思维链（Chain-of-Thought, CoT）允许模型自由推理，但这往往导致模型跳过关键步骤、做出无证据的断言或产生幻觉。
2. 全形式化验证（Fully Formal Verification）： 使用 Lean、Coq 或 Datalog 等形式化语言进行证明。这要求将任意代码库翻译为形式化语义，工程难度极大，且当前的 LLM 难以生成完美的证明代码。

本文提出的 半形式化推理 旨在弥合这一差距。它不要求完整的数学证明，但通过结构化的模板强制智能体显式列出证据（Evidence）和推理路径（Trace），从而提高推理的严谨性。

2. 半形式化推理

2.1 核心概念：作为证书的推理

半形式化推理的核心在于引入了 推理模板。这些模板充当了“证书”的角色，强迫智能体在得出结论之前必须完成以下步骤：

1. 陈述前提： 明确指出代码的初始状态、输入假设或已知事实。
2. 追踪路径： 模拟程序的执行流，记录函数调用链、变量状态变化。
3. 形式化结论： 基于上述前提和追踪结果，根据预定义的逻辑规则得出结论。

这种结构迫使模型进行 过程内和过程间 的分析，而不是基于函数命名或局部代码片段进行猜测。

2.2 智能体与单次推理的区别

研究区分了 单次验证 和 智能体验证：

• 单次验证： 模型仅根据静态的代码快照进行推理。
• 智能体验证： 模型可以使用工具（如 grep, find, cat 等 bash 工具）在代码库中主动探索。本文设置最大步数为 100 步。智能体不能运行代码或测试，但可以运行独立的 Python 脚本来测试语言特性（如 regex 行为）。

2.3 结构化模板设计

针对不同的任务，模板的具体内容有所不同，但遵循相同的逻辑框架。

2.3.1 补丁等价性模板

补丁等价性指两个补丁在给定测试套件下是否产生相同的通过/失败结果。半形式化模板要求：

• 定义： 明确等价性的定义（Modulo Tests）。
• 前提： 描述每个补丁修改了哪些文件。
• 测试行为分析： 对每个相关测试，分别追踪 Patch 1 和 Patch 2 下的执行路径。

  • Claim: 在 Patch 1 下，测试 X 将 [PASS/FAIL]，因为 [执行追踪]。
  • Claim: 在 Patch 2 下，测试 X 将 [PASS/FAIL]，因为 [执行追踪]。
• 反例（Counterexample）： 如果不等价，必须提供具体的代码路径证据。
• 结论（Formal Conclusion）： 基于 D1 定义判定是否等价。

2.3.2 故障定位模板

• 阶段 1：测试语义分析： 将测试的期望行为形式化为 PREMISE。
• 阶段 2：代码路径追踪： 记录从测试入口到生产代码的调用序列。
• 阶段 3：差异分析： 识别实现代码与测试期望在何处发生偏离，形式化为 CLAIM。
• 阶段 4：排序预测： 基于 CLAIM 生成预测结果。

2.3.3 代码问答模板

• 函数追踪表： 列出所有检查过的函数、位置、参数类型和验证过的行为。
• 数据流分析： 追踪关键变量的创建、修改和使用。
• 语义属性： 列出属性及其证据（文件:行号）。
• 替代假设检查： 强迫模型思考“如果反面为真，会存在什么证据”，并去寻找该证据。

3. 实验任务与评估

论文在三个主要任务上评估了该方法：补丁等价性验证、故障定位和代码问答。

3.1 任务一：补丁等价性验证

这是本文的核心任务。给定针对同一规范（Issue）的两个补丁，判断它们在存储库的测试套件上是否产生相同的结果。

3.1.1 数据集构建

为了避免简单的表面相似性干扰，作者基于 SWE-bench-Verified 构建了一个具有挑战性的数据集。

• 来源：社区贡献的智能体轨迹和生成的补丁。
• 筛选：选取由不同智能体生成的补丁对。
• 难度控制：平衡了高相似度但行为不同（Non-Equivalent）和行为相同（Equivalent）的样本。
• 规模：170 个高难度样本。

3.1.2 实验结果：策展数据集

分析：

• 半形式化推理将错误率降低了近一半，准确率从 78.2% 提升至 88.8%。
• 虽然平均步数增加了约 2.8 倍（从 10 步增加到 28 步），但这换来了显著的性能提升。
• 主要的错误来源是“遗漏的执行差异”，即智能体未能追踪到导致行为差异的所有代码路径。

3.1.3 实验结果：验证 LLM 生成的补丁

该实验模拟实际应用场景：验证一个 LLM 生成的补丁是否与已知的参考（Gold）补丁等价。这可以作为强化学习的奖励信号。
数据集：从 SWE-bench-Verified 中随机抽样的 200 个例（100 个正确，100 个错误）。

分析：

• 基于文本相似度（difflib）的方法仅能达到 73% 的准确率，完全不足以作为可靠的奖励信号。
• Opus-4.5 配合半形式化推理达到了 93.0% 的准确率。这表明，在拥有测试代码（Fail-to-Pass tests）作为上下文的情况下，智能体能够进行非常精确的语义分析。
• 单次调用（Single Call）即使加上文件上下文，准确率也仅为 87.5%，证明了智能体自主探索代码库的必要性。

3.1.4 案例研究：Django 补丁分析

案例描述（django-13670）：
两个补丁都试图修复 1000 年以前的年份格式化问题。

• Patch 1: return format(self.data.year, "04d")[-2:]
• Patch 2: return '%02d' % (self.data.year % 100)

标准推理（Standard Reasoning）：
模型认为两者等价。它假设 format() 调用的是 Python 的内置函数，对于整数输入，行为应与 Patch 2 一致。

半形式化推理（Semi-formal Reasoning）：
模型通过强制追踪 format 的定义，发现它并非内置函数，而是 dateformat.py 模块中定义的函数（第 340 行）：
def format(value, format_string): ... df = DateFormat(value) ...
该函数期望 value 是一个日期对象，而不是整数。因此，Patch 1 会抛出 AttributeError，而 Patch 2 能正常工作。
结论： 半形式化推理成功识别出两者不等价，避免了错误判断。

3.2 任务二：故障定位

任务是在 Defects4J 数据集中，给定一个失败的测试，找出具体的 Bug 代码行。

3.2.1 实验设置

• 指标： Top-N 准确率（预测的前 N 个位置中包含 Bug 的比例）。
• 变体：

  • All: 要求覆盖所有 Ground Truth 代码块。
  • Any: 要求覆盖至少一个 Ground Truth 代码块。
• 评估规模： 小规模（50 个 Bug）和较大规模（100 个 Bug）。

3.2.2 实验结果

分析：

• 在 Agentic 模式下，半形式化推理使 Top-5 (All) 准确率提升了 11.6 个百分点 (60.5% -> 72.1%)。
• 在更大规模的验证（100 bugs）中，优势依然存在（+5pp）。
• 这证明了结构化推理有助于模型在复杂的代码库中缩小搜索范围并精确定位问题。

3.2.3 案例研究：Mockito_8

Bug 描述： Java 泛型类型解析中的 StackOverflowError。当处理自引用类型（如 SelfRef<T extends SelfRef<T>>）时，递归无限循环。

标准推理：
模型仅进行了一轮推理，预测崩溃发生的位置 getActualTypeArgumentFor 是 Bug 所在。这只是症状，不是根因。

半形式化推理：
通过 4 个阶段的模板，模型进行了两轮推理：

1. Phase 1 (语义分析): 确定测试涉及自引用泛型类型。
2. Phase 2 (路径追踪): 详细记录了 10 个观察点（O1-O10），追踪了从 inferFrom 到 registerTypeVariablesOn 的完整调用链。
3. Phase 3 (差异分析): 模型提出了三个假设，并测试了自引用类型会导致 contextualActualTypeParameters 映射重写（overwrite），导致后续查找无限递归。
4. Phase 4 (预测): 正确指出了第 80 行的 registerTypeVariablesOn 方法覆盖了安全的映射，是真正的根因。

3.3 任务三：代码问答

使用 RubberDuckBench 基准测试，包含 15 个涉及 Python、Java、C++ 的代码理解问题。

3.3.1 实验结果

分析：

• Opus-4.5 获得了显著提升 (+8.7pp)。
• Sonnet-4.5 的提升较小，表明结构化推理的收益可能与基础模型的能力或偏好有关。Sonnet 可能在标准模式下已经具备较强的内在结构化能力，或者 Opus 更受益于强制性的详细追踪。
• 半形式化推理有效地纠正了模型“看名字猜功能”的倾向。例如在 cpp_3 问题中，标准推理猜测 at() 和 [] 的区别在于错误处理，而半形式化推理通过追踪发现 map 初始化使用了枚举，证明不存在无效键值，从而得出了正确结论。

4. 错误分析与局限性

尽管性能显著提升，半形式化推理并非完美。论文详细分析了 Opus-4.5 在补丁验证中的失败模式：

1. 不完整的执行追踪： 尽管指令要求追踪，智能体有时仍会假设函数行为而不去实际读取代码，特别是对于深层调用。
2. 第三方库语义： 当源代码不可用（如引用的外部库）时，智能体只能依靠猜测，这往往导致错误。
3. 忽视细微差异： 智能体识别出了语义差异，但错误地判断这些差异不会影响测试结果。

在故障定位中，主要失败原因包括：

1. 间接 Bug： Bug 位于配置类或未被测试直接调用的类中，模型容易忽略。
2. 跨文件 Bug： 涉及多个文件的修改极其困难。
3. 领域特定知识： 如数值分析算法中的 Bug，超出了模型的通用编程知识范围。

5. 相关工作对比

• SWE-bench & Agents: SWE-agent, OpenHands, Agentless 等系统依赖于执行测试来验证修复。本文的方法提供了不执行的替代方案。
• 非执行验证 (SWE-RM, Agentic Rubrics, CodeJudge): 这些工作使用奖励模型或 LLM 作为裁判，但大多采用非结构化推理。本文证明了结构化（半形式化）推理能显著提高准确性。
• 形式化验证 (Lean, Coq): 提供了数学上的保证，但门槛过高，难以扩展到任意代码库。半形式化推理是介于自然语言推理和完全形式化证明之间的折衷方案。

6. 结论与未来展望

这篇论文通过引入半形式化推理，展示了 LLM 智能体在不执行代码的情况下进行深度语义分析的潜力。主要贡献在于：

1. 提出了一套通用的结构化推理模板（Premises -> Trace -> Conclusion）。
2. 在补丁等价性验证上达到了 93% 的高准确率，使其成为 RL 训练中昂贵沙盒执行的有力替代者。
3. 在故障定位和代码问答任务上验证了该方法的泛化能力。

未来工作方向：

• 后训练（Post-training）： 微调模型以内化半形式化模板的结构，从而可能消除繁琐的提示工程并减少 Token 消耗。
• 扩展到其他静态分析任务： 如安全漏洞检测、代码异味（Code Smell）识别等。
• 混合验证（Hybrid verification）： 结合 LLM 推理与轻量级的形式化方法或符号执行，以提供更强的保证。

深度解读：为什么“半形式化”有效？

这篇论文的发现与最近在数学推理领域的研究（如 Chain-of-Thought 的改进版）不谋而合。LLM 在处理逻辑密集型任务时，往往倾向于“系统 1”的直觉思维。通过强制要求特定格式的输出（即本文的 Certificate），实际上是强迫模型切换到“系统 2”的慢思考模式。

1. 显式证据： 要求引用 file:line 减少了模型编造不存在的代码行为的可能性。
2. 假设检验： 在故障定位中，模板明确要求提出假设并验证，这模仿了人类调试代码的过程。
3. 路径覆盖： 在补丁比较中，要求分别追踪两个补丁的路径，使得差异在对比中自然显现，而不是依赖模型对两个代码块的整体“感觉”。

这种方法的一个潜在缺点是上下文窗口的消耗和推理时间的增加（Token 数增加）。但在高价值的任务（如合并代码前的自动验证、RL 训练的奖励计算）中，这种计算成本的增加相对于执行测试的成本或错误代码上线带来的风险来说，是完全可以接受的。

更多细节请阅读原文。

往期文章：

• LK Losses：投机采样中接受率的直接优化方法

• 腾讯混元提出 RubricBench：对齐模型生成的评分标准与人类标准

• Weak-Driven Learning：弱模型如何助力强模型突破后训练瓶颈

• Agentic Proposing——基于组合技能合成的大语言模型推理增强

• 美团提出 DynaMO：面向RLVR的动态Rollout分配与优势调节策略

• 你的推理模型其实知道何时停止：解决 Long CoT 中的“过度思考”

• 小红书提出 VESPO 变分序列级软策略优化，从测度变换视角重构重要性采样

• Qwen 团队新作：统一视角解读 Transformer 中的 Attention 与 Residual Sinks

• Less is Enough——在大模型特征空间中合成多样化数据

• 腾讯混元提出 G-OPD：超越教师模型的广义在线蒸馏与奖励外推

• 腾讯混元提出 Composition-RL：通过合成可验证Prompt提升大模型强化学习效率

• 上交 & 千问提出 OPUS：论大模型预训练中数据选择与优化器几何的对齐

• 大语言模型强化微调中的熵动力学分析

• Sea AI Lab 提出 DPPO：重新审视 PPO 算法中的信任域

• MaxRL：重新审视强化学习与最大似然估计的统一

• Agentic RL 的新范式：在强化学习循环中融合规则、模型奖励与自然语言批评

• 自蒸馏优化 SDPO：如何利用富文本反馈打破 RLVR 的信用分配瓶颈？

• MIT 提出 SDFT：作为逆强化学习（Inverse RL）的在线自蒸馏

• GPT 之父 Alec Radford 新作：通过 Token 级数据过滤实现比 RLHF 更稳健的拒绝边界

• 美团 LongCat 技术报告解读：在高稀疏度下，Embedding 扩展优于专家扩展

• 阿里云提出 DASD 分布对齐的序列蒸馏：实现更优的长链思维推理

• DeepSeek-OCR 2: Visual Causal Flow 技术报告解读

• 美团 LongCat-Flash-Thinking-2601 技术报告解读

• Agentic Reasoning for Large Language Models 综述：基础、进化与协作

• 小米推出 JudgeRLVR：先判断后生成——打破推理模型“长思维链”的效率悖论

• 你的 GRPO 的优势估计是有偏差的：GRPO 中的统计陷阱与 HA-DW 修正方案

• Meta 提出 Dr.Zero：零数据训练的自进化 Search Agent

• 深度解析 Ministral 3：基于级联蒸馏的参数高效密集模型训练方法论

• Sparse-RL：通过稳定稀疏 Rollout 突破 LLM 强化学习的显存墙

• Qwen 发布 ArenaRL：解决开放域 Agent 的奖励建模难题

• NTU & 通义提出 AgentOCR：基于光学自压缩的智能体历史重构

• DeepSeek 新论文 Engram 深度解读

• Anthropic 提出 EDL 来量化大模型的泛化能力

• 小米 MiMo-V2-Flash 技术报告：MoE 架构、混合注意力机制与多教师在线蒸馏

• DeepSeek-R1 v2 发布：新增技术细节与训练流程全解读

• WAIT, WAIT, WAIT... WHY DO REASONING MODELS LOOP?

• 陈丹琦团队新作：负样本强化在 LLM 推理中的有效性机制

• 深度解读 Recursive Language Models：利用递归与环境交互突破 LLM 上下文限制

• 论大语言模型强化学习训练中的 KL 正则化

• 阿里新作 Let It Flow: Agentic Crafting on Rock and Roll 深度解读

• DeepSeek 新作 mHC：为何要把超连接约束在流形上？

• 字节 Seed 新作：通过辅助损失实现 MoE 专家与路由器的紧密耦合 (ERC Loss)

• Bottom-up Policy Optimization: 自下而上的策略优化——语言模型内部潜藏的子策略

• Google DeepMind 新作：自回归模型中的涌现时间抽象实现了分层强化学习

• 被牺牲的元认知：效率导向优化如何改变了模型的推理结构

• Who is Adam? 重新审视大模型 RLVR 阶段的优化器选择

• 代码大模型的 Scaling Laws：编程语言差异性与多语言混合策略研究

• 从 0.5B 到 72B：揭秘 RL Post-Training 中的计算、数据与模型规模权衡

• 【深度专访】Gemini 3 预训练负责人：我们不再只是构建模型，而是构建 AI 系统

• 为什么 RM 总是学不好推理？揭秘 BT Loss 中被忽视的“距离偏差”

• QwenLong-L1.5：长上下文推理与记忆管理的后训练方案

• Motif-2-12.7B-Reasoning：RL 训练配方与全栈优化实践指南