h t t p s : / / a r x i v . o r g / h t m l / 2 6 0 3 . 0 1 8 9 6 v 2

Ingest: Agentic Code Reasoning

Type: kb/sources/types/ingest-report.md

Classification

ArXiv preprint with explicit methodology, controlled ablations across three evaluation tasks, multiple baselines, error analyses, and quantitative results on established benchmarks (SWE-bench, Defects4J, RubberDuckBench). Author: Shubham Ugare and Satish Chandra (Meta). Industry researchers reporting ablations on practical SWE-agent workflows with access to frontier models (Opus-4.5, Sonnet). Moderate-to-strong credibility for empirical claims.

Summary

The paper introduces "semi-formal reasoning" — structured prompting templates that require LLM agents to construct explicit premises, trace execution paths, and derive formal conclusions when analysing code without executing it. The templates are task-specific but share a common principle: force the agent to document verifiable evidence before reaching a conclusion. Across three tasks (patch equivalence verification, fault localization on Defects4J, code question answering on RubberDuckBench), semi-formal reasoning consistently improves accuracy over unstructured baselines by 5-12 percentage points. The headline result is 93% verification accuracy on real-world agent-generated patches using Opus-4.5, approaching the reliability needed for execution-free RL reward signals. The paper's motivating application is replacing test execution with LLM-based verification in training pipelines, though the cost argument for this substitution is asserted rather than demonstrated.

Quotes

  • Source extract (verbatim): We study this capability, which we call agentic code reasoning, and introduce semi-formal reasoning: a structured prompting methodology that requires agents to construct explicit premises, trace execution paths, and derive formal conclusions.
  • Source location: Abstract.
  • Source extract (verbatim): Crucially, the agent cannot execute repository code or run its test suite: dependencies are not installed and the environment is not sandboxed.
  • Source location: Section 2.1, Agentic vs. Single-Shot Verification.
  • Source extract (verbatim): For fault localization on Defects4J just2014defects4j, semi-formal reasoning improves Top-5 accuracy by 5-12 percentage points over standard agentic reasoning.
  • Source location: Section 1, Contributions.
  • Source extract (verbatim): Even with semi-formal analysis, 19 cases are incorrect.
  • Source location: Section 4.1.1, Curated Dataset Evaluation.
  • Source extract (verbatim): The results reveal that structured semi-formal reasoning provides substantial gains: Opus improves from 78.3% (standard agentic) to 87.0% with the semi-formal template (+8.7pp). For Sonnet, standard agentic reasoning already achieves 85.3%, and the semi-formal template does not yield further gains (84.8%), suggesting that the benefit of structured reasoning varies by model capability and may plateau when the base model is already strong.
  • Source location: Section 4.3, Code Question Answering.
  • Source extract (verbatim): The structured template requires the agent to fill in a function trace table (listing every function examined with file:line locations and verified behavior), data flow analysis (tracing how key variables flow through the code), semantic properties with explicit evidence, and an alternative hypothesis check.
  • Source location: Section 4.3, Code Question Answering.

Connections Found

The /connect discovery identified 7 note connections and 2 source connections, with 9 candidates rejected after evaluation.

Strongest connections:

  1. Structured-prompt gains do not establish training-distribution selection (evidenced-by): The paper supplies the note's central contrast: semi-formal templates improve code-verification accuracy by 5–12 percentage points, yet the bundled intervention does not isolate format, process, extra computation, or a training-distribution mechanism. Claude Sonnet's code-QA result (84.8% with the template versus 85.3% without it) also shows that the measured effect is condition-dependent.

  2. human-writing-structures-transfer-to-llms-because-failure-modes-overlap (exemplifies): The paper documents specific human-like failure modes that structured templates correct: guessing function behavior from names, skipping case enumeration, dismissing subtle differences as irrelevant. The semi-formal template corrects these by forcing explicit evidence at each step.

  3. agentic-systems-interpret-underspecified-instructions (extends): Semi-formal templates are a concrete, measured interpretation-narrowing mechanism. "Standard reasoning" (minimal prompt, no constraints) is maximally underspecified; the template constrains the interpretation space. The 10pp accuracy gain measures the value of that narrowing.

  4. oracle-strength-spectrum (grounds): The paper works in a domain with hard oracles (test execution) but positions LLM verification as a cheaper substitute. Semi-formal reasoning at 93% accuracy is a soft oracle approximating the hard oracle. The error analysis characterises the remaining 7% gap (incomplete tracing, third-party semantics, dismissing subtle differences).

  5. error-correction-works-above-chance-oracles-with-decorrelated-checks (enables): The paper establishes that semi-formal verification has strong discriminative power (93% vs 50% random baseline), satisfying TPR > FPR for error-correction amplification. The three identified failure modes suggest decorrelation strategies (varying trace order, varying detail level) that the paper does not explore.

  6. structured-output-is-easier-for-humans-to-review (exemplifies): The paper explicitly describes semi-formal certificates as designed to be "easier to manually validate than examining full agent trajectories."

  7. methodology-enforcement-is-constraining (exemplifies): Templates constrain how the agent reasons (must state premises, must trace paths, must derive conclusions) — methodology enforcement at the skill level with underspecified response, matching the note's enforcement gradient.

Source connections: Synthesises with ConvexBench ingest (both show structured process > free-form reasoning across different domains) and connects to Towards a Science of AI Agent Reliability (reliability framework applicable to the verification approach).

Extractable Value

  1. Semi-formal templates as a causal-identification case. The paper provides a quantified gain and a null, but its bundled templates do not reveal which component caused either result. This now grounds Structured-prompt gains do not establish training-distribution selection. [quick-win]

  2. Failure-mode taxonomy for verification agents. Three specific failure classes — incomplete execution tracing, third-party library semantic guessing, and dismissal of subtle differences — are reusable for designing eval harnesses or decorrelation strategies. Not currently captured in any KB note. [quick-win]

  3. Process structure vs output structure as separate design dimensions. Existing KB notes mostly discuss output schema constraints; this paper shows process-schema constraints (what reasoning steps must occur) as an independent lever. The distinction is not articulated in the KB. [deep-dive]

  4. Decorrelation strategy design for soft-oracle amplification. The three failure modes map to natural decorrelation axes: vary which code paths to trace first, vary the level of detail required, vary whether to start from tests or from patches. Combining this with the error-correction note could yield a concrete amplification protocol. [experiment]

  5. 93% as a calibration point on the oracle-strength spectrum. A concrete data point for what "soft oracle replacing hard oracle" looks like in practice — useful for the oracle-strength-spectrum note's maturation path, specifically the question of when substitution is economically justified. [just-a-reference]

  6. Model capability as boundary condition for structured reasoning gains. Semi-formal reasoning helps Opus but not Sonnet on code QA. This suggests a threshold: weaker models may need the scaffolding more, while stronger models have already internalised equivalent reasoning patterns. Relevant to the structure-activates note's cautionary status. [experiment]

Limitations (our opinion)

What was not tested:

  • Cost comparison is entirely absent. The paper asserts execution-free verification is cheaper than running tests, but provides no cost analysis. Semi-formal mode uses 2.8x more agent steps than standard; Opus-4.5 inference at 100 steps per verification is expensive. Whether this is cheaper than sandbox/CI depends on scale, repo diversity, and infrastructure — none measured. The oracle-strength-spectrum note predicts this tension: soft oracles substitute for hard oracles only when the cost differential justifies the accuracy gap.

  • No evaluation of amplification through repetition. The paper establishes that semi-formal verification has discriminative power (93% accuracy), satisfying the conditions the error-correction note identifies for amplification. But voting, ensemble, or decorrelated-prompt strategies were not tested. This is a significant omission given that the motivating application (RL reward signals) would benefit most from pushing accuracy above 93%.

  • Single model family on a single benchmark ecosystem. All results use Claude models (Opus-4.5, Sonnet) on SWE-bench-derived tasks, Defects4J (Java only), and RubberDuckBench (15 questions). Generalization to other model families, programming languages, and repository structures is untested. The Sonnet non-improvement on code QA hints that the gains may be model-specific.

  • Accuracy ceiling may be insufficient for the stated application. 93% on a balanced dataset means ~7% false reward signals in RL training. The paper does not evaluate whether this error rate is tolerable downstream — whether RL training with 7% noisy rewards converges to similar policies as training with test execution. The gap between "feasibility result" and "deployment result" is unaddressed.

  • No comparison with formal or semi-automated verification. The paper positions semi-formal reasoning between unstructured CoT and full formal verification (Lean, Coq, Datalog). But no hybrid approaches were tested — combining LLM reasoning with lightweight symbolic checks, type-system verification, or property-based testing. The codification framework predicts that hybrid approaches (hard checks where possible, soft elsewhere) would outperform purely soft verification.

  • Template design is not ablated. The templates differ by task but the paper does not ablate which components matter. Is the premises section critical? The per-test traces? The formal conclusion format? Without this, it's unclear whether the gains come from forcing evidence collection (process structure) or from the specific output format (output structure) — a distinction the KB notes would care about.

The completed update to Structured-prompt gains do not establish training-distribution selection uses the 5–12-point gain and the Claude Sonnet null as evidence that prompt performance alone does not identify which bundled component caused the result.