PaperlayerView exact revision on arXiv

Source-linked AI summary

Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models

Daniel Koh, Yannic Noller, Corina S. Pasareanu, Adrians Skapars, Youcheng Sun

arXiv:2506.08171v2cs.SEcs.AI

TL;DR

LLMs’ ability to perform complex symbolic reasoning over code remains underexplored, while worst-case constraint analysis can identify inputs associated with software bottlenecks or denial-of-service vulnerabilities. WARP uses program analysis to obtain constraints at smaller input sizes and LLMs to generalise them; its results report substantial gains under WARP and strong performance from WARP-1.0-3B.

  • Problem

    LLMs’ ability to perform complex symbolic reasoning over code remains underexplored, although worst-case constraints can identify inputs exposing software bottlenecks or denial-of-service vulnerabilities.

    Source: §1 · p. 1

  • Method

    WARP obtains worst-case constraints for smaller inputs using program analysis, then uses incremental LLM reasoning and solver-guided learning to generalise constraints to larger inputs.

    Source: §1 · p. 2, §4.1 · p. 7

  • Results

    GPT-5 achieves 13% accuracy when prompted directly and 95.47% under WARP; WARP-1.0-3B is reported to exceed previous-generation state-of-the-art models like GPT-4o.

    Source: §5.2 · p. 11, §6 · p. 18

  • Takeaways & Limitations

    The authors describe RLSGF as a lightweight and scalable path toward more capable neurosymbolic systems.

    Source: §6 · p. 18

    The benchmark covers 20 Java programs and input sizes up to n=30, not the full spectrum of real-world software or larger-scale symbolic reasoning tasks.

    Source: §5.5 · p. 18

Abstract

from arXiv · show

Large language models (LLMs) have demonstrated strong performance on coding tasks such as generation, completion and repair, but their ability to handle complex symbolic reasoning over code still remains underexplored. We introduce the task of worst-case symbolic constraints analysis, which requires inferring the symbolic constraints that characterise worst-case program executions; these constraints can be solved to obtain inputs that expose performance bottlenecks or denial-of-service vulnerabilities in software systems. We show that even state-of-the-art LLMs (e.g., GPT-5) struggle when applied directly on this task. To address this challenge, we propose WARP, an innovative neurosymbolic approach that computes worst-case constraints on smaller concrete input sizes using existing program analysis tools, and then leverages LLMs to generalise these constraints to larger input sizes. Concretely, WARP comprises: (1) an incremental strategy for LLM-based worst-case reasoning, (2) a solver-aligned neurosymbolic framework that integrates reinforcement learning with SMT (Satisfiability Modulo Theories) solving, and (3) a curated dataset of symbolic constraints. Experimental results show that WARP consistently improves performance on worst-case constraint reasoning. Leveraging the curated constraint dataset, we use reinforcement learning to fine-tune a model, WARP-1.0-3B, which significantly outperforms size-matched and even larger baselines. These results demonstrate that incremental constraint reasoning enhances LLMs' ability to handle symbolic reasoning and highlight the potential for deeper integration between neural learning and formal methods in rigorous program analysis.

1 Introduction

The paper addresses the challenge of applying LLMs to rigorous worst-case complexity reasoning, where symbolic execution faces scalability limits. WARP combines small-input program analysis, solver-guided learning, and curated constraints to support generalisation to larger inputs.

Incremental Worst-Case Constraint Reasoning

  • WARP first obtains solver-checked constraints for small inputs, then prompts or trains LLMs to generalise their patterns to larger inputs.This reframes the task as semantics-preserving pattern induction, reducing the effective search space and mitigating path explosion.Source: §1 · p. 2, Figure 1 · p. 2

Neurosymbolic Approach for Worst-Case Complexity Analysis

  • Reinforcement Learning from Solver-Guided Feedback fine-tunes LLMs with SMT-solver feedback to generate semantically valid, generalisable constraints.WARP trains on tractable small-scale constraints rather than exhaustively exploring exponentially growing search spaces.Source: §1 · pp. 2–3

Fine-Tuning and Benchmarking Datasets

  • The paper introduces a fine-tuning dataset of synthetic programs and worst-case path constraints, alongside a benchmark for semantic fidelity, formal correctness, and generalisation.The benchmark is presented as a reproducible testbed for future work on LLM-driven worst-case constraint synthesis.Source: §1 · p. 3

A Trained Model for Worst-Case Symbolic Constraint Reasoning

  • WARP-1.0-3B is reported to generalise across input sizes and outperform baselines on asymptotic prediction tasks.The model is fine-tuned using the WARP framework.Source: §1 · p. 3

2 Related Work

Prior symbolic program analysis can explore execution paths but faces exponential path growth, while LLMs can assist with program analysis without formal correctness guarantees. Neurosymbolic work combines learned guidance with symbolic tools, including solver feedback, but reinforcement-learning approaches can be computationally expensive.

2.1 Symbolic Program Analysis

  • Worst-case analysis compounds symbolic execution’s path-explosion problem, and existing search-pruning approaches remain limited by exponential growth and solver dependence.WISE learns simple generator policies from small inputs, while SPF-WCA tracks branch history for more complex strategies.Source: §2.1 · p. 3

2.2 LLMs for Program Analysis

  • LLMs have been explored for program properties and vulnerability repair, but their outputs lack formal correctness guarantees without external checking.Prior work studied loop invariants and verifier-validated repair patches [23].Source: §2.2 · pp. 3–4

2.3 Neurosymbolic Reasoning

  • Neurosymbolic systems use learned guidance with formal tools; prior reinforcement-learning proof approaches can be computationally expensive because they attempt many proof paths.LeanDojo [25] combines LLMs with retrieval and a proof assistant, while DeepSeek Prover [24] uses proof-assistant feedback during training; this paper applies solver verification to worst-case path constraints.Source: §2.3 · p. 4

3 Problem Formulation

Worst-case symbolic analysis seeks input conditions that maximize software resource use, but symbolic execution becomes difficult as path counts grow. The section motivates incrementally generalizing solver-derived constraints to larger inputs instead of deriving them from scratch.

3 Problem Formulation

  • Worst-case analysis seeks input conditions producing maximal resource consumption, while symbolic execution faces scalability limits from exponential path growth.The analysis considers worst-case constraints for a given input size n.Source: §3 · p. 4

3.1 Motivating Example

  • At input size n=12, symbolic execution becomes increasingly intensive, quickly exceeding thousands of logical clauses; this represents a 2^12 = 4096-fold increase in execution paths compared to input n=3.Source: §3.1 · p. 5
  • For QuickSort at n=30, exhaustive analysis entails exploring 2^30 ≈ 10^9 paths, making CPU time and memory use impractical.The example illustrates why exhaustive symbolic methods do not scale to larger inputs.Source: §3.1 · p. 5

3.2 Vanilla Prompting

  • The vanilla-prompting evaluation sampled input sizes 2, 4, 8, 16, and 30 across all 20 benchmark programs.GPT-5 was prompted to produce worst-case path constraints for each sampled size.Source: §3.2 · p. 5
  • GPT-5 achieved 13/100 overall accuracy when prompted directly, with most outputs failing semantic equivalence checks despite being syntactically well formed.The evaluation counted a constraint as correct only when syntactically valid and semantically equivalent to the ground truth.Source: §3.2 · p. 6, Table 1 · p. 6

3.3 Augmenting Symbolic Execution with LLMs

  • WARP uses SPF-WCA constraints at small input sizes to teach LLMs patterns they can extrapolate to larger inputs.The approach reframes worst-case analysis as pattern induction, reducing exponential search and mitigating path explosion.Source: §3.3 · p. 7
  • Incremental reasoning formalizes the task as inferring a larger-size constraint semantically equivalent to the solver-derived constraint from smaller sizes.The formulation uses a sequence of constraints for n1 < n2 < ... < nk and targets n much larger than nk.Source: §3.3 · p. 7

4 Methodology

WARP combines solver-derived constraints at tractable sizes with LLM generalization, a curated benchmark, and solver-guided reinforcement learning. Its evaluation treats correctness as syntactic validity plus solver-verified semantic equivalence.

4 Methodology

  • WARP combines symbolic program analysis, solver-guided reinforcement learning, and benchmarking to improve LLM worst-case constraint reasoning.The framework uses an incremental strategy and reports that it improves task performance.Source: §4 · p. 7

4.1 Incremental Worst-Case Path Constraints Curation

  • SPF-WCA generates worst-case path constraints at multiple tractable input sizes, forming sequences that show how constraint structure changes as n grows.Its default cost model assigns greater cost to paths visiting more branches with symbolic conditions.Source: §4.1 · p. 7

4.2 Dataset Creation and Benchmarking

  • The fine-tuning corpus contains 23,600 instances, including 17,700 training and 5,900 test examples drawn from synthetic programs and real-world applications.The final benchmark contains 671 instances and restricts n to at most 30 for Z3 verification; a separate test set has over 600 instances from 20 Java programs.Source: §4.2 · pp. 8–9
  • Benchmark instances vary the extrapolation jump from available examples to a held-out target, with small, medium, and large tiers for jump size.Larger jumps require more extrapolation; prompt-size limits preserve output capacity, while examples exceeding the threshold may be excluded.Source: §4.2 · pp. 8–9

4.3 Reinforcement Learning from Solver-Guided Feedback

  • WARP-1.0-3B is a 3B-parameter model fine-tuned to generate SMT constraints for worst-case execution, built upon Qwen2.5-3B [19] and adapted with a task-specific prompt for SMT constraint generation.The model is required to reason through the problem before providing its final answer.Source: §4.3 · p. 9
  • The reward combines a larger semantic component, based on Z3 equivalence to ground truth, with a smaller bonus for exact output-template compliance.The reasoning block is left unscored, prioritizing verifiable constraint generalization over natural-language reasoning quality.Source: §4.3 · p. 10

4.4 Evaluation and Performance Metrics

  • Accuracy counts tasks whose generated constraints are both syntactically valid and semantically correct according to Z3 verification.This metric avoids surrogate measures such as BLEU or perplexity, which do not guarantee formal correctness.Source: §4.4 · p. 11

5 Experiments

The experiments ask whether incremental reasoning improves on vanilla prompting, reflects symbolic reasoning rather than syntax adaptation, and generalizes across model scales and program settings.

5 Experiments

  • The experiments examine whether incremental constraint reasoning outperforms vanilla prompting when extrapolating from smaller to larger inputs.Source: §5 · p. 11
  • A research question tests whether WARP's gains reflect symbolic reasoning rather than domain-specific adaptation to SMT-LIB syntax.Source: §5 · p. 11
  • The evaluation also asks how performance varies across model scales, extrapolation regimes, and representative program families, including practical accuracy, scalability, and cost trade-offs.Source: §5 · p. 11

5.1 Evaluation Setup

The evaluation uses a uniform prompt to elicit complete SMT constraints and compares WARP-1.0-3B with open-source and proprietary baselines.

5.1 Evaluation Setup

  • All models receive a uniform instruction to provide reasoning and a canonical SMT assertion without commentary or truncation.Evaluations are zero-shot and impose no output-length limit.Source: §5.1 · p. 11
  • WARP-1.0-3B is benchmarked against nine open-source checkpoints ranging from 3B to 32B parameters and several contemporaneous OpenAI models.Source: §5.1 · p. 11
  • The baselines were selected to span a representative range of model scales within the available computational budget.Source: §5.1 · p. 11

5.2 Overall Results

Incremental worst-case constraint reasoning substantially improves LLM accuracy over direct prompting. WARP-1.0-3B generalises strongly for its size, while GPT-5 reaches the highest reported accuracy when given the incremental strategy.

5.2 Overall Results

  • 95.47% accuracy for GPT-5 under WARP contrasts with 13% under direct prompting.The reported results identify incremental reasoning as a consistent advantage over vanilla prompting.Source: §5.2 · pp. 11–12
  • 41.08% average zero-shot accuracy for WARP-1.0-3B exceeds its Qwen2.5-3B-Instruct baseline's 9.79% and several larger models.The result is more than a fourfold baseline improvement; Table 2 covers models evaluated under the incremental approach.Source: §5.2 · pp. 11–12, Table 2 · p. 12
  • WARP-1.0-3B outperforms its parameter-size peers and matches or surpasses several 14B models; its deviation from parameter-only scaling highlights the impact of integrating formal SMT validation through RLSGF.Source: §5.2 · p. 13
  • Across models, the incremental strategy consistently outperforms vanilla prompting on worst-case constraint reasoning.The section reports this pattern alongside the model-specific accuracy comparisons.Source: §5.2 · pp. 11, 13

5.3 Disentangling Symbolic Reasoning from Syntax Adaptation

The analysis separates solver-equivalent constraints from syntax and formatting failures, then uses aggregate error categories and case studies to assess whether WARP-1.0-3B generalises logical patterns. The examples show both genuine logical improvement and evaluation fragility caused by output formatting.

5.3.1 Aggregated Results.

  • Syntax errors fall from 83% for Qwen2.5-3B-Instruct to 14% for WARP-1.0-3B, but WARP-1.0-3B also has 21% formatting errors.Because the categories are dependent, some outputs never reach semantic evaluation, limiting what aggregate counts reveal about reasoning.Source: §5.3.1 · p. 14, Table 3 · p. 14

5.3.2 Case Studies.

  • For N=28, WARP-1.0-3B produces a solver-equivalent decreasing-chain constraint, while the baseline reverses the intended comparison and generalises an increasing pattern.The WARP constraint preserves both weak and strict inequalities across adjacent indices.Source: §5.3.2 · pp. 14–15
  • A WARP-1.0-3B response can contain solver-equivalent constraints yet fail evaluation because it omits the required answer delimiters.The paper links formatting fragility to the base Qwen2.5-3B architecture's lack of supervised instruction tuning.Source: §5.3.2 · pp. 15–16
  • Strict formatting and extraction rules can cause some solver-equivalent outputs to be categorised as errors.The conclusion states that evaluation remains sensitive to categorisation and protocol adherence.Source: §5.3.2 · p. 16

5.3 Disentangling Symbolic Reasoning from Syntax Adaptation

  • WARP-1.0-3B raises solver-equivalent outputs beyond syntax adaptation alone, and case studies show it correcting logically invalid baseline constraints.The categories distinguish solver-equivalent outputs from syntactically valid but incorrect constraints, parse failures, and formatting failures.Source: §5.3 · pp. 13–14, §5.3.2 · p. 16

5.4 Robustness Across Scales, Regimes and Program Families

Across scales, extrapolation regimes, and program families, WARP disproportionately lifts smaller models, while accuracy remains sensitive to jump size and program structure. Regular patterns are broadly solved, but irregular graph workloads remain difficult.

5.4.1 Across Model Scale.

  • WARP disproportionately lifts smaller models, while accuracy increases with parameter count and failure modes shift from syntax errors toward semantic errors at greater capability.Mid-scale models also retain non-semantic failures.Source: §5.4.1 · p. 16

5.4.2 Across Extrapolation Regimes.

  • Accuracy degrades gently from small to medium jumps, then drops on the large tier for most models; only the most capable sustain high accuracy.Table 4 reports tier-wise correct counts for representative models, aggregated over three trials.Source: §5.4.2 · pp. 16–17, Table 4 · p. 17

5.4.3 Across Program Families.

  • Dijkstra is hardest at 3.57% overall micro-accuracy, while TowerOfHanoi and MazeSolver reach 88.99% and 85.92% overall, respectively.BinarySearch reaches 8.75% overall, with local models at 0.60%; best single-model accuracy ranges from 50.00% on Dijkstra to 100% on several regular families.Source: §5.4.3 · p. 17

5.4 Robustness Across Scales, Regimes and Program Families

  • The evaluation finds cross-family generalisation alongside practical trade-offs in token, verification, and compute limits.Irregular graph workloads are hardest, whereas regular patterns are broadly solved.Source: §5.4.3 · p. 17

5.5 Threats to Validity

The evaluation has threats involving automated equivalence checks, binary accuracy, benchmark scope, and model length limits. These define the boundaries of the current evaluation rather than undermining the paper’s contributions.

Internal Validity

  • Z3 equivalence checking and formatting or parsing failures can prevent valid constraints from being assessed, while a uniform prompt may bias comparisons toward instruction-tuned models.Such failures may underestimate reasoning ability.Source: §5.5 · p. 17

Construct Validity

  • Binary accuracy may mask partial progress when outputs capture much of the intended structure but deviate slightly.The authors include case studies to expose under- and over-estimations, while noting that finer-grained metrics could add insight.Source: §5.5 · p. 17

External Validity

  • The benchmark covers 20 Java programs and input sizes up to n=30, not the full spectrum of software or larger symbolic-reasoning tasks.Deeper recursion and more complex data structures are particular scope boundaries.Source: §5.5 · p. 18

Token Length Limits

  • Maximum context and generation lengths restrict prompt size and output completeness, particularly for larger n.The paper identifies this as a scalability challenge for autoregressive LLMs in symbolic constraint reasoning.Source: §5.5 · p. 18

Threats to Validity

  • These threats define the current evaluation’s boundaries; future work will extend fine-tuning to larger models and explore broader program domains and alternative generation and evaluation strategies.The authors state that the threats do not undermine the main contributions.Source: §5.5 · p. 18

6 Conclusion

The paper presents a neurosymbolic approach for computing and generalising worst-case symbolic constraints for Java programs. WARP-1.0-3B exceeds previous generation state-of-the-art models such as GPT-4o, while the authors frame its results as complementary to strong test-time reasoning models.

Conclusion

  • WARP-1.0-3B exceeds previous generation state-of-the-art models such as GPT-4o on the benchmark.The paper also reports remarkable results from the latest OpenAI thinking-series models.Source: §6 · p. 18
  • The paper’s neurosymbolic approach computes and generalises worst-case symbolic constraints for Java programs.Source: §6 · p. 18
  • The authors conclude that reinforcement learning equips compact WARP-1.0-3B with strong symbolic generalisation, offering a lightweight and scalable path toward neurosymbolic systems.They position this result as complementing the momentum behind scaling test-time reasoning.Source: §6 · p. 18
Loading 2506.08171v2…