Boosting Skeleton-Driven SMT Solver Fuzzing by Leveraging LLM to Produce Formula Generators

• URL: http://arxiv.org/abs/2508.20340v1
• Date: Thu, 28 Aug 2025 01:21:26 GMT
• Title: Boosting Skeleton-Driven SMT Solver Fuzzing by Leveraging LLM to Produce Formula Generators
• Abstract summary: Satisfiability Modulo Theory (SMT) solvers are foundational to modern systems and programming languages research.<n>While prior testing techniques performed well on earlier solver versions, they struggle to keep pace with rapidly evolving features.<n>Recent approaches based on Large Language Models (LLMs) show promise in exploring advanced solver capabilities.
• Score: 5.527936960933817
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Satisfiability Modulo Theory (SMT) solvers are foundational to modern systems and programming languages research, providing the foundation for tasks like symbolic execution and automated verification. Because these solvers sit on the critical path, their correctness is essential, and high-quality test formulas are key to uncovering bugs. However, while prior testing techniques performed well on earlier solver versions, they struggle to keep pace with rapidly evolving features. Recent approaches based on Large Language Models (LLMs) show promise in exploring advanced solver capabilities, but two obstacles remain: nearly half of the generated formulas are syntactically invalid, and iterative interactions with the LLMs introduce substantial computational overhead. In this study, we present Chimera, a novel LLM-assisted fuzzing framework that addresses both issues by shifting from direct formula generation to the synthesis of reusable term (i.e., logical expression) generators. Particularly, Chimera uses LLMs to (1) automatically extract context-free grammars (CFGs) for SMT theories, including solver-specific extensions, from documentation, and (2) synthesize composable Boolean term generators that adhere to these grammars. During fuzzing, Chimera populates structural skeletons derived from existing formulas with the terms iteratively produced by the LLM-synthesized generators. This design ensures syntactic validity while promoting semantic diversity. Notably, Chimera requires only one-time LLM interaction investment, dramatically reducing runtime cost. We evaluated Chimera on two leading SMT solvers: Z3 and cvc5. Our experiments show that Chimera has identified 43 confirmed bugs, 40 of which have already been fixed by developers.

Related papers

• A Hybrid Nested Harness for Decoupling Structure and Parameters in LLM-Driven Optimization [6.599344783327054]
  In evolutionary algorithms powered by language models, the LLM acts as a single operator that simultaneously updates structural components and continuous parameters.<n>We formalize a hybrid nested search, in which an outer loop has the LLM propose a structural sketch, with numeric gaps, and an innernest tunes the sketch.<n>We validate our framework across three scientific domains: (i) meta-optimizers on closed-form test functions, (ii) code-based policies for systems research and social dilemmas, and (iii) approximate Bayesian inference tasks.
  arXiv  Detail & Related papers  (2026-08-08T14:35:22Z)
• A2RBench: An Automatic Paradigm for Formally Verifiable Abstract Reasoning Benchmark Generation [59.98516959731531]
  Abstract reasoning ability reflects intelligence and capacity of LLMs to extract and apply abstract rules.<n>Existing benchmarks either rely on expensive manual annotation, limiting their scale, or risk measuring memorization rather than genuine reasoning.<n>We introduce an automated pipeline named A2RBench, encompassing generation, expansion, evaluation, and analysis.
  arXiv  Detail & Related papers  (2026-05-17T06:14:20Z)
• From I/O to Code with Discovery Agent [103.88427301265669]
  We propose DIO-Agent, a discovery agent for IO2Code.<n>Our method frames IO2Code as an evolutionary search over discrete program space.<n>Extensive experiments show that DIO-Agent consistently outperforms both traditional program-by-example method and SOTA evolution-agent baselines.
  arXiv  Detail & Related papers  (2026-05-14T18:57:32Z)
• Breaking Validity-Induced Boundaries to Expand Algorithm Search Space: A Two-Stage AST-Based Operator for LLM-Driven Automated Heuristic Evolution [0.0]
  We propose a two-stage, structure-based evolutionary operator for LLM-AHD.<n>In the first stage, our approach directly performs crossover and mutation on the Abstract Syntax Trees (ASTs) of code.<n>In the second stage, the LLM is employed to repair these invalids into executable, high-quality code.
  arXiv  Detail & Related papers  (2026-04-03T07:35:43Z)
• RAVEL: Reasoning Agents for Validating and Evaluating LLM Text Synthesis [78.32151470154422]
  We introduce RAVEL, an agentic framework that enables the testers to autonomously plan and execute typical synthesis operations.<n>We present C3EBench, a benchmark comprising 1,258 samples derived from professional human writings.<n>By augmenting RAVEL with SOTA LLMs as operators, we find that such agentic text synthesis is dominated by the LLM's reasoning capability.
  arXiv  Detail & Related papers  (2026-02-28T14:47:34Z)
• Gecko: A Simulation Environment with Stateful Feedback for Refining Agent Tool Calls [56.407063247662336]
  We introduce Gecko, a comprehensive environment that simulates tool responses using a combination of rules and LLMs.<n>GATS consistently improves the tool calling performance of various LLMs including GPT-4o, GPT-5, and Gemini-3.0-pro.
  arXiv  Detail & Related papers  (2026-02-22T15:02:00Z)
• The Automated LLM Speedrunning Benchmark: Reproducing NanoGPT Improvements [87.61432174951891]
  A critical capability toward scientific progress is the ability to reproduce existing work.<n>To evaluate the ability of AI agents to reproduce results in an active research area, we introduce the Automated LLM Speedrunning Benchmark.<n>We find that recent reasoning LLMs combined with SoTA scaffolds struggle to reimplement already-known innovations in our benchmark.
  arXiv  Detail & Related papers  (2025-06-27T17:44:32Z)
• SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning [18.40402135952776]
  This paper presents SymRTLO, a novel neuron-symbolic RTL optimization framework.<n>A symbolic module is proposed for analyzing and optimizing finite state machine (FSM) logic.<n> Experiments on the RTL-Rewriter benchmark with Synopsys Design Compiler and Yosys show that SymRTLO improves power, performance, and area (PPA) by up to 43.9%, 62.5%, and 51.1%, respectively.
  arXiv  Detail & Related papers  (2025-04-14T16:15:55Z)
• D2LLM: Decomposed and Distilled Large Language Models for Semantic Search [18.63768158439252]
  We present D2LLMs-Decomposed and Distilled LLMs for semantic search. We decompose a cross-encoder into an efficient bi-encoder integrated with Pooling by Multihead Attention and an Interaction Emulation Module. Our experiments show that D2LLM surpasses five leading baselines in terms of all metrics across three tasks.
  arXiv  Detail & Related papers  (2024-06-25T04:03:04Z)
• LLMRefine: Pinpointing and Refining Large Language Models via Fine-Grained Actionable Feedback [65.84061725174269]
  Recent large language models (LLM) are leveraging human feedback to improve their generation quality. We propose LLMRefine, an inference time optimization method to refine LLM's output. We conduct experiments on three text generation tasks, including machine translation, long-form question answering (QA), and topical summarization. LLMRefine consistently outperforms all baseline approaches, achieving improvements up to 1.7 MetricX points on translation tasks, 8.1 ROUGE-L on ASQA, 2.2 ROUGE-L on topical summarization.
  arXiv  Detail & Related papers  (2023-11-15T19:52:11Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  Large Language Models (LLMs) have shown success in code analysis and synthesis. We present a combination of LLMs and static analysis to synthesize invariants, assertions, and other proof structures for a Rust-based formal verification framework called Verus. Our prototype decomposes the verification task into multiple smaller ones, iteratively queries GPT-4, and combines its output with lightweight static analysis.
  arXiv  Detail & Related papers  (2023-11-07T05:47:47Z)
• BOOST: Harnessing Black-Box Control to Boost Commonsense in LMs' Generation [60.77990074569754]
  We present a computation-efficient framework that steers a frozen Pre-Trained Language Model towards more commonsensical generation. Specifically, we first construct a reference-free evaluator that assigns a sentence with a commonsensical score. We then use the scorer as the oracle for commonsense knowledge, and extend the controllable generation method called NADO to train an auxiliary head.
  arXiv  Detail & Related papers  (2023-10-25T23:32:12Z)
• MuSR: Testing the Limits of Chain-of-thought with Multistep Soft Reasoning [63.80739044622555]
  We introduce MuSR, a dataset for evaluating language models on soft reasoning tasks specified in a natural language narrative. This dataset has two crucial features. First, it is created through a novel neurosymbolic synthetic-to-natural generation algorithm. Second, our dataset instances are free text narratives corresponding to real-world domains of reasoning.
  arXiv  Detail & Related papers  (2023-10-24T17:59:20Z)
• Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving [23.426866969743525]
  Generative large language models (LLMs) with instruct training can generate human-like responses to prompts. Despite their improved accuracy, these models are still known to produce factually incorrect or contextually inappropriate results. This limitation makes it difficult to use these models to synthesize formal artifacts that are used in safety-critical applications.
  arXiv  Detail & Related papers  (2023-09-28T13:40:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.