Boosting Skeleton-Driven SMT Solver Fuzzing by Leveraging LLM to Produce Formula Generators
作者: Maolin Sun, Yibiao Yang, Yuming Zhou
分类: cs.SE, cs.AI, cs.PL
发布日期: 2025-08-28
💡 一句话要点
Chimera：利用LLM生成公式生成器，提升骨架驱动的SMT求解器模糊测试
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: SMT求解器 模糊测试 大型语言模型 代码生成 形式化验证
📋 核心要点
- 现有SMT求解器模糊测试方法难以跟上求解器功能的快速发展，且基于LLM的直接公式生成方法存在语法错误率高和计算开销大的问题。
- Chimera框架利用LLM合成可重用的术语生成器，并用其填充从现有公式派生的结构骨架，从而保证语法有效性并降低计算成本。
- 实验表明，Chimera在Z3和cvc5上发现了43个已确认的错误，其中40个已被修复，验证了该方法的有效性。
📝 摘要（中文）
SMT（Satisfiability Modulo Theory）求解器是现代系统和编程语言研究的基础，为符号执行和自动验证等任务提供基础。由于这些求解器位于关键路径上，因此其正确性至关重要，高质量的测试公式是发现错误的关键。然而，虽然先前的测试技术在早期求解器版本上表现良好，但它们难以跟上快速发展的功能。最近基于大型语言模型（LLM）的方法在探索高级求解器功能方面显示出希望，但仍然存在两个障碍：近一半生成的公式在语法上无效，并且与LLM的迭代交互引入了大量的计算开销。在本研究中，我们提出了Chimera，一种新颖的LLM辅助模糊测试框架，通过将直接公式生成转变为可重用的术语（即逻辑表达式）生成器的合成来解决这两个问题。Chimera使用LLM自动从文档中提取SMT理论的上下文无关文法（CFG），包括求解器特定的扩展，并合成符合这些文法的可组合布尔术语生成器。在模糊测试期间，Chimera使用LLM合成的生成器迭代生成的术语填充从现有公式派生的结构骨架。这种设计确保了语法有效性，同时促进了语义多样性。值得注意的是，Chimera只需要一次性的LLM交互投资，从而大大降低了运行时成本。我们在两个领先的SMT求解器Z3和cvc5上评估了Chimera。我们的实验表明，Chimera已经发现了43个已确认的错误，其中40个已经被开发人员修复。
🔬 方法详解
问题定义：论文旨在解决SMT求解器模糊测试中，现有方法难以有效利用LLM探索高级求解器功能，且直接使用LLM生成公式存在语法错误率高和计算开销大的问题。现有方法无法很好地平衡公式的有效性和生成效率。
核心思路：论文的核心思路是将LLM从直接生成公式转变为生成可重用的术语生成器。通过让LLM学习SMT理论的语法规则，并生成符合这些规则的术语生成器，可以确保生成的公式在语法上是有效的。同时，通过复用这些生成器，可以降低与LLM交互的频率，从而降低计算开销。
技术框架：Chimera框架主要包含以下几个阶段：1) 语法提取：利用LLM从SMT求解器的文档中自动提取上下文无关文法（CFG），包括求解器特定的扩展。2) 生成器合成：利用LLM合成可组合的布尔术语生成器，这些生成器符合提取的CFG。3) 骨架填充：在模糊测试期间，从现有公式派生结构骨架，并使用LLM合成的生成器迭代生成的术语填充这些骨架。4) 公式测试：将生成的公式输入到SMT求解器中进行测试，并报告发现的错误。
关键创新：Chimera的关键创新在于利用LLM生成可重用的术语生成器，而不是直接生成公式。这种方法确保了生成的公式在语法上是有效的，同时降低了计算开销。此外，Chimera还能够自动从文档中提取SMT理论的语法规则，从而减少了人工干预。
关键设计：Chimera的关键设计包括：1) 使用LLM进行语法提取和生成器合成的具体prompt设计；2) 如何从现有公式中提取结构骨架；3) 如何控制生成器的多样性，以探索不同的语义空间；4) 如何有效地将生成的公式输入到SMT求解器中进行测试，并报告发现的错误。论文中可能包含关于LLM选择、prompt工程、骨架提取算法和模糊测试策略等方面的具体细节，但具体参数设置和损失函数等细节未知。
🖼️ 关键图片
📊 实验亮点
Chimera在Z3和cvc5两个主流SMT求解器上进行了评估，发现了43个已确认的bug，其中40个已经被开发者修复。这表明Chimera能够有效地发现现有模糊测试方法难以发现的bug，显著提升了SMT求解器的测试效率和质量。具体的性能数据和对比基线在论文中可能有所体现，但此处未知。
🎯 应用场景
Chimera框架可应用于各种SMT求解器的模糊测试，提高求解器的可靠性和安全性。通过自动发现和修复求解器中的错误，可以提升依赖于这些求解器的软件系统的质量。该研究对于形式化验证、程序分析和软件测试等领域具有重要意义，并有助于构建更安全可靠的软件系统。
📄 摘要（原文）
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.