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: 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

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. --- kb/sources/.snapshots/agentic-code-reasoning.md @ sha256:19f33415923cf24ea366560df5f62c897f6ef94c5cee0891c54abfeae2e37a76 — Abstract.

Crucially, the agent cannot execute repository code or run its test suite: dependencies are not installed and the environment is not sandboxed. --- kb/sources/.snapshots/agentic-code-reasoning.md @ sha256:19f33415923cf24ea366560df5f62c897f6ef94c5cee0891c54abfeae2e37a76 — Section 2.1, Agentic vs. Single-Shot Verification.

For fault localization on Defects4J just2014defects4j, semi-formal reasoning improves Top-5 accuracy by 5-12 percentage points over standard agentic reasoning. --- kb/sources/.snapshots/agentic-code-reasoning.md @ sha256:19f33415923cf24ea366560df5f62c897f6ef94c5cee0891c54abfeae2e37a76 — Section 1, Contributions.

Even with semi-formal analysis, 19 cases are incorrect. --- kb/sources/.snapshots/agentic-code-reasoning.md @ sha256:19f33415923cf24ea366560df5f62c897f6ef94c5cee0891c54abfeae2e37a76 — Section 4.1.1, Curated Dataset Evaluation.

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. --- kb/sources/.snapshots/agentic-code-reasoning.md @ sha256:19f33415923cf24ea366560df5f62c897f6ef94c5cee0891c54abfeae2e37a76 — Section 4.3, Code Question Answering.

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. --- kb/sources/.snapshots/agentic-code-reasoning.md @ sha256:19f33415923cf24ea366560df5f62c897f6ef94c5cee0891c54abfeae2e37a76 — 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.