Functionally Equivalent or Not? Graph-Grounded Differential Surrogate Execution for Code Equivalence

AI summary

Overview

Research area: AI for software engineering, specifically automated program-equivalence assessment, LLM code reasoning, and benchmark/patch validation.

Technical level: Advanced. The paper assumes familiarity with program graphs, control-flow and data-flow analysis, symbolic/concolic execution, translation validation, differential testing, and selective classification.

Scope: The paper introduces FEAgent, a graph-grounded agent that decides whether two programs are functionally equivalent, inequivalent, or unclear within an explicitly declared input domain, observable schema, and environment contract, and audits its verdicts against direct execution.

What This Paper Is About

Deciding whether two programs behave the same is central to code modernization, patch validation, refactoring, and code-generation evaluation, but existing signals are incomplete: tests cover only finite inputs, textual similarity confuses implementation with behavior, and unconstrained language-model judgments are hard to audit. Direct execution is often impossible when a program depends on an obsolete, licensed, unavailable, or unsafe environment. FEAgent addresses this by combining typed program-graph evidence with "differential surrogate execution," in which blinded language-model surrogates predict each program's behavior on branch-targeting inputs, and a deterministic reconciler returns Equivalent, Inequivalent, or Unclear instead of forcing a verdict.

Key Contributions

1. A formulation of scoped observational equivalence that makes the input domain, observable behavior, and environment assumptions explicit through an assessment specification Σ = (𝒟, 𝒪, Γ, τ), supporting Equivalent, Inequivalent, and Unclear judgments rather than a forced binary decision.

2. The FEAgent architecture, which aligns behavioral anchors, derives checkable obligations, generates branch-targeting inputs, and independently predicts source and target traces using mutually blinded surrogates.

3. An auditable decision process in which every claim cites graph nodes and source spans, predicted mismatches identify a concrete input and observable, and deterministic gates prevent an LLM from validating its own evidence.

4. An execution-grounded evaluation on 1,200 EquiBench pairs and 331 test-passing SWE-bench Verified patches, confirming 216 of 230 challenged EquiBench labels and 94 of 109 flagged patch divergences.

Main Findings

• EquiBench label errors are substantial: Across all 1,200 evaluated EquiBench pairs, FEAgent's disagreement rate was 19.2% (230 pairs), and execution verified 216 of those 230 disagreements (93.9%), giving an execution-confirmed divergence (ECD) of 18.0% (216/1,200). The paper states that at least this fraction of pairs carries a published label contradicted by an executed counterexample.

• Disagreement concentrates in two subsets: OJ_A showed a 29% disagreement rate (116 of 400) with 95.7% verified genuine (111 cases) and an ECD of 27.8%; OJ_VA showed 27.25% (109 of 400) with 96.3% verified genuine (105 cases) and an ECD of 26.3%. OJ_V showed only 1.25% disagreement (5 of 400), and none of its disagreements were genuine mislabels (0%), with an ECD of 0%.

• Test-passing patches can diverge from reference behavior: On SWE-bench Verified, FEAgent flagged 109 of 331 test-passing patches (32.9%) as inequivalent, and execution confirmed 94 of those flags (86.2%), yielding an ECD of 28.4% (94/331). Fourteen flags did not reproduce because the change is compensated elsewhere, unreachable, or observably equivalent, and one remained inconclusive.

• Graph context localizes hidden divergences: In the django-11066 case study, both the reference and candidate revisions return None, but the candidate calls clear_cache(using='default') while the reference calls clear_cache(), so the candidate clears only the default alias. The graph slice links RenameContentType._rename to the effectful clear_cache call and its router, lookup, and save guards, showing which inputs reach the call.

• Concrete counterexamples separate algorithmic, boundary, and data divergences: Figure 2 (OJ-VA case 370) shows that for n = 4 and [0, 0, 2, 2], multiplicity-only validation returns 4 while exact sequence validation returns 0. Figure 3 (OJ-A case 10) shows that for a = 10, b = 3, and n = 16, exact long division produces 48 while floating-point conversion produces 50. Figure 4 (OJ-VA case 288) shows boundary clamping outputs Yes on {#.., ..., ...} while padded neighbor references output No.

• Model configuration: All model-backed components in the reported experiments used Claude Opus 4.6 with a 32,000-token thinking budget and prompt caching enabled. Candidate patches for SWE-bench Verified were generated with mini-SWE-agent and GPT-OSS-120B from the 500 issues, retaining the 331 patches that pass all tests.

• Scope limits are stated explicitly: FEAgent is a selective audit layer, not a formal verifier. Inequivalent prioritizes a concrete candidate counterexample; Equivalent requires covered obligations without a stable contradiction; Unclear exposes missing evidence. Surrogate traces only propose witnesses, and every reported divergence was reproduced by direct execution.

Methodology in Plain English

FEAgent treats equivalence as an evidence-acquisition problem rather than a single yes/no question. It has five phases.

First, it parses both programs into typed, attributed program graphs whose nodes represent entities such as files, types, functions, parameters, statements, variables, literals, and external symbols, and whose edges encode containment, declaration, calls, imports, inheritance, overrides, control-flow succession, def-use links, reads, writes, returns, throws, and externally visible effects. Unresolved calls become explicit nodes rather than silently missing edges.

Second, it aligns entry points and behavioral anchors, then derives checkable obligations across five groups: interface, control, data, effects, and environment. An obligation is a question like "do both programs reject a zero denominator with the same observable exception?" and carries a status of supported, contradicted, unresolved, or out-of-scope.

Third, a structural analyst inspects only bounded graph slices through a query API. Its responses are accepted into an evidence ledger only if they cite a claim, polarity, node IDs, a relation path, source spans, and assumptions; unsupported prose is discarded.

Fourth, a branch-aware generator proposes typed inputs targeting uncovered obligations, including boundary values, values around branch thresholds, aliasing and mutation cases, empty and singleton structures, and exceptional inputs permitted by the domain. Then separate source and target surrogates, blinded from each other, predict a structured trace per program covering return value, exception, external side effects, reachable-parameter mutations, termination status, and a stepwise trace anchored to graph nodes. A non-generative comparator returns match, mismatch, or unknown per observable field.

Fifth, deterministic reconciliation applies ordered gates: a validity gate for missing inputs (Unclear), a contradiction gate for supported contradictions or stable mismatches (Inequivalent), a conflict gate when channels disagree (Unclear), a coverage gate requiring all mandatory obligations supported or exercised with confidence above threshold (Equivalent), and otherwise Unclear. Confidence is computed from observable-comparison stability, obligation coverage, graph resolution quality, and evidence completeness, calibrated on a development partition and frozen before test evaluation. No LLM is asked to override these gates. For every disagreement with a label, the team executed code to check whether the disagreement was a genuine label error or a method failure, using asymmetric verification rules for the two disagreement directions.

Why This Matters

Impact on research: The paper argues that accuracy against published labels conflates method errors with label errors, and proposes execution-grounded metrics (Disagreement Rate, Verified Genuine, Execution-confirmed Divergence) as a replacement. It also positions model-based reasoning as an audit layer between testing and formal verification, complementing translation validation, differential testing, and symbolic execution in settings where those cannot run.

Real-world applications:

• Code modernization and cross-language migration, where legacy or proprietary dependencies prevent direct execution.
• Patch validation in bug fixing, where a candidate patch may pass tests yet silently lose reference behavior.
• Refactoring verification, where syntactically different programs may be interchangeable and nearly identical programs may diverge on one boundary condition.
• Code-generation evaluation, where tests under-specify behavior and unconstrained model judgments are hard to audit.

Industry relevance: The work comes from AWS AI Labs, and its SWE-bench Verified result suggests that benchmark scoring based only on repository tests can count behaviorally divergent patches as resolved. For teams that gate releases on test suites, an audit layer that yields reviewable evidence—concrete inputs, cited graph nodes, and explicit uncertainty—targets a practical blind spot without claiming formal proof.

Future Directions

• Matched-budget component ablations. The paper states that a quantitative graph ablation remains future work, and that causal attribution of FEAgent's gains to specific components requires a matched ablation.
• Execution audits of unflagged cases. The authors list this among the next priorities, since their current verification focuses on cases where FEAgent disagrees with the oracle.
• Extending the graph front end. The EquiBench evaluation excludes the C/DCE, CUDA, and x86-64 subsets because the current graph front end does not support them.
• Reducing miss and abstention risk. The scope section notes that incomplete graphs, unresolved symbols, and surrogate errors can still lead FEAgent to miss a divergence or abstain, which defines an open reliability target.

Target Audience

Researchers and engineers working on program equivalence, differential testing, translation validation, LLM-based code reasoning, and benchmark or patch-evaluation methodology. It will also interest software-engineering practitioners responsible for validating generated patches, code modernization, or cross-language ports, and readers of selective-prediction and calibration work applied to code. A background in static program analysis and language-model evaluation will help, since the paper is written at an advanced technical level.

Authors’ abstract

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.