Recoleta Item Note
Agentic Code Reasoning
本文研究一种无需执行代码、仅靠代理在代码库中探索与推理来理解程序语义的能力，并提出“半形式化推理”作为结构化证据模板。该方法在补丁等价验证、故障定位和代码问答三类任务上都优于常规非结构化代理推理。
agentic-reasoningcode-intelligencepatch-verificationfault-localizationstatic-code-analysis
Summary
本文研究一种无需执行代码、仅靠代理在代码库中探索与推理来理解程序语义的能力，并提出“半形式化推理”作为结构化证据模板。该方法在补丁等价验证、故障定位和代码问答三类任务上都优于常规非结构化代理推理。
Problem
- 论文要解决的是：LLM 代理能否在不运行代码的情况下，可靠地分析代码语义、判断补丁是否等价、定位缺陷并回答代码理解问题。
- 这很重要，因为执行真实仓库代码通常昂贵、依赖复杂且难以扩展；若能静态完成高质量语义判断，可用于 RL 奖励信号、代码审查、静态分析、缺陷排查。
- 现有非结构化推理容易“猜答案”或跳步；完全形式化验证又需要为真实仓库和多语言框架建立严格语义，实际成本过高。
Approach
- 核心方法是 semi-formal reasoning：不给模型自由散乱地想，而是要求它按固定模板写出前提、代码路径追踪、逐项证据、形式化结论，像提交一张“推理证明单”。
- 这种模板被设计成一种证书（certificate）：代理若不先找到代码依据、没有覆盖关键测试/路径，就很难直接下结论，从而减少无依据断言。
- 方法是提示工程层面的通用机制，不是训练专门模型，也不是把代码翻译成 Lean/Coq 这类完全形式系统；因此更容易跨任务迁移到补丁等价、故障定位、代码 QA。
- 在代理设置下，模型可用工具浏览仓库、跟踪调用链、查看测试和相关文件，但不能执行仓库代码或测试；主要依赖静态分析式的代码探索与推理。
Results
- 补丁等价验证（170 个精心构造样本）：Opus-4.5 从标准推理的 78.2% 提升到半形式化的 88.8%，提升 10.6 个百分点；其中非等价样本准确率 78.6% → 82.9%，等价样本 78.0% → 93.0%。代价是平均步数 10.08 → 28.17（约 2.8x）。
- 真实 agent 生成补丁验证（200 个样本，含测试规格）：最佳结果为 Opus-4.5 + agentic semi-formal，准确率 93.0%；对比 difflib 73%、单次调用 86.0%、单次调用+文件上下文 87.5%、agentic standard 87.0%。Sonnet-4.5 在同设置下也达到 91.5%。
- 代码问答（RubberDuckBench）：摘要声明半形式化推理达到 87% 准确率，相比标准 agentic reasoning 提升 9 个百分点；贡献段还给出相对 single-shot 76% 提升 10.8 个百分点、相对标准 agentic 提升 8.7 个百分点。
- 故障定位（Defects4J，小规模 43 个可评估 bug）：Opus-4.5 在 agentic 模式下，Top-5（All）从 60.5% 提升到 72.1%，提升 11.6 个百分点；Top-5（Any）从 81.4% 提升到 88.4%，提升 7.0 个百分点。single-shot 下 Top-5（All）为 55.6% → 63.9%。
- 故障定位（更大规模 90 个可评估 bug）：文中声称 Opus-4.5 的半形式化推理相比标准模式在 Top-5（All）上再提升约 5 个百分点；给出的截断表中标准值为 43.3%，但半形式化的完整数值在提供摘录中未完整显示。
- 论文最强结论是：通过结构化代理推理，LLM 可以在不执行代码时做出有意义的语义级代码分析，并接近可用于执行免费/低执行依赖验证与 RL 反馈的可靠性门槛。
Link
Built with Recoleta
Run your own research radar
Turn arXiv, Hacker News, OpenReview, Hugging Face Daily Papers, and RSS into local Markdown, Obsidian notes, Telegram digests, and a public site.