論文の概要: RECON: An LLM-Enhanced Backward Constraint Analysis Framework
- arxiv url: http://arxiv.org/abs/2606.10264v1
- Date: Tue, 09 Jun 2026 00:09:50 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-11 16:42:37.969638
- Title: RECON: An LLM-Enhanced Backward Constraint Analysis Framework
- Title（参考訳）: RECON: LLM強化後方制約分析フレームワーク
- Authors: Babangida Bappah, Lamine Noureddine, Umar Farooq, Aisha Ali-Gombe,
- Abstract要約: 本稿では,新しい大規模言語モデル (LLM) を用いた後方制約解析フレームワークを提案する。
我々のアプローチはRECONと呼ばれ、ターゲットメソッドからアプリケーションエントリポイントへの後方経路探索を行い、メソッドレベルの制御フロー制約を発見し、LCM推論を利用してバイトコード条件を解釈可能な仕様に変換する。
その結果,従来のシンボル実行よりも5.8倍高速に動作し,論理的等価性を保ちながら100%の成功率を示した。
- 参考スコア（独自算出の注目度）: 0.5424799109837065
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: While traditional techniques, such as symbolic execution, provide a principled foundation for precise constraint reasoning in program analysis, they struggle to scale to modern software systems mainly due to path explosion, the need for function modeling, and the loss of semantic intent at low-level program representations. In complex execution environments such as Android, characterized by extensive framework interactions and event-driven behavior, these limitations are even more amplified. Thus, in this paper, we present a novel large language model (LLM)-enhanced backward constraint analysis framework that combines the precision of static program analysis with LLM's semantic understanding to extract precise execution constraints from Android bytecode. Our approach, titled RECON, performs backward path discovery from target method(s) to the application entry point(s), discovers method-level control-flow constraints, and leverages LLM reasoning to transform bytecode conditions into interpretable specifications. We evaluated RECON using five LLMs across 78 Android constraint-extraction scenarios and compared it with traditional symbolic execution on real-world applications. Results demonstrate that our approach operates 5.8X faster than traditional symbolic execution, with a 100% success rate, while maintaining logical equivalence and providing significantly more precise and interpretable output. We further evaluated RECON for malware analysis on 100 samples. The results indicate an 84% success rate in generating semantic constraints that lead to the execution of dangerous API behaviors and in detecting complex constraints across multiple execution paths.
- Abstract（参考訳）: 記号的実行のような伝統的な技術は、プログラム分析における厳密な制約推論の基礎となるが、経路の爆発、機能モデリングの必要性、低レベルのプログラム表現における意味的意図の喪失など、現代のソフトウェアシステムへの拡張に苦慮している。
Androidのような複雑な実行環境では、広範なフレームワークインタラクションとイベント駆動の振る舞いによって特徴づけられるが、これらの制限はさらに増幅されている。
そこで本稿では,静的プログラム解析の精度とLLMのセマンティック理解を組み合わせ,Androidバイトコードから正確な実行制約を抽出する,新しい大規模言語モデル(LLM)による後方制約解析フレームワークを提案する。
我々のアプローチはRECONと呼ばれ、ターゲットメソッドからアプリケーションエントリポイントへの後方経路探索を行い、メソッドレベルの制御フロー制約を発見し、LCM推論を利用してバイトコード条件を解釈可能な仕様に変換する。
78のAndroid制約抽出シナリオに対して,5つのLLMを用いてRECONを評価し,実世界のアプリケーション上での従来のシンボル実行と比較した。
その結果,従来のシンボル実行よりも5.8倍高速に動作し,100%の成功率を維持しつつ,論理的等価性を保ち,より正確かつ解釈可能な出力を提供することができた。
さらに,100検体を対象にマルウェア解析のためのRECONを評価した。
結果は、危険なAPI動作の実行につながるセマンティック制約の生成と、複数の実行パスにわたる複雑な制約の検出において、84%の成功率を示している。
関連論文リスト
- Evaluating the Formal Reasoning Capabilities of Large Language Models through Chomsky Hierarchy [62.32144504442516]
SOTA LLMが形式言語の構造的・階層的複雑性を把握できるかどうかは不明である。
ChomskyBench はchomsky Hierarchy のレンズを通して LLM を体系的に評価するためのベンチマークである。
ChomskyBenchは、各レベルで機能をテストするように設計された、言語認識と生成タスクの包括的なスイートで構成されている。
論文 参考訳（メタデータ） (2026-04-03T04:06:39Z) - Understanding by Reconstruction: Reversing the Software Development Process for LLM Pretraining [66.89012795621349]
大規模言語モデル(LLM)は、複雑なソフトウェア工学に必要な、深く、長期にわたる推論に苦しむことが多い。
本稿では,再構築による理解という,新しいパラダイムを提案する。
マルチエージェントシミュレーションを用いて潜在エージェント軌道を合成するフレームワークを提案する。
論文 参考訳（メタデータ） (2026-03-11T09:23:20Z) - Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code [2.0890922389987683]
Gordianはハイブリッドなシンボリック実行フレームワークである。
軽量なゴーストコードを生成し、SMTソルバがソルバ-ホストコードのフラグメントを処理するのに役立つ。
従来のシンボリックな実行ベースラインよりも平均52～84%のカバレッジ向上を実現している。
論文 参考訳（メタデータ） (2026-01-31T07:14:57Z) - VIRO: Robust and Efficient Neuro-Symbolic Reasoning with Verification for Referring Expression Comprehension [51.76841625486355]
Referring Expression (REC) は、自然言語クエリに対応する画像領域をローカライズすることを目的としている。
最近のニューロシンボリックRECアプローチは、大規模言語モデル(LLM)と視覚言語モデル(VLM)を利用して構成推論を行う。
推論ステップ内に軽量な演算子レベルの検証器を組み込む,ニューロシンボリックなフレームワークであるVIROを紹介する。
論文 参考訳（メタデータ） (2026-01-19T07:21:19Z) - From Brute Force to Semantic Insight: Performance-Guided Data Transformation Design with LLMs [48.83701310501069]
大規模言語モデル(LLM)は、コード合成において顕著な性能を達成した。
本稿では,LLMが最適変換を自律的に設計できる性能対応クローズドループソリューションを提案する。
6,000以上のPyTorch拡張関数を実験的に評価した新しいリポジトリ上で,低ランク適応型LPMを微調整する。
論文 参考訳（メタデータ） (2026-01-07T11:13:02Z) - KBQA-R1: Reinforcing Large Language Models for Knowledge Base Question Answering [64.62317305868264]
テキスト模倣から強化学習によるインタラクション最適化へパラダイムをシフトするフレームワークである textbfKBQA-R1 を提案する。
KBQAを多ターン決定プロセスとして扱うことで,行動のリストを用いて知識ベースをナビゲートすることを学ぶ。
WebQSP、GrailQA、GraphQuestionsの実験では、KBQA-R1が最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2025-12-10T17:45:42Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。