PaperlayerView exact revision on arXiv

Source-linked AI summary

Agentic Code Reasoning

Shubham Ugare, Satish Chandra

arXiv:2603.01896v2cs.SEcs.AIcs.PL

TL;DR

LLM agents need to reason about code semantics across repositories without executing code, but unstructured reasoning can make unsupported claims. The paper introduces semi-formal reasoning, which uses evidence-bearing templates to structure agent exploration and tracing. Across three tasks, it consistently improves accuracy and supports execution-free semantic code analysis, while data contamination remains a limitation for absolute performance estimates.

  • Problem

    The paper asks whether LLM agents can explore codebases and determine code semantics without execution, while addressing the difficulty of establishing correct, thorough reasoning.

  • Method

    Semi-formal reasoning prompts agents to state explicit premises, trace relevant code paths, and provide formal conclusions in structured certificates.

  • Results

    Semi-formal reasoning consistently improves agentic code reasoning across three tasks, including 93% patch-equivalence verification accuracy, 87% code-question-answering accuracy, and 5–12 percentage-point fault-localization gains.

  • Takeaways & Limitations

    Structured reasoning enables meaningful semantic code analysis without execution and supports applications in RL training pipelines, code review, and static program analysis.

  • Takeaways & Limitations

    SWE-bench data contamination may inflate absolute performance numbers, although the primary relative same-model comparisons are less affected.

Abstract

from arXiv · show

Can LLM agents explore codebases and reason about code semantics without executing the code? 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. Unlike unstructured chain-of-thought, semi-formal reasoning acts as a certificate: the agent cannot skip cases or make unsupported claims. We evaluate across three tasks (patch equivalence verification, fault localization, and code question answering) and show that semi-formal reasoning consistently improves accuracy on all of them. For patch equivalence, accuracy improves from 78% to 88% on curated examples and reaches 93% on real-world agent-generated patches, approaching the reliability needed for execution-free RL reward signals. For code question answering on RubberDuckBench Mohammad et al. (2026), semi-formal reasoning achieves 87% accuracy. For fault localization on Defects4J Just et al. (2014), semi-formal reasoning improves Top-5 accuracy by 5 percentage points over standard reasoning. These results demonstrate that structured agentic reasoning enables meaningful semantic code analysis without execution, opening practical applications in RL training pipelines, code review, and static program analysis.

1 Introduction

The paper studies whether LLM agents can explore codebases and reason about code semantics without execution, introducing semi-formal reasoning to make such analysis explicit and evidence-based. Across patch equivalence, code question answering, and fault localization, the approach consistently improves reported accuracy and supports execution-free applications.

  • Motivation: Agentic code reasoning lets LLM agents navigate files, trace dependencies, and gather context for semantic analysis without executing code.The capability targets bug detection, code review, and patch verification in repositories where relevant context spans multiple files.
  • Approach: Semi-formal reasoning bridges unstructured reasoning and formal verification by requiring explicit evidence, traced code paths, and formal conclusions.The templates act as certificates and encourage interprocedural reasoning by requiring agents to follow function calls.
  • Results: 10 percentage points: curated patch-equivalence accuracy rises from 78% with standard reasoning to 88% with semi-formal reasoning.The curated evaluation focuses on whether two patches produce identical test outcomes.
  • Results: 93% verification accuracy is achieved on real-world agent-generated patches with test specifications, compared with 86% for single-shot and 73% for difflib-based similarity.This result supports the use of execution-free verification feedback in training pipelines.
  • Results: 87% accuracy is achieved on RubberDuckBench, while fault-localization Top-5 accuracy improves by 5–12 percentage points over standard agentic reasoning.These evaluations extend beyond patch equivalence to code understanding and bug finding.
  • Implications: The results support meaningful semantic code analysis without execution and potential applications in RL training pipelines, code review, and static program analysis.The paper also describes structured reasoning as a possible flexible alternative to specialized static-analysis algorithms.
  • Limitation: Data contamination in SWE-bench instances may inflate absolute performance numbers, although relative same-model comparisons are expected to be less affected.The agent’s runtime repository exploration provides an additional distinction from simply recalling memorized solutions.

2 Background

The background defines the execution-free agentic setting, narrows semantic equivalence to test-outcome equivalence, and introduces the benchmarks used for fault localization and code question answering.

  • Agentic Verification: Agentic verification allows repository exploration, dependency tracing, and context gathering while forbidding repository-code execution and test-suite execution.The setup uses a minimal SWE-agent configuration with bash tools and a maximum of 100 steps.
  • Patch Equivalence: General semantic equivalence is undecidable, so the paper studies patch equivalence modulo tests: two patches are equivalent when the test suite yields identical pass/fail outcomes.This operational definition makes the evaluation tractable while preserving an execution-based ground truth criterion.
  • Defects4J: Defects4J contains reproducible bugs from real-world Java projects, with buggy and fixed versions plus at least one failing test exposing each bug.Fault localization identifies buggy lines from the failing test without stack traces, error messages, or execution information.
  • Defects4J: Fault-localization evaluation uses Top-N accuracy, the percentage of bugs whose ground-truth buggy lines are covered within the top N predictions.This metric evaluates whether the ranked predictions cover all relevant buggy lines.
  • RubberDuckBench: RubberDuckBench contains 15 code-understanding questions across Python, Java, and C++ repositories, evaluated with expert-written rubrics.The questions require understanding project-specific logic, library semantics, and edge cases; answers are free-form rather than test-execution outcomes.

3 Semi-formal Reasoning

Semi-formal reasoning structures agent exploration through task-specific templates that require explicit premises, evidence, execution traces, and conclusions. The format is intended to reduce unsupported claims while remaining in natural language rather than requiring fully formal proofs.

  • Design Rationale: Semi-formal reasoning combines natural-language intuition with structured logical steps, positioned between informal reasoning and fully formal methods.The paper motivates this design using prior work suggesting that semi-formal approaches can outperform both extremes.
  • Standard Reasoning: Standard reasoning asks for a natural-language explanation and YES/NO conclusion without structural constraints, allowing unverified assumptions.The paper gives as an example assuming that tests do not depend on changes in extra files.
  • Semi-formal Reasoning: Semi-formal reasoning requires explicit premises, per-test execution traces, and a formal conclusion through a structured prompt template.The structure is designed to enforce completeness and reduce unsupported claims while remaining natural-language based.
  • Execution Tracing: Tracing function calls can reveal shadowed definitions and expose patch failures that informal reasoning misses.The motivating Django example shows that discovering a module-level definition changes the predicted behavior of one patch.
  • Task-Specific Certificates: Templates are task-specific: patch equivalence traces per-test behavior, fault localization evaluates suspicious regions, and code question answering uses task-specific evidence structures.All templates require verifiable evidence before a conclusion, while their sections vary by task.
  • Certificate Template: The condensed patch-equivalence certificate requires the agent to fill bracketed fields with evidence gathered from the codebase.The full template adds pass-to-pass tests, confidence levels, and alternative-hypothesis checks.

4 Evaluation

The evaluation tests semi-formal reasoning across patch equivalence, fault localization, and code question answering, using execution-based or known-bug ground truth where available. It consistently improves accuracy, while remaining errors and test-patch dependencies define important boundaries.

  • Patch Equivalence: Semi-formal reasoning reduces errors by nearly half, raising curated patch-equivalence accuracy from 78.2% to 88.8%.The approach performs well on both equivalent and non-equivalent cases but requires about 2.8× as many steps.
  • Patch Equivalence: 93.0% accuracy is achieved by Opus-4.5 for verification with test patches available.Accuracy is computed against actual test-execution results.
  • Limitations: Remaining verification errors primarily involve incomplete execution tracing, guessed third-party library semantics, and dismissing subtle differences.A separate scope boundary is that strong verification performance depends on available fail-to-pass test patches.
  • Fault Localization: Semi-formal reasoning improves fault-localization Top-5 accuracy by +8pp to +12pp under All and by +7pp to +8pp under Any across exploration modes.Agentic semi-formal reasoning reaches 72.1% Top-5 (All) and 88.4% Top-5 (Any).
  • Fault Localization: +5pp Top-5 (All) accuracy is gained over standard reasoning in agentic fault localization across dataset sizes.The Any metric shows the same trend with higher absolute numbers.
  • Code Question Answering: 87.0% code-question-answering accuracy is achieved by Opus with semi-formal reasoning, versus 78.3% for standard agentic reasoning.The gain is +8.7pp; Sonnet shows no further improvement, suggesting benefits vary by model capability.

5 Related Work

Related work spans software-engineering agents, execution-free verification, fault localization, repository understanding, formal verification, reasoning methods, and training pipelines. This paper positions semi-formal reasoning as structured input-side guidance rather than specialized formalization or post-hoc verification.

  • Software-Engineering Agents: Repository-level software-engineering agents differ in how they interact with codebases, decompose bugs, or plan multi-step edits.The cited systems include SWE-agent, OpenHands, Agentless, and CodePlan.
  • Execution-Free Verification: Execution-free verification methods include learned reward models, LLM-generated rubrics, and direct LLM evaluators.The paper distinguishes these approaches from its use of structured reasoning with explicit justification.
  • Program Equivalence and Formal Verification: Program-equivalence work includes formal methods and LLM-based verification, but arbitrary-code formalization remains challenging.EquiBench focuses on small self-contained code pairs rather than repository-level patches with test suites.
  • Reasoning Methods: Semi-formal reasoning differs from post-hoc verification by improving the agent’s requested reasoning process rather than checking outputs afterward.Its structured templates require explicit evidence during reasoning.
  • Training and Scaling: Training pipelines for software-engineering agents increasingly combine environments, procedural generation, reinforcement learning, and hybrid verifiers.Examples include SWE-Gym, R2E-Gym, and SWE-RL.

6 Conclusion and Future Work

Semi-formal structured reasoning improves agentic code reasoning across patch equivalence, code question answering, and fault localization, while supporting execution-free semantic analysis and future extensions.

  • Semi-formal structured reasoning consistently improves agentic code reasoning across all three evaluated tasks, with gains of 5–12 percentage points over standard agentic baselines.
  • 93% verification accuracy on real-world patches is a 7 percentage point improvement over single-shot baselines, enabling execution-free feedback for RL training pipelines.
  • 87% accuracy on RubberDuckBench represents a 9 percentage point gain over standard agentic reasoning for code question answering.
  • Fault localization accuracy improves by up to 12 percentage points on fit-in-context bugs and by 5 percentage points on a larger 90-bug Defects4J evaluation.
  • Structured reasoning templates support semantic code analysis without execution and complement classical static analysis, while lacking traditional tools’ formal guarantees.
  • Future Work: Future work includes applying the approach to security vulnerabilities, code smells, API misuse, hybrid verification, and post-training to reduce prompt overhead.

A Patch Equivalence Semi-formal Reasoning Template

The patch-equivalence template requires explicit premises, per-patch test traces, comparisons, edge-case analysis, and a formal conclusion grounded in existing tests.

  • The template requires a formal proof of patch equivalence or non-equivalence based on explicit claims about each patch and test.
  • Agents state each patch’s predicted test outcome, trace the code behavior, and compare whether outcomes are the same or different.
  • The analysis covers only edge cases exercised by existing tests and explicitly compares both patches’ behavior on those cases.
  • For non-equivalence, the template requires a counterexample showing different outcomes; for equivalence, it requires evidence that no counterexample exists.
  • The formal conclusion records both patches’ test outcomes and determines equivalence modulo the existing tests.
  • Example: In the motivating example, semi-formal reasoning detects name shadowing: Patch 1 raises AttributeError while Patch 2 succeeds, so the patches are not equivalent.

B Fault Localization Semi-formal Reasoning Template

The fault-localization template traces from test semantics through code paths to formal divergence claims, then ranks predictions supported by those claims.

  • The template uses a PREMISE → CLAIM → PREDICTION chain linking test expectations, code divergences, and ranked fault locations.
  • Phase 1: Test Semantics Analysis: Phase 1 formalizes the failing test’s calls, assertions, expected behavior, and observed failure mode as premises.
  • Phase 2: Code Path Tracing: Phase 2 traces each significant method call from the test into production code, recording its location, behavior, and relevance.
  • Phase 3: Divergence Analysis: Phase 3 identifies implementation divergences and states each as a formal claim tied to a specific test premise.
  • Phase 4: Ranked Predictions: Phase 4 converts supported divergence claims into ranked predictions, with each prediction citing its supporting claims.
  • Structured Exploration Format: Structured exploration requires hypotheses, evidence, confidence, observations, hypothesis updates, unanswered questions, and next-action rationales.

C Case Study for Mockito_8

The Mockito_8 case study shows that semi-formal tracing identifies a root-cause overwrite in generic type registration rather than stopping at the visible recursive crash site.

  • Mockito_8’s StackOverflowError arises from infinite recursion in Java generic type resolution for a self-referential type.
  • Standard reasoning localized the problem to getActualTypeArgumentFor, the crash site, but missed the upstream cause.
  • Code Path Tracing: Semi-formal reasoning traced ten observations through inference, return-type resolution, type-parameter registration, and bound processing.
  • Divergence Analysis: The agent tested multiple type scenarios and verified that non-self-referential cases preserve the existing bounded-type mapping.
  • Divergence Analysis: For SelfRef<T extends SelfRef<T>>, registration overwrites T → TypeVarBoundedType(T) with T → T, creating the self-reference that recurses infinitely.
  • Ranked Predictions: The structured analysis ranked registerTypeVariablesOn at lines 73–81 as the root cause and getActualTypeArgumentFor at lines 181–189 as the crash site.
  • Why the Structured Template Mattered: The four-phase template led to a Top-1 correct root-cause identification across two turns instead of stopping at the symptom.

D Code Question Answering Details

Semi-formal code-question answering uses structured certificates to make agents verify implementations, data flow, semantic properties, and alternative hypotheses before answering. The approach can improve evidence-based reasoning, but deeper traces can still produce confident errors when downstream paths are missed.

  • Reasoning Template: Semi-formal templates require explicit function traces, data-flow analysis, semantic properties, alternative-hypothesis checks, and evidence-backed final answers.The format is designed to document evidence systematically before the agent commits to an answer.
  • Reasoning Template: The template directs agents to locate implementations, record exact signatures and behavior, identify differences with file:line evidence, and test the opposite conclusion.These steps replace guesses based on naming conventions with explicit verification.
  • Success Case: 100% score was achieved in the cpp_3 invariant example after tracing map initialization and enum assignments to show that non-existent keys are impossible.Standard reasoning scored 79% and incorrectly elevated irrelevant invalid-key handling.
  • Failure Case: 57% score was produced in the py_5 failure case, where the agent correctly found a possible empty BUILD_DIR but incorrectly concluded that an explicit check was needed.The correct answer was that Runner’s constructor already handles the case.
  • Failure Case: The failure arose because the agent missed Runner’s downstream build_directory check through find_fuzzer_path, which returns None and triggers a CorpusPruningException when the value is falsy.The example shows that a plausible chain can remain wrong without verifying all downstream paths.
  • Evaluation Breakdown: Code-question accuracy varies by language, with Java questions described as most challenging because they rely on framework-specific semantics.Table 7 is identified as the language-level accuracy breakdown for Opus-4.5 using semi-formal reasoning.
Loading 2603.01896v2…