論文の概要: Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code

• arxiv url: http://arxiv.org/abs/2603.19239v1
• Date: Sat, 31 Jan 2026 07:14:57 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-06 02:36:12.765004
• Title: Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code
• Title（参考訳）: LLM生成ゴースト符号を用いた記号実行における論理爆弾の定義
• Authors: Dimitrios Stamatios Bouras, Sergey Mechtaev,
• Abstract要約: Gordianはハイブリッドなシンボリック実行フレームワークである。 軽量なゴーストコードを生成し、SMTソルバがソルバ-ホストコードのフラグメントを処理するのに役立つ。 従来のシンボリックな実行ベースラインよりも平均52～84%のカバレッジ向上を実現している。
• 参考スコア（独自算出の注目度）: 2.0890922389987683
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Symbolic execution is a powerful program analysis technique, but its effectiveness is fundamentally limited by solver-hostile program fragments, complex numerical reasoning, and unbounded heap structures. Recent work proposed replacing constraint solvers with large language models (LLMs) to bypass these limitations, but such approaches struggle to analyze real-world codebases, where deep execution paths require globally consistent reasoning across many interacting constraints. We present Gordian, a hybrid symbolic execution framework that uses LLMs selectively to generate lightweight ghost code that aids an SMT solver in handling solver-hostile code fragments, while preserving its precise, global reasoning capability. In particular, we propose three types of ghost code: (1) inversion of difficult code fragments with iterative bidirectional constraint propagation, (2) modeling via solver-friendly surrogates while preserving relevant behavior, and (3) semantic partitioning of unbounded heap spaces. We implemented Gordian on top of the KLEE symbolic execution engine and evaluated it on synthetic "logic bombs" capturing distinct symbolic reasoning challenges, a popular mathematical library FDLibM, and three structured-input programs (libexpat, jq, and bc). Across all benchmarks, Gordian improves coverage on average by 52-84% over traditional symbolic execution baselines, and by 86-419% over LLM-based techniques, while reducing LLM token usage by an average of 90-96%. This highlights the practicality and effectiveness of this approach in real-world settings.
• Abstract（参考訳）: シンボリック実行は強力なプログラム解析手法であるが、その効果はソルバ・ホスト型プログラムフラグメント、複素数値推論、および非有界ヒープ構造によって根本的に制限されている。 最近の研究は、制約解決を大きな言語モデル(LLM)に置き換えてこれらの制限を回避することを提案したが、そのようなアプローチは、多くの相互作用する制約に対して、深い実行パスが一貫した推論を必要とする実世界のコードベースを分析するのに苦労している。 本稿では,LLMを選択的に使用するハイブリッドなシンボル実行フレームワークであるGordianについて述べる。 具体的には,(1) 難解なコードフラグメントの反復的双方向制約伝搬による逆転,(2) 関連する振る舞いを保ちながらソルバフレンドリーなサロゲートによるモデリング,(3) 有界なヒープ空間のセマンティックパーティショニング,の3種類のゴーストコードを提案する。 我々は,KLEEシンボリック実行エンジン上にGordianを実装し,異なるシンボリック推論課題,一般的な数学ライブラリFDLibM,構造化入力プログラム(libexpat,jq,bc)を合成した「論理爆弾」を用いて評価した。 すべてのベンチマークで、Gordianは従来のシンボリックな実行ベースラインよりも平均52～84%、LLMベースのテクニックよりも86～419%、LLMトークンの使用率の平均90～96%の改善を実現している。 これは、実際の環境でのこのアプローチの実践性と有効性を強調します。

関連論文リスト

• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。 テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。 そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
  論文  参考訳（メタデータ） (2026-02-02T09:14:51Z)
• Programming over Thinking: Efficient and Robust Multi-Constraint Planning [54.77940831026738]
  SCOPEは、クエリ固有の推論をジェネリックコード実行から切り離すフレームワークである。 SCOPEは、コストとレイテンシを下げながら最先端のパフォーマンスを達成する。
  論文  参考訳（メタデータ） (2026-01-14T02:58:07Z)
• Can Large Language Models Solve Path Constraints in Symbolic Execution? [32.45630887872447]
  我々は,経路制約問題の解決に大規模言語モデル(LLM)を採用する可能性を検討することに注力する。 テストケース生成とパス分類という2つのタスクのための新しい評価パイプラインとベンチマークを構築します。 実験の結果,LLMは生成タスクと分類タスクの両方において経路制約を解くことができることがわかった。
  論文  参考訳（メタデータ） (2025-11-23T04:54:48Z)
• Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models [7.658134651527103]
  最悪のケースのシンボリック制約分析では、最悪のケースのプログラムの実行を特徴付けるシンボリック制約を推論する必要がある。 我々は,現在最先端の大規模言語モデル (LLM) でさえ,このタスクに直接適用した場合に苦労することを示す。 我々は,より小さな具体的入力サイズに対する最悪の制約を計算する,革新的ニューロシンボリックアプローチであるWARPを提案する。
  論文  参考訳（メタデータ） (2025-06-09T19:33:30Z)
• SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning [30.938876549335067]
  本稿では,新しいニューロン-シンボリックRTL最適化フレームワークであるSymRTLOを提案する。 有限状態機械(FSM)論理の解析と最適化のための記号モジュールを提案する。 Synopsys Design Compiler と Yosys による RTL-Rewriter ベンチマークの実験では、SymRTLO は 43.9% と 62.5% と 51.1% に向上している。
  論文  参考訳（メタデータ） (2025-04-14T16:15:55Z)
• Control Large Language Models via Divide and Conquer [94.48784966256463]
  本稿では,Lexically Constrained Generation(LCG)に着目し,大規模言語モデル(LLM)のプロンプトベース制御による制御可能生成について検討する。 我々は,レキシカル制約を満たすためのLLMの性能を,プロンプトベース制御により評価し,下流アプリケーションでの有効性を検証した。
  論文  参考訳（メタデータ） (2024-10-06T21:20:06Z)
• Python Symbolic Execution with LLM-powered Code Generation [40.906079949304726]
  シンボリック実行はソフトウェアテストにおいて重要な技術であり、シンボリックパスの制約を収集してテストケースを生成する。 シンボリック実行は高いカバレッジテストケースを生成する上で有効であることが証明されている。 本稿では,実行経路制約を解決するために,SMTソルバ,Z3を自動的に呼び出すエージェント LLM-Sym を提案する。
  論文  参考訳（メタデータ） (2024-09-14T02:43:20Z)
• Hierarchical Context Merging: Better Long Context Understanding for Pre-trained LLMs [61.40047491337793]
  本稿では,大規模言語モデルの制約を克服する新しいトレーニングフリースキームである階層型cOntext MERging(HOMER)を提案する。 HomeRは、長いインプットを管理可能なチャンクに分割する、分別/対数アルゴリズムを使用する。 トークン削減技術がマージ毎に先行し、メモリ使用効率が保証される。
  論文  参考訳（メタデータ） (2024-04-16T06:34:08Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)

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

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