NeuroTestGen: Neuro-Symbolic Guided Test Generation with Large Language Models

For pure numerical paths, we employ SMT-based symbolic execution to precisely solve path constraints without relying on LLM reasoning. Figure 2(a) illustrates such a case. In the example, the uncovered branch at lines 13–15 depends entirely on numerical constraints derived from the input variable n. Since the path contains no object states, heap references, or complex API semantics, it can be solved accurately using symbolic reasoning alone.

To solve this type of path, we leverage the Z3 SMT solver De Moura and Bjørner (2008). We first extract the method parameters and create corresponding symbolic variables according to their declared types. During symbolic execution, the selected path is traversed sequentially while maintaining a symbolic environment that records the symbolic value of each program variable. Assignment statements update the symbolic state, whereas the original symbolic inputs are preserved for final model construction. For each branch condition along the path, we translate the predicate into a Z3-compatible constraint. If the execution path follows the false branch of a condition, the predicate is negated before being added to the solver (e.g., we translate if (n < 0) is False to Not(n < 0) and add it to the solver). Numerical expressions involving arithmetic operators, modulo operations, and bitwise operations are directly encoded into SMT formulas. In the example shown in Figure 2(a), the symbolic executor accumulates constraints from the preceding branches and finally derives the constraint associated with line 13, i.e., 0 == rem, where rem = n % 3. Solving the resulting constraint system enables the solver to synthesize concrete input values that drive execution into the uncovered branch at line 14. To control solving complexity and maintain efficiency, we currently skip loop bodies during symbolic execution, as loop handling typically requires loop unrolling or invariant inference, both of which can substantially increase constraint complexity and solving overhead. After all constraints along the selected path are collected, Z3 checks the satisfiability of the path condition. If the constraint set is satisfiable, we extract concrete input assignments from the generated model and use them as guidance for subsequent test generation. Otherwise, the path is regarded as infeasible and excluded from the current generation attempt.

While symbolic execution is effective for solving numerical constraints, it becomes significantly less effective on object-related paths. Such paths often depend on semantic knowledge that cannot be easily encoded into SMT constraints. Figure 2(b) presents an example of an object-related path. In this example, reaching the uncovered branch at lines 13–15 requires simultaneously satisfying two semantic conditions: the input object mode must reference the singleton object Mode.STRICT, and the string parameter text must satisfy the predicate text.startsWith("A"). These conditions involve object identity comparison and string API semantics, which are difficult to model precisely using traditional symbolic execution alone.

To address this challenge, we employ an LLM-based path-solving strategy using a specialized component called LLM-Path-Solver. Given a object-related path, we avoid translating the path into SMT constraints. Instead, we provide the path information directly to the LLM-Path-Solver, including the source code, method signature, uncovered branch conditions, and execution path context. Based on this information, the model reasons about the program semantics and synthesizes concrete method inputs capable of driving execution toward the target branch. For the example shown in Figure 2(b), the LLM-Path-Solver infers that the branch condition at line 13 can only be satisfied when mode equals Mode.STRICT and the input string begins with the character "A". Accordingly, it may generate an input such as classify("Apple", Mode.STRICT), which enables execution to enter the uncovered branch and cover line 14.

Since LLM-generated inputs may still contain reasoning mistakes or semantic hallucinations, we further introduce a secondary validation stage using another model named LLM-Verifier. The verifier symbolically traces the target method using the generated input and checks whether the execution indeed follows the intended path. If the verification fails, the rejection reason, together with the invalid input, is fed back to the LLM-Path-Solver for iterative refinement. This feedback-driven process continues until a valid input is generated or a predefined retry limit is reached. Once a valid input is confirmed, the generated concrete values are appended to the downstream test-generation prompt as path guidance examples.

After symbolic execution, the candidate paths and their corresponding input references are formatted into prompts for test generation. To enrich the context provided to the LLM, we augment these prompts with explicit type information by annotating variables directly in the code as comments. For example, an initialization such as Date date = new Date() is transformed into Date date = new Date() // ‘‘date’’ is a variable of type ‘‘Date’’. We similarly handle container types (e.g., arrays, ArrayList, Set, and Map) by appending element-type annotations, such as // ‘‘list’’ is a List of type ‘‘Integer’’ for List<Integer> list = new List<>().

Figure 1 (Prompt Building part) illustrates the template of the test-generation prompt with integrated path-resolving information. The path information combines three types of code: (1) variable definition or object creation code, augmented with variable descriptions; (2) normal operation code, such as calculations and method calls; and (3) conditional or loop code, represented by True/False conditions indicating execution requirements. Finally, we also append an input guide derived from Z3 SMT solver or LLMs in the prompt.

The prompt is then fed to the LLM to generate test cases. If a generated test fails (e.g., due to compilation or runtime errors), we provide the error messages along with the failed test file back to the LLM for iterative refinement. Only tests that successfully pass are retained and appended to the existing test suite. The augmented test suite is then re-evaluated for coverage, and the process repeats until the target coverage is achieved or a predefined limit is reached.

To ensure a fair comparison and following the state-of-the-art setting, we use the same dataset as Gu et al. (2026), which includes 14 real-world subjects from Defects4J Just et al. (2014). The number of classes ranges from 2 to 30, and the number of methods under test ranges from 31 to 586. Table 3 presents the selected subjects. The column Project denotes the project name together with its Defects4J version identifier. In total, we evaluate 130 classes containing 2,971 methods under test. Across all projects, object-related paths overwhelmingly dominate execution, accounting for 80.96% of all paths on average, compared to only 19.04% for pure numerical paths. This trend is consistent across nearly all subjects, indicating that real-world Java programs are largely driven by object interactions rather than purely numerical computations.

For a controlled and comparable evaluation, we discard the original test suites in each project and generate tests from scratch for all target classes, which helps eliminate any potential bias introduced by existing tests and ensures that all approaches are evaluated under the same conditions.

To evaluate NeuroTestGen, we compare it against the state-of-the-art LLM-based test generation technique, Panta Gu et al. (2026), which combines static control-flow analysis and dynamic coverage feedback to iteratively guide LLMs toward generating tests for uncovered execution paths.

For the experimental LLM configuration, we follow Panta Gu et al. (2026) and adopt the same evaluation protocol, benchmark setup, and language models to ensure a fair and consistent comparison. Specifically, we experiment with the same four representative large language models used in Gu et al. (2026), including Meta’s Llama 3.3 70B¹¹ 1 https://www.llama.com/docs/model-cards-and-prompt-formats/llama3_3/, OpenAI’s GPT-4o Mini²² 2 https://developers.openai.com/api/docs/models/gpt-4o-mini, and Anthropic’s Claude 3.5 Haiku³³ 3 https://www.anthropic.com/news/3-5-models-and-computer-use. In addition, we include a strong state-of-the-art coding-oriented model, Claude Sonnet 4.6⁴⁴ 4 https://www.anthropic.com/news/claude-sonnet-4-6, to better contextualize the performance of our approach.

All evaluated LLMs support a context window of up to 128K tokens, ensuring sufficient capacity for handling large code contexts and specifications. To maintain consistency and eliminate confounding factors, we fix the decoding parameters across all models: the maximum number of generated tokens is set to 4096, and the temperature is set to 0.2. This relatively low temperature encourages stable and near-deterministic outputs while still allowing limited variability.

We adopt widely used quality metrics from the test generation literature Gu et al. (2026); Chen et al. (2024); Schäfer et al. (2023), including Line Coverage, Branch Coverage, Pass Rate, and Cost.

Line Coverage. measures the proportion of executable source code lines that are exercised by the generated test suite. It is computed as the number of lines executed at least once divided by the total number of executable lines in the target class. Branch Coverage. measures the proportion of control-flow branches (e.g., true/false outcomes of conditional statements such as if, switch, and loop conditions) that are executed by the test suite. It is calculated as the number of covered branches divided by the total number of branches in the class. Pass Rate. The pass rate is defined as the percentage of generated tests that execute successfully when incorporated into the test suite. A test is considered passing if it compiles successfully and runs without failures or runtime exceptions. Cost. Since different LLMs incur varying usage expenses, we report the corresponding monetary cost of NeuroTestGen with each model.

As our evaluation is conducted at the class level rather than the method level, we compute line and branch coverage for each class individually and report the average coverage across all target classes within each project.

Panta Gu et al. (2026) reported its best performance using Claude-3.5-Haiku; therefore, to ensure a fair comparison with Panta, we adopt Claude-3.5-Haiku as one of our primary evaluation models and use the original results reported in their paper. In addition, we include the latest state-of-the-art coding-oriented model, Claude Sonnet 4.6, to further evaluate the effectiveness of NeuroTestGen under a stronger LLM setting.

Our main results are presented in Table 1, which compares Panta Gu et al. (2026) and NeuroTestGen using both Claude-3.5-Haiku and Claude Sonnet 4.6. Overall, NeuroTestGen consistently outperforms Panta across most projects and metrics, achieving higher average line coverage, branch coverage, and pass rates under both LLM settings. These results demonstrate the effectiveness of combining symbolic execution with LLM-guided test synthesis. For line coverage, NeuroTestGen improves the average coverage from 70.88% to 75.87% with Claude 3.5 and from 91.68% to 92.91% with Claude 4.6, with notable gains on projects such as Csv, Jsoup, and JXPath. For branch coverage, NeuroTestGen increases the average coverage from 65.15% to 70.87% using Claude 3.5 and from 87.24% to 88.89% using Claude 4.6, demonstrating a stronger ability to cover difficult execution paths. NeuroTestGen also maintains high test validity, slightly improving the average pass rate from 65.92% to 66.34% with Claude 3.5 and from 96.81% to 96.88% with Claude 4.6.

NeuroTestGen achieves larger improvements over Panta when using earlier-generation LLMs such as Claude 3.5 compared to stronger models such as Claude 4.6. This suggests that the symbolic reasoning and constraint-solving capabilities introduced by NeuroTestGen can effectively compensate for the weaker reasoning abilities of smaller or less advanced LLMs.

We also examine the performance of NeuroTestGen across different LLMs to evaluate its effectiveness and generalizability under models with varying capabilities and costs.

Table 2 presents a detailed comparison of NeuroTestGen when instantiated with different LLMs, namely Llama 3.3 70B, GPT-4o Mini, Claude 3.5 Haiku, and Claude Sonnet 4.6. Overall, the performance varies significantly across models, highlighting the strong impact of the underlying LLM on test generation effectiveness.

Among the evaluated models, Claude Sonnet 4.6 achieves the highest average line coverage (92.91%), branch coverage (88.89%), and pass rate (96.88%), demonstrating the benefit of stronger code reasoning and generation capabilities. Claude 3.5 Haiku also performs competitively, reaching 75.87% line coverage and 70.87% branch coverage, indicating that NeuroTestGen can effectively leverage mid-sized LLMs to achieve strong testing performance. In contrast, Llama 3.3 and GPT-4o Mini exhibit noticeably lower performance, particularly in pass rate and branch coverage, suggesting that weaker LLMs struggle more with generating valid tests and satisfying complex execution constraints even with symbolic guidance. Nevertheless, NeuroTestGen still enables these smaller models to achieve reasonable coverage across multiple projects, highlighting the robustness of the hybrid symbolic execution and LLM-guided framework.

Figure 4 compares the generation cost of different LLMs. Llama 3.3 70B incurs the lowest cost ($116.23), followed by GPT-4o-Mini ($183.50) and Claude 3.5 Haiku ($428.41), while Claude Sonnet 4.6 is the most expensive at $904.28. Although Claude Sonnet 4.6 achieves the best coverage and pass rates, these gains come at a significant cost, requiring approximately 7.8$\times$ higher cost than Llama 3.3 70B and 4.9$\times$ higher cost than GPT-4o-Mini. In contrast, Claude 3.5 Haiku offers a more favorable balance between performance and cost, achieving competitive test generation quality at substantially lower expense.

As discussed in Section 2, execution paths include both pure numerical and object-related paths. While pure numerical paths can be effectively handled by symbolic execution, object-related paths are more challenging and require LLM-based support. In this section, we compare NeuroTestGen with symbolic execution only against the full NeuroTestGen framework to evaluate the contribution of the LLM component in path solving.

Table 3 presents the ablation study comparing the symbolic-only variant of NeuroTestGen with the full framework under Claude 3.5 Haiku and Claude Sonnet 4.6. Overall, integrating LLM-guided test synthesis consistently improves both line and branch coverage over symbolic execution alone. With Claude 3.5, the full framework improves average line coverage from 73.45% to 75.87% and branch coverage from 68.53% to 70.87%. Similarly, under Claude Sonnet 4.6, the full framework increases average line coverage from 92.35% to 92.91% and branch coverage from 88.15% to 88.89%. The relatively small improvement of the full NeuroTestGen framework over the symbolic-only variant is partly due to the strong inherent capabilities of modern LLMs. Even without explicitly solving object-related constraints, LLMs can often infer reasonable object constructions, API sequences, and input values from learned programming patterns, allowing the symbolic-only variant to achieve relatively strong performance.

Nevertheless, the full NeuroTestGen framework consistently performs better, especially on projects with complex object-oriented logic and API interactions. These results highlight the complementary strengths of symbolic execution and LLM-based synthesis: symbolic execution provides precise path reasoning, while LLMs contribute semantic understanding and flexible test generation.

Automated unit test generation using LLMs has been widely researched in recent years. AthenaTest Tufano et al. (2020) used transformer models trained on the focal method context to generate unit tests, and ATLAS Watson et al. (2020) proposed neural methods that predict meaningful assertions to strengthen fault detection. Later, TOGA Dinella et al. (2022) shows that machine learning models can learn assertion patterns from existing tests and documentation and successfully generate useful oracles. CodaMosa Lemieux et al. (2023) invokes a model to escape coverage plateaus in search-based generation, while Cedar Nashid et al. (2023) retrieves effective demonstrations to stabilize few-shot prompting for assertion-related tasks. Shin et al. Shin et al. (2024) further study retrieval augmented test generation and show that providing LLMs with external domain knowledge can improve unit test generation for library APIs. ChatUniTest Chen et al. (2024) introduces an iterative validation and repair mechanism to fix failed tests, and MuTAP Dakhel et al. (2024) incorporates feedback from mutation tests to improve the effectiveness of test cases. More recently, Steenhoek et. al. Steenhoek et al. (2025) proposed a method that used reinforcement learning from automatic quality metrics that helps to reduce test smells. Panta Gu et al. (2026) used a hybrid approach that increased line and branch coverage by using static program analysis to reveal uncovered paths, which gives LLM more information, and ASTER Pan et al. (2025) introduced a generic, multi-language unit test generation pipeline that combines program analysis with environment mocking to handle real-world software systems. Together, these studies indicate a switch from one-shot prompting toward iterative and feedback-guided test generation that improves both coverage and test effectiveness.

Symbolic execution is a white box program analysis technique that runs a program using symbolic values in place of concrete inputs and accumulates a path condition that captures the constraints required to follow each explored execution path King (1976). By solving these constraints, it can get concrete inputs that lead the program execution toward specific branches and behaviors, making it helpful for systematic test case generation King (1976). Early work King (1976) established the core idea of symbolic execution for program testing, while concolic execution, such as CUTE Sen et al. (2005), combined concrete runs with symbolic reasoning to iteratively negate branch predicates and generate new tests with higher path diversity. Scalable engines such as KLEE Cadar et al. (2008) further demonstrated that symbolic execution can automatically generate high-coverage tests for complex systems, but also highlighted challenges, including path explosion and constraint-solver bottlenecks.

Recent research revisits these challenges by integrating LLMs with symbolic and concolic execution to improve test generation Wu et al. (2026a); Li et al. (2025); Wang et al. (2024b); Ryan et al. (2024); Tu et al. (2025); Wang et al. (2025). PALM intentionally avoids SMT-based constraint solving by translating paths into executable variants interpretable by LLMs Wu et al. (2026a). Wang et al. Wang et al. (2024b) proposed LLM-Sym to translate complex Python path constraints into Z3 code. SymPrompt Ryan et al. (2024) studies coverage-guided regression test generation and proposes a multi-stage prompting strategy that aligns generation with execution paths while feeding type and dependency contexts, thereby helping the model produce executable tests and escape coverage plateaus in practice. Cottontail Tu et al. (2025) employs LLM-driven solving into concolic execution to generate highly structured inputs for programs to avoid wasted testing efforts.

Different from prior studies, our approach combines precise symbolic reasoning with LLM-based semantic understanding in a unified path-solving framework. By adaptively applying SMT-based symbolic execution to numerically constrained paths and verifier-guided LLM reasoning to semantically complex paths, our method improves both the accuracy and effectiveness of solving uncovered execution paths in real-world test generation scenarios.