PaperlayerView exact revision on arXiv

Source-linked AI summary

Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA

Mikoláš Janota, Jan Jakubův

arXiv:2609.16706v1cs.LO

TL;DR

Developing state-of-the-art SMT solvers with LLM agents remains an open question, especially as such agents rapidly improve at formal-methods tooling. This paper presents primo through human-supervised, literature-driven vibe-coding and parameter tuning, and reports that primo⋆ outperforms SMT-COMP 2026’s QF-LRA winner. The authors also identify correctness testing as an ongoing concern because fuzzing was initially insufficient.

  • Problem

    The paper asks whether LLM-driven agents can develop state-of-the-art SMT solvers, extending beyond their already demonstrated ability to develop formal-methods tools.

  • Method

    The authors develop primo through human-supervised, clean-room vibe-coding guided by literature, solver-engineering practice, profiling, and RamParILS parameter tuning.

  • Results

    Primo⋆ outperforms the SMT-COMP 2026 QF-LRA winner opensmt in both solved-instance count and PAR2 score.

  • Takeaways & Limitations

    The reported results provide a positive answer for LLM-agent development of state-of-the-art QF-LRA solvers and indicate similar potential for QF-UFLRA.

  • Takeaways & Limitations

    Correctness testing remains incomplete because fuzzing was insufficient in some cases, making increased test coverage future work.

Abstract

from arXiv · show

This paper presents the SMT solver primo, which is fully vibe-coded and then parameter-tuned, achieving state-of-the-art results on linear real arithmetic (QF-LRA). The performance of primo is achieved by a systematic literature survey, repeated profiling, and parameter tuning. The resulting solver outperforms the winner of the QF-LRA track of SMT-COMP~2026. This confirms that vibe-coding of automated reasoning tools will enable us to make great strides in the future.

1 Introduction

The paper asks whether LLM-driven agents can develop state-of-the-art SMT solvers, answering positively for QF-LRA with primo. It combines literature-guided, human-supervised development with solver engineering and parameter tuning, yielding strong benchmark results.

  • 1 Introduction: The study evaluates primo on the full SMT-LIB QF-LRA benchmark and the SMT-COMP 2026 QF-LRA selection, while indicating similar potential for QF-UFLRA.The paper frames this as a positive answer to whether LLM agents can develop state-of-the-art SMT solvers.
  • 1 Introduction: The paper presents primo as an entirely vibe-coded QF-LRA solver, developed by an LLM-powered agent under human supervision and a clean-room policy.The policy forbids consulting existing solver source code while allowing access to performance and aggregate statistics.
  • 1 Introduction: The development methodology combines literature-driven target selection with fuzzing, delta-debugging, profiling, SMT-LIB regression testing, and iterative human feedback.The process documents its steps in Markdown and repeatedly connects literature, implementation, and empirical evidence.
  • 1 Introduction: RamParILS tunes primo’s configuration, producing primo⋆ and a complementary primo+ configuration; tuning lifts primo from below to above opensmt and yices.RamParILS is an LLM-designed, parallelized rewrite of ParamILS.
  • 1 Introduction: Primo⋆ improves PAR2 by 28% over default primo and 13% over default opensmt at the SMT-COMP 1,200 s timeout, including held-out instances.It also solves more instances than default opensmt at a 30 s timeout, with most gains concentrated in one benchmark family.

2 Preliminaries

The paper introduces QF-LRA within the DPLL(T) framework and describes primo’s implementation and LRA theory-solver architecture. Its design combines a Dutertre–de Moura simplex variant with heuristics for phases, elimination, pivoting, representation, and slack management.

  • 2 Preliminaries: Primo uses CaDiCaL through IPASIR-UP, arbitrary-precision GMP rationals, and ANTLR, supporting QF-UF, QF-LRA, and their combination.The reported evaluation focuses mainly on QF-LRA because QF-UFLRA is currently immature.
  • 2 Preliminaries: The LRA theory solver is based on a Dutertre–de Moura simplex variant that repairs out-of-bound basic variables in a dual-simplex style.Unlike traditional simplex, it targets the decision problem and supports lower and upper variable bounds.
  • 2 Preliminaries: Additional engineering choices include cheap stack-based backtracking, δ-rationals for strict inequalities, shared slacks, and small-integer arithmetic wrappers around GMP.Equalities are desugared into paired non-strict inequalities before solving.
  • 2 Preliminaries: Sparse pivoting limits tableau fill-in by favoring short defining rows, infrequently occurring entering variables, and coefficients of +1 or −1.The sparse rule is the current default; primo falls back to Bland’s rule after a bounded number of iterations.
  • 2 Preliminaries: Model-based phase selection uses the maintained tableau assignment to prefer the Boolean phase whose bound is already satisfied, avoiding unnecessary repairs.VSIDS still determines variable order by default.
  • 2 Preliminaries: Monotone variable elimination removes variables bounded only from one side, then reconstructs model values through post-solving.The reconstruction pins remaining variables and propagates bounds across eliminated atoms.

3 Parameter Vibe-Tuning

RamParILS tunes primo through iterated local search over a reduced parameter space, extending ParamILS with parallel evaluation, persistent caching, and mechanisms for escaping stalled searches.

  • Iterated Local Search: Iterated local search explores one-parameter neighbors, accepts improvements, and perturbs configurations to escape local optima.Basic ILS evaluates neighboring configurations and randomly changes s parameters during perturbation.
  • RamParILS: RamParILS extends ParamILS with parallel configuration evaluation and persistent result caching to accelerate parameter tuning.It is a Rust reimplementation of ParamILS designed to speed tuning through parallel evaluation and cached solver runs.
  • RamParILS: RamParILS submits whole neighborhoods to workers and takes the first improving neighbor, reducing a one-hour sequential evaluation to minutes with 60 workers.The parallel strategy evaluates configurations concurrently rather than one at a time.
  • RamParILS: Persistent SQLite caching avoids repeated solver calls for revisited configuration-instance pairs, including expensive timed-out instances.The cache survives across tuning runs and is keyed by both configuration and instance.
  • RamParILS: RamParILS escapes frozen searches by accepting slightly worse local optima and restarting from the best configuration after repeated rejections.These mechanisms supplement ParamILS’s random restarts when the search stops improving.
  • Parameter space: The tuning study reduced primo’s roughly 90 options to 11 parameters and 8,640 configurations, using dependencies detected from trial logs and cached results.The default configuration has 16 neighbors, and the tuned benchmark uses a representative subset of 473 instances.

4 Experiments: Strategy Tuning and Analysis

Parameter tuning produced two specialized primo configurations and raised primo⋆ above the default reference solvers on full QF-LRA and SMT-COMP evaluations, while revealing complementary strengths and benchmark-specific gains.

  • Tuning runs: RamParILS tuning selected primo⋆ as the overall best configuration and primo+ as the most complementary, enabling techniques disabled in primo’s default configuration.primo⋆ enables model-based phase selection and monotone variable elimination; primo+ adds mixed dispatch and widened row-propagation cost caps.
  • Full QF-LRA evaluation: 1,599 instances were solved by primo⋆ on the full 1,753-instance SMT-LIB QF-LRA benchmark, outperforming default primo by 63, default opensmt by 21, and yices by 36.primo⋆ also achieved the best PAR2 score, although opensmt retained a 23-instance lead on unsatisfiable instances.
  • Full QF-LRA evaluation: 62 of primo⋆’s 77 additional solved instances came from the LassoRanker family, where monotone elimination simplifies large disjunctive Boolean structure.The tuned model-based phase selection also causes primo⋆ to lose 14 satisfiable instances, because it can miss models outside the selected candidate polarity.
  • Full QF-LRA evaluation: The complementary primo+ configuration solved 23 instances missed by primo⋆ but finished 37 instances behind it overall.Combining primo⋆ with default opensmt solved 1,639 instances, while combining all five configurations reached 1,671.
  • SMT-COMP competition experiments: The 1,200 s evaluation split 519 SMT-COMP instances into 194 tuning instances and 325 held-out test instances, with primo⋆ gaining four of its five remaining instances in the held-out half.This pattern argues against overfitting the tuning subset within the reported experiment.
  • SMT-COMP competition experiments: 28% lower PAR2 than default primo and 13% lower than default opensmt were achieved by primo⋆ at the 1,200 s SMT-COMP cutoff.Across the 483 instances solved by all five configurations, primo⋆ used 46.6% less total time than default primo: 7,284 s versus 13,648 s.

5 Conclusions and Future Work

The paper concludes that a fully vibe-coded and tuned solver can outperform established QF-LRA systems, while identifying training-data provenance and test coverage as important validity and correctness boundaries.

  • Conclusions: primo⋆ outperforms the SMT-COMP 2026 QF-LRA winner opensmt in both solved-instance count and PAR2 score.The comparison is reported on both the full SMT-LIB QF-LRA benchmark and the SMT-COMP 2026 QF-LRA selection at 30 s and 1,200 s cutoffs.
  • Validity and limitations: The authors identify uncontrolled LLM training data as an inherent threat to validity despite anti-plagiarism checks finding no overlaps beyond boilerplate enums.The work’s motivation is to assess how well LLM-guided agents integrate existing literature into code.
  • Correctness and future work: Fuzzing was insufficient in some cases, so hand-written fuzzers for dedicated fragments were added; increasing test coverage remains future work.These additional fuzzers exposed bugs in difficult fragments, including functions taking Boolean arguments.
  • Future work: Natural continuations include improving QF-UFLRA support and extending the solver to integer arithmetic.The current implementation already combines real arithmetic and uninterpreted functions through Nelson–Oppen closure.

A Performance Cactus Plots

The evaluations compare solver performance using cactus plots that show the percentage of instances solved over wall-clock time. Figure 4 covers QF-LRA at two time limits, while Figure 5 compares solvers on QF-UFLRA.

  • A Performance Cactus Plots: Figure 4 plots the percentage of instances solved against wall-clock time for QF-LRA evaluations.The evaluations use the full benchmark at 30 s and the SMT-COMP selection at 1,200 s.
  • A Performance Cactus Plots: Figure 5 compares primo with four other solvers on QF-UFLRA.The comparison uses a 120 s cutoff and instances not settled by every solver within 5 s.
  • A Performance Cactus Plots: The QF-UFLRA comparison concerns a different logic combination from the mainly reported QF-LRA evaluation.QF-UFLRA is described as currently immature in the implementation discussion.

B Tableau Structure

The tableau structure maintains unsorted occurrence lists for variables and back-indices from row elements to their locations. Removing an occurrence uses swap-pop and repairs the moved row’s index.

  • B Tableau Structure: Occurrence lists store rows containing each variable, while back-indices map row elements to their occurrence-list positions.For a row containing ⟨x, c, i⟩, the structure records its row index in occ[x][i].
  • B Tableau Structure: Removing an occurrence uses swap-pop: the target slot is unlinked and the last occurrence is moved into it.This avoids shifting all later entries in the unsorted occurrence vector.
  • B Tableau Structure: The moved row can be located with a binary search in the sorted row, costing O(log |row_x7|).The search identifies the surviving column position whose back-index must be updated.
  • B Tableau Structure: After swap-pop, only the surviving moved column element requires a new back-index.The removed row’s entry disappears, and the moved row entry is repaired separately.
Loading 2609.16706v1…