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

What it claims

NEUROTESTGEN reaches 92.91% line coverage and 88.89% branch coverage on Defects4J when paired with Claude Sonnet 4.6, its best configuration, while beating the prior state-of-the-art (Panta) across all four LLMs tested. The summary names the hybrid approach but omits both the baseline it beats and these numbers.

How it works

The key mechanism the summary glosses is that uncovered paths are split into two categories and routed differently:

• Pure numerical paths (branch predicates over primitive numerics only — arithmetic, modulo, comparison, bitwise): solved directly by Z3. The executor walks the path, negates predicates on false branches, encodes numeric expressions as SMT formulas, and extracts concrete inputs from a satisfying model. Unsatisfiable → path marked infeasible and dropped.
• Object-related paths (object identity, method/API calls, string semantics, heap): bypass SMT entirely. An LLM-Path-Solver infers concrete inputs from source, signature, and path context; a second LLM-Verifier symbolically traces the method with those inputs to confirm they follow the intended path, feeding rejection reasons back for retry.

Both feed a prompt-building stage that annotates variables with inline type comments (e.g. Date date = new Date() // "date" is a variable of type "Date") before test synthesis, then iterates on compile/runtime errors.

flowchart TD
  P[Uncovered path] --> C{Pure numerical<br/>or object-related?}
  C -->|numerical| Z[Z3 SMT solver]
  C -->|object| S[LLM-Path-Solver]
  S --> V[LLM-Verifier]
  V -->|reject| S
  Z --> B[Prompt build + type annotations]
  V -->|valid input| B
  B --> G[LLM test synthesis]
  G -->|compile/runtime error| B
  G --> OK[Retained test]

Evidence

Dataset: same 14 Defects4J subjects as Panta — 130 classes, 2,971 methods under test, classes ranging 2–30, methods 31–586. A notable finding for anyone weighing the symbolic half: object-related paths dominate at 80.96% of all paths on average vs only 19.04% pure numerical, meaning most of the coverage work falls to the LLM-Path-Solver rather than Z3. Original test suites were discarded and tests generated from scratch for fair comparison.

Limits

• Loops are skipped during symbolic execution to avoid unrolling/invariant cost — a stated gap that will miss loop-dependent branches.
• Z3 handles only the ~19% numerical minority; the majority object-related path handling rests on LLM inference plus verification, which the authors acknowledge can hallucinate.
• This is a preprint (arXiv 2609.30178v1, dated Sep 2026). The fetched text cuts off mid-sentence in Section 3.2, so per-model coverage breakdowns, ablations, validity rates, and token-cost comparisons are not visible here — check the paper before assuming the headline numbers hold across the cheaper LLMs.