Source-linked AI summary
NEUROTESTGEN: Neuro-Symbolic Guided Test Generation with Large Language Models
Ruixin Zhang, Jiho Shin, Hung Viet Pham, Song Wang
TL;DR
Precise structural coverage is challenging because LLMs struggle with path constraints, while symbolic execution can fail to produce realistic tests and scale. NEUROTESTGEN combines symbolic guidance with LLM test synthesis and iterative validation; it outperforms the state-of-the-art approach across LLMs on the benchmark evaluation.
Problem
Automated tests that reach specific lines or branches must satisfy intricate path conditions, which LLMs struggle to produce and symbolic execution alone does not turn reliably into developer-friendly tests.
Source: §1 · pp. 1–2Method
NEUROTESTGEN combines symbolic path-constraint guidance with LLM test synthesis and iterative validation, using LLM reasoning for complex object-related constraints.
Source: §1 · p. 2Results
NEUROTESTGEN consistently improves on Panta across multiple LLMs; with Claude Sonnet 4.6 it achieves 92.91% line coverage and 88.89% branch coverage.
Source: §1 · pp. 2–3Takeaways & Limitations
The evaluation supports combining symbolic reasoning with LLM-guided synthesis to improve automated unit-test effectiveness and robustness across LLMs of varying capability and cost.
Source: §1 · p. 3Symbolic execution remains constrained by path explosion and incomplete modeling of complex heap states; domain-specific libraries, deep semantics, and iterative computational overhead also remain challenges.
Source: §6 · p. 10
Abstract
from arXiv · showhide
Ensuring high structural coverage remains a fundamental challenge in automated test generation, particularly for complex software systems where reaching specific lines or branches requires satisfying intricate control- and data-flow constraints. Large Language Models (LLMs) have recently demonstrated strong capabilities in producing human-like test cases; however, they often struggle to generate inputs that satisfy precise path conditions. Conversely, symbolic execution can systematically derive such constraints, but it often fails to construct realistic, executable test cases and is constrained by scalability limitations. In this paper, we introduce NEUROTESTGEN, a hybrid approach that integrates symbolic execution with LLM-driven test synthesis to generate test cases targeting on-demand code coverage. Given a set of target statements within a method, NEUROTESTGEN first employs a symbolic analysis engine (i.e., the Z3 SMT solver) to extract path-specific constraints and construct a symbolic guidance specification for the desired coverage goal. This specification is then used to guide an LLM in synthesizing concrete test cases that are both structurally valid and semantically meaningful. For paths involving complex object-related constraints that are difficult for SMT solvers to handle, NEUROTESTGEN leverages LLMs to infer plausible constraints. Furthermore, NEUROTESTGEN incorporates an iterative feedback loop that validates LLM-generated tests and provides corrective guidance until the target line or branch is covered or a limit is reached. Our empirical evaluation on a widely used benchmark demonstrates that NEUROTESTGEN significantly outperforms the state-of-the-art approach across multiple LLMs, including Llama 3.3 70B1, GPT-4o Mini, Claude 3.5 Haiku3, and Claude Sonnet 4.6.
1 Introduction
Precise structural-coverage test generation remains difficult because LLMs struggle with path constraints, while symbolic execution can struggle to scale and produce developer-friendly tests. NEUROTESTGEN combines symbolic guidance with LLM synthesis and iterative validation; its evaluation reports improved coverage over Panta across multiple LLMs.
1 Introduction
- Traditional automated testing methods have advanced systematic exploration, yet may struggle to scale to real-world software and produce tests developers can adopt.The introduction names symbolic execution, search-based testing [8], and concolic execution.Source: §1 · p. 1
- LLMs can generate realistic, human-like tests but struggle to satisfy the precise control- and data-flow conditions needed for target coverage.Reaching a target may also require maintaining object invariants or triggering specific program states.Source: §1 · p. 2
- Panta guides LLMs with uncovered paths and dynamic feedback, but may prompt for infeasible paths without resolving their constraints.This can lead to repeated attempts, wasted tokens, redundant generations, and unstable performance.Source: §1 · p. 2
- Symbolic execution derives path constraints but often produces low-level inputs rather than readable tests, and can face path-explosion and heap-reasoning limits.The paper frames this as complementary to LLMs’ test synthesis strengths and path-constraint weakness.Source: §1 · p. 2
- NEUROTESTGEN combines symbolic path constraints, LLM test synthesis, and iterative execution feedback to target lines or branches.For object-related paths that are difficult for SMT solvers, LLMs infer plausible constraints; corrective guidance continues until coverage or an iteration limit.Source: §1 · p. 2
- Across four LLMs, NEUROTESTGEN improves on Panta; with Claude Sonnet 4.6 it reaches 92.91% line coverage and 88.89% branch coverage.The evaluation uses Defects4J, including 2,971 methods from 130 classes across 14 projects.Source: §1 · pp. 2–3
2 Problem Formulation
NEUROTESTGEN separates uncovered paths into numerical and object-related cases, applying symbolic solving to numerical constraints and LLM reasoning to object semantics. It builds path-guided prompts, validates generated tests, and iterates toward coverage.
2 Problem Formulation
- The workflow classifies uncovered paths as pure numerical or object-related, then handles them differently during symbolic execution.Numerical paths use primitive-variable predicates; object-related paths may involve object creation, method calls, APIs, or complex strings.Source: §2 · p. 3
2.1 Pure Symbolic Execution for Solving Pure Numerical Paths
- For pure numerical paths, SMT-based symbolic execution derives constraints from branch predicates and can solve them to produce concrete inputs for an uncovered branch.The example’s constraint is 0 == rem, where rem = n % 3.Source: §2.1 · pp. 3–4
- The current numerical-path solver skips loop bodies to limit constraint complexity and solving overhead.The paper notes that loop handling can require unrolling or invariant inference.Source: §2.1 · p. 4
2.2 LLM-Based Path Solving for Object-related Paths
- Object-related paths can require semantic conditions, such as a singleton-object identity check and a string API predicate, that SMT handles poorly.The example requires mode to reference Mode.STRICT and text to start with “A”.Source: §2.2 · p. 4
- For object-related paths, LLM-Path-Solver receives source code, the method signature, branch conditions, and path context to infer inputs for the target branch.The example input classify("Apple", Mode.STRICT) reaches the uncovered branch.Source: §2.2 · pp. 4–5
- LLM-Verifier symbolically traces proposed inputs; failed checks return rejection reasons for iterative refinement until validation or a retry limit.Confirmed values are then supplied as path-guidance examples for test generation.Source: §2.2 · p. 5
2.3 Prompt Building and Test Case Generation
- Test-generation prompts combine candidate paths and input references with variable and container type annotations and path-resolving code.The path representation includes definitions or object creation, operations, and conditional or loop execution requirements, plus an input guide from Z3 or LLMs.Source: §2.3 · p. 5
- Failed generated tests are returned with error messages for refinement; passing tests are retained, and coverage is reevaluated until the target or a limit is reached.The process covers compilation and runtime failures as well as subsequent coverage evaluation.Source: §2.3 · p. 5
3 Experiments
The experiments compare NEUROTESTGEN with Panta under a shared benchmark and model protocol. They report coverage, pass rate, and cost, with coverage averaged across target classes within each project.
3.1 Datasets
- Original project test suites are discarded, and tests are generated from scratch for target classes to reduce existing-test bias and standardize comparisons.Source: §3.1 · p. 5
3.2 Baseline and LLM Selection
- NEUROTESTGEN is compared with Panta using four LLMs: Llama 3.3 70B, GPT-4o Mini, Claude 3.5 Haiku, and Claude Sonnet 4.6.The protocol, benchmark setup, and models follow Panta for comparability, with Claude Sonnet 4.6 added as a coding-oriented model.Source: §3.2 · p. 6
3.3 Evaluation Metrics
- The evaluation reports line coverage, branch coverage, pass rate, and monetary cost, averaging class-level coverage across target classes within each project.Pass rate counts generated tests that compile and run without failures or runtime exceptions.Source: §3.3 · p. 6
4 Results
NEUROTESTGEN improves on Panta across evaluated models and coverage metrics, while performance and generation cost vary substantially by model. Its full framework also outperforms symbolic execution alone on line and branch coverage.
4.1 Main Results of NEUROTESTGEN’s Performance
- Branch coverage rises from 65.15% to 70.87% with Claude 3.5 and from 87.24% to 88.89% with Claude 4.6; pass rates also improve slightly.Average pass rates increase from 65.92% to 66.34% with Claude 3.5 and from 96.81% to 96.88% with Claude 4.6.Source: §4.1 · pp. 6–7
- NEUROTESTGEN improves over Panta in average line coverage from 70.88% to 75.87% with Claude 3.5 and from 91.68% to 92.91% with Claude 4.6.The comparison covers projects using both base models.Source: §4.1 · p. 6, Table 1 · p. 7
4.3 Ablation Study
- NEUROTESTGEN’s improvements over Panta are larger with Claude 3.5 than with Claude 4.6, while the ablation attributes complementary roles to precise symbolic reasoning and flexible LLM synthesis.The symbolic-only variant can still perform relatively strongly because LLMs can infer object constructions, API sequences, and input values from learned programming patterns.Source: §4.1 · p. 7, §4.3 · p. 8
4.2 Impact of Different Models
- Claude Sonnet 4.6 costs $904.28, compared with $116.23 for Llama 3.3 70B, $183.50 for GPT-4o Mini, and $428.41 for Claude 3.5 Haiku.Claude 3.5 Haiku is described as offering a more favorable performance-cost balance.Source: Figure 4 · p. 7, §4.2 · p. 8
- Across the evaluated models, Claude Sonnet 4.6 has the highest average line coverage (92.91%), branch coverage (88.89%), and pass rate (96.88%).Claude 3.5 Haiku reaches 75.87% line coverage and 70.87% branch coverage, while Llama 3.3 and GPT-4o Mini perform lower, particularly on pass rate and branch coverage.Source: §4.2 · pp. 7–8, Table 2 · p. 7
4.3 Ablation Study
- With Claude 3.5 Haiku, the full framework raises average line coverage from 73.45% to 75.87% and branch coverage from 68.53% to 70.87% over symbolic execution alone.With Claude Sonnet 4.6, line coverage rises from 92.35% to 92.91% and branch coverage from 88.15% to 88.89%.Source: Table 3 · p. 8, §4.3 · p. 8
5 Related Work
Prior LLM-based test generation research includes methods for generating tests, strengthening assertions, and using feedback to improve test quality and coverage. Symbolic-execution research provides systematic path reasoning, while newer work explores combinations of symbolic methods and LLMs; NEUROTESTGEN differentiates itself through adaptive use of each.
5.1 LLM-Based Test Generation
5.2 Symbolic Execution
- Symbolic execution accumulates path conditions for systematic test generation, while concolic execution and KLEE address path diversity and high-coverage testing.The related-work discussion also identifies path explosion and constraint-solver bottlenecks as scalability challenges.Source: §5.2 · p. 9
- Recent hybrid approaches include executable path variants for LLM interpretation [29], translating Python constraints into Z3 code [24], and prompting or concolic methods for structured test generation [21].The cited passage also names [13] and [25] among recent integrations of LLMs with symbolic and concolic execution.Source: §5.2 · p. 9
- NEUROTESTGEN adaptively applies SMT-based execution to numerically constrained paths and verifier-guided LLM reasoning to semantically complex paths.The paper presents this as combining precise symbolic reasoning with LLM semantic understanding.Source: §5.2 · p. 9
6 Conclusion
NEUROTESTGEN combines symbolic execution with LLM-driven test synthesis and significantly outperforms the state-of-the-art approach on a standard benchmark. The conclusion also identifies scalability, semantic-reasoning, and computational-cost limitations.
6 Conclusion
- NEUROTESTGEN combines symbolic execution with LLM-driven test synthesis to generate test cases.The paper reports that it significantly outperforms the state-of-the-art approach on a standard benchmark.Source: §6 · p. 9
- Symbolic execution remains constrained by path explosion and incomplete modeling of complex heap states.These constraints limit symbolic execution's scalability.Source: §6 · p. 9
- The approach may struggle with highly domain-specific libraries or programs requiring deep semantic understanding.Iterative refinement also adds computational overhead through repeated compilation, execution, and prompting.Source: §6 · p. 10
A Failure Analysis
A qualitative case study examines methods where NEUROTESTGEN falls short of full coverage, using manual inspection and open coding to identify recurring limitation patterns.
A Failure Analysis
- The case study selects methods where NEUROTESTGEN achieves less than full coverage and manually inspects their uncovered lines and branches.It uses open coding to identify recurring patterns and underlying causes.Source: A Failure Analysis · p. 12
- The analysis reports three primary categories of limitations.The supplied passage does not specify the categories.Source: A Failure Analysis · p. 12
A.1 Partially Covered Lines and Branches
JaCoCo-based prompting can miss partially covered branches, leaving feasible paths within conditionals unexplored even when method-level coverage appears complete. The analysis illustrates this gap and proposes finer-grained feedback and path prioritization.
A.1 Partially Covered Lines and Branches
- JaCoCo may report a method fully covered even when constituent lines or branches are only partially exercised.Partially covered conditional statements are not always surfaced or prioritized in prompts, so unexplored paths may remain.Source: §A.1 · p. 12
- Figure 5 uses green for fully covered lines, yellow for partially covered branches, and red for uncovered conditions within a compound predicate.The visualization highlights the distinction between method-level coverage and untested predicate combinations.Source: Figure 5 · p. 12, §A.1 · p. 13
- 99.04% line coverage and 93.15% branch coverage in handleX() coexist with feasible compound-condition combinations left unexplored.The partly covered branch is not surfaced as an actionable target for further exploration.Source: §A.1 · pp. 12–13
- Once a method is deemed fully covered, the approach exposes no additional path information in the prompt to guide further coverage improvement.The authors propose fine-grained feedback for partially covered branches and systematic enumeration and prioritization of unexplored path combinations.Source: §A.1 · p. 13
A.2 Unreachable Paths
JaCoCo can count infeasible or unreachable code as missed, so coverage signals may overstate the test-adequacy gap. The gcd() example shows a condition that remains unreachable because its required state change occurs only in a loop that does not execute.
A.2 Unreachable Paths
- JaCoCo counts infeasible branches or unreachable lines as missed when they appear in compiled bytecode and coverage counters.Its runtime-based reports do not distinguish feasible uncovered paths from inherently infeasible ones.Source: §A.2 · p. 13
- In gcd(), k remains unchanged because the loop at line 562 does not run, leaving the dependent condition at line 568 unreachable along that path.JaCoCo still marks the line partially covered, potentially overstating the test-adequacy gap.Source: §A.2 · p. 13
A.3 LLM Capability Limitation
LLM limitations reduce coverage through errors in both path solving and test generation. The reported problems include code misunderstandings, missing cross-file object context, complex control flow, and invalid tests.
A.3 LLM Capability Limitation
- Model limitations affect both the LLM-based path solver and test generator, with errors in code understanding and code generation reducing coverage.The authors report that model capability also affects object-related path solving.Source: §A.3 · p. 13
- Misunderstood type hierarchies or invoked-method behavior can lead the path solver to accept infeasible inputs or miss a target condition.A generated HashSet cannot satisfy the cited Set condition; another path required an invoked method to return null.Source: §A.3 · p. 14
- When customized object definitions are outside the prompt, the LLM may infer invalid inputs from partial path information.For decode(), the missing Context definition led to an input with context.eof = true despite a requirement that it be false.Source: §A.3 · p. 14
- Paths with multiple calls, loops, object invocations, and nested conditions can overwhelm the LLM’s tracking of states and constraints.The authors say compact code and conditions dependent on earlier updates can cause inputs to satisfy only part of a path.Source: §A.3 · p. 15
- A correct path solution may still leave coverage unchanged if the generated test fails and cannot be repaired.One test remained uncovered after three fixing rounds because its assertion was incorrect.Source: §A.3 · p. 15
B Impact Statements
NEUROTESTGEN combines symbolic execution with LLMs to bridge constraint reasoning and test synthesis. The paper presents this hybrid approach as a basis for targeted coverage and readable tests, while pointing to trade-offs and future directions.
B Impact Statements
- The work demonstrates a neuro-symbolic approach that bridges precise constraint reasoning and high-quality test synthesis.It combines symbolic execution with LLMs to target structural coverage while generating readable, developer-friendly tests.Source: B Impact Statements · pp. 15–16
- The reported findings suggest hybrid designs can balance scalability and precision for real-world applications.The authors also say empirical improvements on Defects4J demonstrate the approach’s effectiveness.Source: B Impact Statements · p. 16
- The work motivates future testing research in constraint-guided generation, feedback-driven refinement, scalable analysis, and path-level coverage and usability benchmarks.The authors describe the approach as a foundation for AI-assisted testing systems that are semantically grounded and practically deployable.Source: B Impact Statements · p. 16