PaperlayerView exact revision on arXiv

Source-linked AI summary

Large Language Model Powered Symbolic Execution

Yihe Li, Ruijie Meng, Gregory J. Duck

arXiv:2505.13452v2cs.PL

TL;DR

Traditional symbolic execution struggles with unbounded loops, external environments, and heaps, while LLM-based analysis faces accuracy and scale challenges. The paper introduces path-based LLM symbolic execution with code-based path constraints, implemented in AutoBug. The authors report improved accuracy and scale, especially for smaller models that can run on consumer-grade hardware.

  • Problem

    Traditional symbolic execution has limitations with unbounded loops, external environments, and heap-manipulating programs, while LLM analysis faces accuracy and scalability challenges.

    Source: §1 · p. 2, Traditional Symbolic Execution · p. 10

  • Method

    The approach decomposes analysis into path-based subtasks and represents path constraints as code for direct LLM reasoning, implemented in the lightweight, language-agnostic AutoBug engine.

    Source: §1 · pp. 2–3, §7 · p. 25

  • Results

    The authors report that path-based decomposition improves LLM-based program analysis accuracy and scale, especially for small LLMs and real-world problems.

    Source: §5.5 · p. 24

  • Takeaways & Limitations

    The authors conclude that higher accuracy can be achieved with smaller models running on consumer-grade hardware, and that a lightweight, language-agnostic workflow can still achieve good results.

    Source: §5.5 · p. 24

    LLM-based symbolic execution is not suited to every application, and path-based decomposition may still explode despite being guaranteed to terminate.

    Source: Limitations · p. 24

Abstract

from arXiv · show

Large Language Models (LLMs) have emerged as a promising alternative to traditional static program analysis methods, such as symbolic execution, offering the ability to reason over code directly without relying on theorem provers or SMT solvers. However, LLMs are also inherently approximate by nature, and therefore face significant challenges in relation to the accuracy and scale of analysis in real-world applications. Such issues often necessitate the use of larger LLMs with higher token limits, but this requires enterprise-grade hardware (GPUs) and thus limits accessibility for many users. In this paper, we propose LLM-based symbolic execution -- a novel approach that enhances LLM inference via a path-based decomposition of the program analysis tasks into smaller (more tractable) subtasks. The core idea is to generalize path constraints using a generic code-based representation that the LLM can directly reason over, and without translation into another (less-expressive) formal language. We implement our approach in the form of AutoBug, an LLM-based symbolic execution engine that is lightweight and language-agnostic, making it a practical tool for analyzing code that is challenging for traditional approaches. We show that AutoBug can improve both the accuracy and scale of LLM-based program analysis, especially for smaller LLMs that can run on consumer-grade hardware.

1 Introduction

The paper combines symbolic execution’s path-based structure with LLM inference to address complementary limitations, representing path constraints as code so LLMs can reason directly over them. Its introduction motivates this approach through the challenges of approximate LLM reasoning and traditional symbolic execution’s difficulty with loops, external environments, and heap-manipulating programs.

1 Introduction

  • LLM-based symbolic execution decomposes analysis by program paths and represents path constraints as code, enabling direct LLM reasoning without translation into formal logic.AutoBug implements this approach as a lightweight, language-agnostic engine; the authors report improved accuracy and scale, especially for smaller models on consumer-grade hardware.Source: §1 · pp. 2–3

2.1.1 Symbolic Execution.

  • Symbolic execution explores multiple paths using symbolic values and path constraints, then uses theorem provers or SMT solvers to check properties such as assertions.For a conditional, it forks constraints for the two branches; each path’s final constraint can be checked against a postcondition.Source: §2.1.1 · p. 3

2.1.2 Large Language Models.

  • LLMs can reason over code directly, but their approximate inference can be incomplete or wrong, unlike the deductive reasoning of theorem provers.LLM-based analysis is typically prompt-engineered for particular tasks rather than general and principled.Source: §1 · p. 2, §2.1.2 · p. 4

2.2.1 Limitation: Handling Loops (and Recursion).

  • Unbounded loops can cause symbolic execution to unroll indefinitely; tools such as KLEE instead use iteration bounds, yielding bounded but incomplete exploration.Loop invariants can avoid explicit unrolling when known, but discovery may work only for simple loops and the general case is computationally hard or undecidable.Source: §2.2.1 · p. 4

2.2.2 Limitation: Handling External Environment.

  • External functions and inputs usually require precise specifications, so users may need to create stubs or models, a manual effort that tends not to scale.Concretizing symbolic variables can also leave program behavior incompletely explored.Source: §2.2.2 · p. 4

2.2.3 Limitation: Heap Manipulating Programs.

  • Traditional theorem provers and SMT solvers have limited support for mutable structures with complex invariants, including linked lists, trees, and DAGs.Separation Logic tools offer some support, but VeriFast is manual and annotation-heavy, while Infer’s heuristics cover common invariants rather than arbitrary heap shapes.Source: §2.2.3 · p. 5

Discussion.

Traditional analysis and LLMs face different practical limits: symbolic execution struggles with some real-world code, while LLMs are constrained by scale and approximate reasoning. The proposed approach combines path-based decomposition with direct LLM reasoning over source-code representations.

Discussion.

  • Figure 1’s example combines unbounded loops, environment interaction, and heap manipulation, challenging traditional symbolic execution tools such as KLEE.The passage describes the example as relatively simple despite these challenges.Source: Discussion · p. 5

2.3.1 Limitation: Scale.

  • LLM token limits can exclude medium-to-large codebases from a single analysis input.The token limit caps both input and output.Source: §2.3.1 · p. 6

2.3.2 Limitation: Approximate Oracles.

  • LLMs use approximate, pattern-based reasoning rather than formal deduction, and verbose prompts with irrelevant information can further hurt performance [44].The cited studies report worse performance even when token limits are not exceeded.Source: §2.3.2 · p. 6

2.4 Our Approach

  • AutoBug represents path constraints as strongest-postcondition predicates over ordinary source code, avoiding translation into a less expressive solver language.The LLM reasons directly over the derived subprogram and precondition.Source: §2.4 · p. 6
  • Path-based decomposition creates smaller, targeted prompts that focus on statements relevant to the analysis and are intended to improve scale and accuracy.The approach uses program slicing and can infer likely behavior of external calls without explicit environment modeling.Source: §2.4 · p. 7
  • In a second example, the derived program is about 64% smaller, and the LLM identifies that strdup() may return NULL, so the postcondition does not hold.The reported token counts are 419 for the original and 149 for the derived program.Source: §2.4 · p. 8

Algorithm.

The algorithm parses a program, partitions its control-flow paths, and sends derived subprograms to an LLM to assess a postcondition.

Algorithm.

  • The frontend parses the program into an AST, builds a control-flow graph, and represents its paths as partitions, each potentially covering infinitely many paths.The partitions collectively represent the set of paths through the graph.Source: Algorithm · p. 8
  • For each partition, the algorithm generates a derived subprogram and constructs a natural-language prompt containing the precondition, subprogram, and postcondition.The subprogram is rendered back into source-code text before prompting.Source: Algorithm · p. 8
  • The LLM may establish or refute the postcondition; with partitions ordered by slice, the algorithm returns the least subprogram deemed to refute it, or HOLDS if none does.These outcomes depend on the underlying LLM’s reasoning capabilities.Source: Algorithm · p. 8

Summary.

The paper develops LLM-based symbolic execution as path analysis over derived subprograms, then describes AutoBug as a lightweight implementation for real-world languages.

Summary.

  • The paper studies LLM-based symbolic execution and shows that tasks can be decomposed over derived subprograms representing paths or sets of paths.The set of partitions considered is finite, so the method terminates even for unbounded loops.Source: Summary · pp. 8–9
  • AutoBug applies the approach to languages such as C, Java, and Python using approximate parsing and dependency analysis rather than heavyweight, language-specific compiler frameworks.The approach is described as mostly language-agnostic apart from aspects such as parsing.Source: Summary · p. 9

3.1 Symbolic Execution Foundations

  • The foundations define symbolic execution as unfolding program paths and solving a verification condition for each path using strongest-postcondition semantics.A Hoare triple holds when each individual path’s verification condition holds.Source: §3.1 · pp. 9–10

Traditional Symbolic Execution.

The paper contrasts theorem-prover-based symbolic execution with direct LLM reasoning over path constraints, then introduces truncation, slicing, and coverage-based partitioning to handle path growth.

Traditional Symbolic Execution.

  • Traditional symbolic execution translates path constraints into a theorem prover’s formal input language, while path explosion and unsupported operations or theories limit its reach.The cited KLEE configuration does not support heap-manipulating programs.Source: Traditional Symbolic Execution · p. 10

3.2 LLM-Based Symbolic Execution (Path-Based)

  • Path-based LLM execution asks whether the postcondition follows from a path constraint directly represented as code, but paths may be infinite, too long, or contain irrelevant statements.The example assumes a multiset implementation and positive values from read; its path represents two loop iterations.Source: §3.2 · p. 11

3.3 LLM-Based Symbolic Execution (Slice-Based)

  • Truncation generalizes the path constraints in a partition, and slicing removes statements while preserving the postcondition check for the truncated program.Back slicing removes statements not data- or control-flow-dependent on variables in the postcondition.Source: §3.3 · pp. 11–12
  • Simplification rules preserve truncation while reducing the resulting subprogram’s token count, which benefits LLM prompting.The rules replace unreachable branches with assumptions.Source: §3.3 · p. 12

3.3.2 Partitioning.

  • The partitioning algorithm explores CFG paths by distinct node coverage and prunes previously seen coverage prefixes, producing a finite set of representative paths.Each representative path defines a partition used to construct a truncated program and slice.Source: §3.3.2 · pp. 13–14
  • Coverage-based partitioning yields a finite set of slices, so slice-based execution terminates even for unbounded loops, with each slice bounded by the original program’s size.A single slice can generalize infinitely many loop paths.Source: §3.3 · p. 12, §3.3.2 · p. 14

4 LLM-Based Symbolic Execution in Practice

The workflow ports path-based symbolic execution to real programming languages through language-agnostic analysis steps and an approximate design. AutoBug parses programs, partitions and slices paths, renders coherent source-language prompts, and queries an LLM.

4 LLM-Based Symbolic Execution in Practice

  • The design assumes approximate steps are acceptable when overall accuracy is not significantly degraded, and the core algorithms need only a suitable parsed representation.This lets the workflow target real-world languages without requiring every step to be perfectly precise.Source: §4 · pp. 14–15

4.1 Partitioning and Truncated Slice Generation

  • Tree-sitter parses code into a unified AST, which is lowered to a language-agnostic CFG for path partitioning and truncated slices based on post-condition dependencies.Slicing removes nodes that are not control- or data-flow dependent on the post-condition.Source: §4.1 · p. 15

4.2 Truncated Slice Rendering

  • The renderer turns each slice back into coherent source code, retaining enclosing context and formatting before prompting the LLM to return PASS or FAIL.The prompt follows a Hoare-triple structure; each path through the slice corresponds to an equivalent path in the original program.Source: §4.2 · pp. 15–16

4.3 Implementation

  • AutoBug accepts C, Java, or Python programs and code, constraint, or natural-language pre- and post-conditions, then submits size-ordered slice prompts to configurable LLMs.Its lightweight, approximate implementation avoids language-specific compiler infrastructure, apart from parsing and some rendering elements.Source: §4.3 · p. 16

5 Evaluation

The evaluation tests AutoBug’s accuracy, scalability, and language support using REval and CodeForces subjects and several forms of Hoare triples. It compares AutoBug with an undecomposed LLM baseline and, on formally specified cases, traditional symbolic execution tools.

5 Evaluation

  • The evaluation asks whether AutoBug improves accuracy, scales to large real-world programs, and supports multiple programming languages.These are the three stated research questions.Source: §5 · p. 17

5.1.1 Dataset.

  • REval contains 85 Python solutions, while CodeForces contributes 662 Python and C subjects; evaluations construct natural-language or manually annotated pre- and post-conditions.The manually annotated Mixed-Manual set samples 30 subjects each from REval and CodeForces; CodeForces subjects were published in June 2025.Source: §5.1.1 · p. 17

5.1.2 Baselines.

  • The baselines are whole-program ad-hoc LLM analysis and traditional tools, with CrossHair and KLEE comparisons limited to Mixed-Manual’s executable-code conditions.Traditional tools were not compared on the other datasets because they cannot handle natural-language post-conditions.Source: §5.1.2 · p. 17

5.1.3 Test Models.

  • The study selects five popular open models, including models at different parameter sizes where available, and reports averages over three runs rounded to integers.The listed model families are Llama3, Phi-4, DeepSeek-R1, Gemma3, and Qwen3.Source: §5.1.3 · p. 18

Method.

The method compares AutoBug with ad-hoc LLM analysis and traditional symbolic execution tools, measuring accuracy against a ground truth for each subject.

Method.

  • AutoBug is compared with ad-hoc LLM analysis on REval-Desc, CodeForces-Automatic, and Mixed-Manual.Traditional-tool comparisons with CrossHair and KLEE use Mixed-Manual, where conditions are executable Python or C code.Source: Method · p. 18
  • Accuracy is measured against ground truth derived from provided test suites when available or from manual verification.Source: Method · p. 18
  • The evaluation checks both counterexample generation and verification of post-conditions.Source: Method · p. 18

Main result.

AutoBug improves accuracy over ad-hoc LLM analysis across the evaluated datasets and outperforms traditional symbolic execution tools on Mixed-Manual. It also supports expressive post-conditions, including natural language.

Main result.

  • AutoBug raises average accuracy from 84.7% to 90.6% on REval-Desc, 79.2% to 86.4% on CodeForces-Automatic, and 66.7% to 73.3% on Mixed-Manual, beating ad-hoc analysis in 20 of 24 experiments.Source: Main result · p. 18, Table 2 · p. 19
  • On Mixed-Manual, AutoBug successfully analyzes 73.3% of subjects, compared with 46.7% for traditional tools.The authors attribute the gap to traditional symbolic execution’s limitations with constructs such as nested loops.Source: Table 3 · p. 19, Main result · p. 19
  • Compared with traditional tools, AutoBug supports more expressive pre- and post-conditions, including natural-language conditions.Source: Main result · p. 19
Loading 2505.13452v2…