論文の概要: Boosting Skeleton-Driven SMT Solver Fuzzing by Leveraging LLM to Produce Formula Generators

• arxiv url: http://arxiv.org/abs/2508.20340v1
• Date: Thu, 28 Aug 2025 01:21:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-29 18:12:01.884997
• Title: Boosting Skeleton-Driven SMT Solver Fuzzing by Leveraging LLM to Produce Formula Generators
• Title（参考訳）: LLMを利用したスケルトン駆動型SMTゾルバファズリングによるフォーミュラジェネレータの試作
• Authors: Maolin Sun, Yibiao Yang, Yuming Zhou,
• Abstract要約: 満足度・モデュロ理論 (Satifiability Modulo Theory, SMT) は、現代のシステムやプログラミング言語の研究に基礎を置いている。 以前のテストテクニックは、初期のソルババージョンではうまく機能していましたが、急速に進化する機能に追従するのに苦労しています。 近年のLarge Language Models (LLM) に基づくアプローチは,高度な問題解決能力の探求において有望であることを示している。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: 満足度モデュロ理論 (Satifiability Modulo Theory, SMT) は、現代のシステムやプログラミング言語の研究に基礎を置き、記号実行や自動検証といったタスクの基盤を提供する。 これらの解法はクリティカルパスに置かれているため、その正確性は不可欠であり、高品質のテスト公式はバグを明らかにするための鍵となる。 しかしながら、以前のテストテクニックは、早期の解決版ではうまく機能する一方で、急速に進化する機能に追従するのに苦労している。 近年のLarge Language Models (LLMs) に基づくアプローチは,高度な解法を探索する上で有望であることを示しているが,生成した公式のほぼ半分は構文的に無効であり,LLMとの反復的相互作用は計算上のオーバーヘッドを大幅に引き起こすという2つの障害が残っている。 本研究では, 直接公式生成から再利用可能な項(論理式)ジェネレータの合成にシフトすることで, 両方の問題に対処する新しいLCM支援ファジリングフレームワークであるChimeraを提案する。 特に、Chimera は LLM を用いて、(1) 文書からソルバ固有の拡張を含む SMT 理論の文脈自由文法 (CFG) を自動的に抽出し、(2) それらの文法に準拠した構成可能なブール項生成器を合成する。 ファジッシングの間、キメラはLLM合成ジェネレータによって反復的に生成される用語で既存の公式から派生した構造骨格をポップアップさせる。 この設計は、意味的多様性を促進しながら、構文的妥当性を保証する。 特に、Chimeraは一度のLLMインタラクション投資しか必要とせず、ランタイムコストを劇的に削減しています。 我々は,Z3とcvc5の2つの主要なSMT解法についてキメラの評価を行った。 我々の実験によると、Chimeraは43の確認済みバグを発見しており、そのうち40がすでに開発者によって修正されている。

関連論文リスト

• SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning [18.40402135952776]
  本稿では,新しいニューロン-シンボリックRTL最適化フレームワークであるSymRTLOを提案する。 有限状態機械(FSM)論理の解析と最適化のための記号モジュールを提案する。 Synopsys Design Compiler と Yosys による RTL-Rewriter ベンチマークの実験では、SymRTLO は 43.9% と 62.5% と 51.1% に向上している。
  論文  参考訳（メタデータ） (2025-04-14T16:15:55Z)
• D2LLM: Decomposed and Distilled Large Language Models for Semantic Search [18.63768158439252]
  D2LLMs-Decomposed and Distilled LLMs for semantic search。 クロスエンコーダを効率的なバイエンコーダに分解し,マルチヘッド・アテンションとインタラクション・エミュレーション・モジュールによるポーリングと統合する。 実験の結果,D2LLMは3つのタスクにまたがるすべての指標において,主要なベースラインを5つ超えていることがわかった。
  論文  参考訳（メタデータ） (2024-06-25T04:03:04Z)
• LLMRefine: Pinpointing and Refining Large Language Models via Fine-Grained Actionable Feedback [65.84061725174269]
  最近の大規模言語モデル(LLM)は、世代品質を改善するために人間のフィードバックを活用している。 LLMの出力を最適化する推論時間最適化手法であるLLMRefineを提案する。 機械翻訳、長文質問応答(QA)、話題要約を含む3つのテキスト生成タスクについて実験を行った。 LLMRefineは、すべてのベースラインアプローチを一貫して上回り、翻訳タスクの1.7 MetricXポイント、ASQAの8.1 ROUGE-L、トピックの要約の2.2 ROUGE-Lの改善を実現している。
  論文  参考訳（メタデータ） (2023-11-15T19:52:11Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  大規模言語モデル(LLM)は、コード解析と合成に成功している。 我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。 プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
  論文  参考訳（メタデータ） (2023-11-07T05:47:47Z)
• BOOST: Harnessing Black-Box Control to Boost Commonsense in LMs' Generation [60.77990074569754]
  本稿では,凍結した事前学習言語モデルを,より汎用的な生成に向けて操る,計算効率のよいフレームワークを提案する。 具体的には、まず、文に常識的スコアを割り当てる参照なし評価器を構築する。 次に、スコアラをコモンセンス知識のオラクルとして使用し、NADOと呼ばれる制御可能な生成法を拡張して補助ヘッドを訓練する。
  論文  参考訳（メタデータ） (2023-10-25T23:32:12Z)
• MuSR: Testing the Limits of Chain-of-thought with Multistep Soft Reasoning [63.80739044622555]
  自然言語ナラティブで指定されたソフト推論タスクの言語モデルを評価するデータセットである MuSR を紹介する。 このデータセットには2つの重要な特徴がある。まず、ニューロシンボリック合成-自然生成アルゴリズムによって生成される。 第二に、私たちのデータセットインスタンスは、実世界の推論の領域に対応する無料のテキスト物語です。
  論文  参考訳（メタデータ） (2023-10-24T17:59:20Z)
• Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving [23.426866969743525]
  インストラクショントレーニングを備えた生成型大規模言語モデル(LLM)は、プロンプトに対する人間的な応答を生成することができる。 精度が向上したにもかかわらず、これらのモデルは事実的に誤りまたは文脈的に不適切な結果をもたらすことが知られている。 この制限により、これらのモデルを使用して安全クリティカルなアプリケーションで使用される形式的なアーティファクトを合成することが困難になる。
  論文  参考訳（メタデータ） (2023-09-28T13:40:50Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。