論文の概要: Can Large Language Models Solve Path Constraints in Symbolic Execution?

• arxiv url: http://arxiv.org/abs/2511.18288v1
• Date: Sun, 23 Nov 2025 04:54:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-25 18:34:24.748903
• Title: Can Large Language Models Solve Path Constraints in Symbolic Execution?
• Title（参考訳）: 大言語モデルは記号実行における経路制約を解けるか?
• Authors: Wenhan Wang, Kaibo Liu, Zeyu Sun, An Ran Chen, Ge Li, Gang Huang, Lei Ma,
• Abstract要約: 我々は,経路制約問題の解決に大規模言語モデル(LLM)を採用する可能性を検討することに注力する。 テストケース生成とパス分類という2つのタスクのための新しい評価パイプラインとベンチマークを構築します。 実験の結果,LLMは生成タスクと分類タスクの両方において経路制約を解くことができることがわかった。
• 参考スコア（独自算出の注目度）: 32.45630887872447
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Symbolic execution is an important software analysis technique which benefits downstream tasks such as software testing and debugging. However, several limitations hinder symbolic execution from application on real-world software. One of the limitations is the inability to solve diverse execution path constraints: traditional symbolic execution based on SMT solvers is difficult to handle execution paths with complex data structures or external API calls. In this paper, we focus on investigating the possibility of adopting large language models (LLM) for path constraint solving instead of traditional solver-based techniques in symbolic execution. We conduct an empirical study to evaluate the ability of LLMs in two types of path constraint solving: generating test inputs to facilitate an execution path, and determining whether a given execution path can be satisfied without triggering any bugs. We build new evaluation pipelines and benchmarks for two tasks: test case generation and path classification, which include data sources from both competition-level programs and real-world repositories. Our experiment results show that state-of-the-art LLMs are able to solve path constraints in both generation and classification tasks, with 60% of generated test cases that accurately cover the given execution path. Moreover, LLMs are capable of improving test coverage by covering execution paths in real-world repositories where traditional symbolic execution tools cannot be applied. These findings highlight the possibility of extending symbolic execution techniques with LLMs in the future to improve the ability and generalizability of symbolic execution.
• Abstract（参考訳）: シンボリック実行は、ソフトウェアテストやデバッグといった下流タスクの恩恵を受ける重要なソフトウェア分析技術である。 しかし、いくつかの制限は現実世界のソフトウェア上のアプリケーションから象徴的な実行を妨げる。 SMTソルバに基づく従来のシンボリックな実行は、複雑なデータ構造や外部API呼び出しによる実行パスの処理が難しい。 本稿では,従来の問題解決手法の代わりに,大規模言語モデル(LLM)を経路制約解決に適用する可能性を検討する。 テスト入力を生成して実行経路を容易にし、与えられた実行経路がバグを発生させることなく満足できるかどうかを判定する。 テストケース生成とパス分類という2つのタスクのための新しい評価パイプラインとベンチマークを構築します。 実験の結果,現状のLCMでは,与えられた実行経路を正確にカバーするテストケースの60%が生成され,生成タスクと分類タスクの両方において経路制約を解くことができることがわかった。 さらに、LLMは従来のシンボリックな実行ツールが適用できない実世界のリポジトリでの実行パスをカバーすることで、テストカバレッジを改善することができる。 これらの知見は,将来,シンボル実行の能力と一般化性を向上させるために,LLMによるシンボル実行技術の拡張の可能性を強調した。

関連論文リスト

• Rethinking Testing for LLM Applications: Characteristics, Challenges, and a Lightweight Interaction Protocol [83.83217247686402]
  大言語モデル(LLM)は、単純なテキストジェネレータから、検索強化、ツール呼び出し、マルチターンインタラクションを統合する複雑なソフトウェアシステムへと進化してきた。 その固有の非決定主義、ダイナミズム、文脈依存は品質保証に根本的な課題をもたらす。 本稿では,LLMアプリケーションを3層アーキテクチャに分解する: textbftextitSystem Shell Layer, textbftextitPrompt Orchestration Layer, textbftextitLLM Inference Core。
  論文  参考訳（メタデータ） (2025-08-28T13:00:28Z)
• Symbolic Execution in Practice: A Survey of Applications in Vulnerability, Malware, Firmware, and Protocol Analysis [3.1844358655583846]
  記号実行は、すべてのプログラムパスの体系的な探索を可能にする強力なプログラム解析技術である。 本稿では,複雑なソフトウェアシステム上でのシンボリックな実行を可能にする戦略の体系的な分類法を提案する。 脆弱性分析,マルウェア解析,ファームウェア再ホスト,ネットワークプロトコル解析など,いくつかの領域におけるシンボル実行の応用を調査した。
  論文  参考訳（メタデータ） (2025-08-08T18:43:45Z)
• Generating and Understanding Tests via Path-Aware Symbolic Execution with LLMs [8.828992823055]
  PALMは、シンボリックパス列挙とLLM支援テスト生成を組み合わせたテスト生成システムである。 Palmは、パスカバレッジをよりよく理解し、PALMが生成したテストで実際にどのパスが実行されているかを特定するのに役立つ。
  論文  参考訳（メタデータ） (2025-06-24T03:46:16Z)
• Beyond Next Token Probabilities: Learnable, Fast Detection of Hallucinations and Data Contamination on LLM Output Distributions [60.43398881149664]
  LLM出力シグナチャの効率的な符号化を訓練した軽量アテンションベースアーキテクチャであるLOS-Netを紹介する。 非常に低い検出レイテンシを維持しながら、さまざまなベンチマークやLLMで優れたパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2025-03-18T09:04:37Z)
• Test Wars: A Comparative Study of SBST, Symbolic Execution, and LLM-Based Approaches to Unit Test Generation [11.037212298533069]
  大規模言語モデル(LLM)は、自動テストを生成する新しい機会を開いた。 本稿では,SBSTのEvoSuite,シンボル実行のKex,LLMベースのテスト生成のTestSparkという3つのツールを用いた自動テスト生成手法について検討する。 以上の結果から,LSMベースのテスト生成は有望であるが,従来の手法には及ばないことがわかった。
  論文  参考訳（メタデータ） (2025-01-17T13:48:32Z)
• Test-driven Software Experimentation with LASSO: an LLM Prompt Benchmarking Example [1.4685355149711299]
  テスト駆動ソフトウェア実験(TDSE)は、ソフトウェア主題の実行と、その"事実上の"実行時の振る舞いの観察と分析を含む。 本稿では,TDSEを行うための最小限のドメイン固有言語とデータ構造を提供するLASSOという汎用解析プラットフォームを提案する。
  論文  参考訳（メタデータ） (2024-10-11T15:32:48Z)
• Python Symbolic Execution with LLM-powered Code Generation [40.906079949304726]
  シンボリック実行はソフトウェアテストにおいて重要な技術であり、シンボリックパスの制約を収集してテストケースを生成する。 シンボリック実行は高いカバレッジテストケースを生成する上で有効であることが証明されている。 本稿では,実行経路制約を解決するために,SMTソルバ,Z3を自動的に呼び出すエージェント LLM-Sym を提案する。
  論文  参考訳（メタデータ） (2024-09-14T02:43:20Z)
• DOCE: Finding the Sweet Spot for Execution-Based Code Generation [69.5305729627198]
  本稿では,候補生成,$n$-best再ランク,最小ベイズリスク(MBR)復号化,自己老化などを含む包括的フレームワークを提案する。 本研究は,実行ベースメソッドの重要性と,実行ベースメソッドと実行フリーメソッドとの差を明らかにする。
  論文  参考訳（メタデータ） (2024-08-25T07:10:36Z)
• Can Long-Context Language Models Subsume Retrieval, RAG, SQL, and More? [54.667202878390526]
  長文言語モデル(LCLM)は、従来、検索システムやデータベースといった外部ツールに依存していたタスクへのアプローチに革命をもたらす可能性がある。 実世界のタスクのベンチマークであるLOFTを導入し、文脈内検索と推論においてLCLMの性能を評価するために設計された数百万のトークンを出力する。 以上の結果からLCLMは,これらのタスクを明示的に訓練したことがないにも関わらず,最先端の検索システムやRAGシステムと競合する驚くべき能力を示した。
  論文  参考訳（メタデータ） (2024-06-19T00:28:58Z)

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

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