发表机构
AWS AI Labs（亚马逊云科技人工智能实验室）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
FEAgent结合程序图证据与差分代理执行，通过有界查询和盲化LLM代理预测，审计代码等价性，在EquiBench和SWE-bench上发现大量基准标签错误与行为差异。
AI 中文摘要
确定两个程序是否功能等价对于代码现代化、补丁验证、重构和代码生成评估至关重要。然而，通常的信号是不完整的：测试仅覆盖有限输入，文本相似性混淆了实现与行为，且不受约束的LLM判断难以审计。当程序依赖于过时、许可受限、不可用或不安全的环境时，直接执行往往不可能。我们引入了FEAgent，一种选择性等价性评估智能体，它将类型化程序图证据与差分代理执行相结合。FEAgent首先对齐公共接口和行为相关的图锚点，然后对调用流、控制流、数据流、类型、导入和效应关系发出有界查询。接下来，一个分支感知的生成器智能体提出判别性输入，两个盲化的LLM代理独立预测源和目标可观测值。每个声明和预测的差异都记录在证据账本中。一个确定性的协调器随后返回等价、不等价或不确定，而不是在路径未被覆盖或证据冲突时强制给出结论。我们在函数级等价性和仓库级错误补丁上评估FEAgent，其中现有预言机是基准标签或通过的测试套件。与预言机的每个分歧都通过直接执行进行裁决，揭示了基准标签中的错误和仅单元测试评分遗漏的行为差异。在EquiBench上，执行确认了FEAgent与已发布标签在1200个评估对中的216个（18.0%）存在分歧；在SWE-bench Verified上，331个通过测试的智能体补丁中有94个（28.4%）与参考补丁存在分歧。因此，FEAgent作为测试和形式验证之间的审计层，保持其证据可审查且不确定性明确，而不声称等价性证明。
英文摘要
Determining whether two programs are functionally equivalent is central to code modernization, patch validation, refactoring, and code-generation evaluation. Yet the usual signals are incomplete: tests cover only finite inputs, textual similarity confuses implementation with behavior, and unconstrained LLM judgments are difficult to audit. Direct execution is often impossible when a program depends on an obsolete, licensed, unavailable, or unsafe environment. We introduce FEAgent, a selective equivalence assessor agent that combines typed program-graph evidence with differential surrogate execution. FEAgent first aligns public interfaces and behaviorally relevant graph anchors, then issues bounded queries over call-flow, control-flow, data-flow, type, import, and effect relations. Next, a branch-aware generator agent proposes discriminating inputs, and two blinded LLM surrogates independently predict source and target observables. Every claim and predicted divergence is recorded in an evidence ledger. A deterministic reconciler then returns EQUIVALENT, INEQUIVALENT, or UNCLEAR rather than forcing a verdict when paths are uncovered or evidence conflicts. We evaluate FEAgent on function-level equivalence and repository-level bug patches, where the existing oracle is a benchmark label or a passing test suite. Every disagreement with that oracle is adjudicated by direct execution, revealing errors in benchmark labels and behavioral divergences missed by unit-test-only scoring. On EquiBench, execution confirms FEAgent's disagreements with published labels on 216 of 1,200 evaluated pairs (18.0%); on SWE-bench Verified, 94 of 331 test-passing agent patches (28.4%) diverge from the reference patch. FEAgent thus serves as an audit layer between testing and formal verification, keeping its evidence reviewable and its uncertainty explicit without claiming a proof of equivalence.
Comments14 pages, 5 figures, 4 tables, accepted by NeurIPS 2026 Workshop on AI for Verifiable Coding
