論文の概要: Python Symbolic Execution with LLM-powered Code Generation

• arxiv url: http://arxiv.org/abs/2409.09271v1
• Date: Sat, 14 Sep 2024 02:43:20 GMT
• ステータス: 処理完了
• システム内更新日: 2024-09-17 21:38:57.139186
• Title: Python Symbolic Execution with LLM-powered Code Generation
• Title（参考訳）: LLMを用いたコード生成によるPythonシンボリック実行
• Authors: Wenhan Wang, Kaibo Liu, An Ran Chen, Ge Li, Zhi Jin, Gang Huang, Lei Ma,
• Abstract要約: シンボリック実行はソフトウェアテストにおいて重要な技術であり、シンボリックパスの制約を収集してテストケースを生成する。 シンボリック実行は高いカバレッジテストケースを生成する上で有効であることが証明されている。 本稿では,実行経路制約を解決するために,SMTソルバ,Z3を自動的に呼び出すエージェント LLM-Sym を提案する。
• 参考スコア（独自算出の注目度）: 40.906079949304726
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Symbolic execution is a key technology in software testing, which generates test cases by collecting symbolic path constraints and then solving constraints with SMT solvers. Symbolic execution has been proven helpful in generating high-coverage test cases, but its limitations, e.g., the difficulties in solving path constraints, prevent it from broader usage in software testing. Moreover, symbolic execution has encountered many difficulties when applied to dynamically typed languages like Python, because it is extremely challenging to translate the flexible Python grammar into rigid solvers. To overcome the main challenges of applying symbolic execution in Python, we proposed an LLM-empowered agent, LLM-Sym, that automatically calls an SMT solver, Z3, to solve execution path constraints. Based on an introductory-level symbolic execution engine, our LLM agent can extend it to supporting programs with complex data type `list'. The core contribution of LLM-Sym is translating complex Python path constraints into Z3 code. To enable accurate path-to-Z3 translation, we design a multiple-step code generation pipeline including type inference, retrieval and self-refine. Our experiments demonstrate that LLM-Sym is capable of solving path constraints on Leetcode problems with complicated control flows and list data structures, which is impossible for the backbone symbolic execution engine. Our approach paves the way for the combination of the generation ability of LLMs with the reasoning ability of symbolic solvers, and opens up new opportunities in LLM-augmented test case generation.
• Abstract（参考訳）: シンボリック実行はソフトウェアテストにおいて重要な技術であり、シンボリックパスの制約を収集し、SMTソルバで制約を解くことによってテストケースを生成する。 シンボリックな実行は高いカバレッジテストケースを生成する上で有効であることが証明されている。 さらに、シンボリック実行は、Pythonのような動的型付け言語に適用する場合、柔軟性のあるPython文法を厳密なソルバに変換することが極めて難しいため、多くの困難に直面している。 LLM-Symは,SMTソルバ,Z3を自動的に呼び出して実行経路制約を解決する。 LLMエージェントは、入門レベルのシンボリック実行エンジンに基づいて、複雑なデータ型‘list’を持つプログラムに拡張することができる。 LLM-Symのコアコントリビューションは、複雑なPythonパスの制約をZ3コードに変換することだ。 正確なパス・ツー・Z3変換を実現するために,型推論,検索,自己修正を含む複数ステップのコード生成パイプラインを設計する。 実験の結果,LLM-Symは複雑な制御フローとリストデータ構造を持つLeetcode問題の経路制約を解くことができることがわかった。 提案手法は,LLMの生成能力とシンボリック・ソルバの推論能力の融合を図り,LLM拡張テストケース生成における新たな機会を開くものである。

関連論文リスト

• Capturing Sparks of Abstraction for the ARC Challenge [0.10878040851637999]
  商用のLarge Language Models(LLM)でさえ、多くの問題を"理解"するのに苦労しています。 LLM出力から'Sparks of Abstraction'を抽出できることを実証する。 arc-dsl-llm DSLフレームワークとGemini LLM生成データの両方がオープンソースになっている。
  論文  参考訳（メタデータ） (2024-11-17T23:40:00Z)
• Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis [0.7580487359358722]
  大規模言語モデル(LLM)は精度に苦しむが、リスクの高いアプリケーションには適さない。 コード生成を LLM で処理する部分と,形式的なメソッドベースのプログラム合成で処理する部分の2つに分割する手法を提案する。
  論文  参考訳（メタデータ） (2024-09-18T15:59:06Z)
• Can Language Models Pretend Solvers? Logic Code Simulation with LLMs [3.802945676202634]
  トランスフォーマーベースの大規模言語モデル(LLM)は、論理問題に対処する上で大きな可能性を示している。 この研究は、論理コードシミュレーションという新しい側面に発展し、論理プログラムの結果を予測するために論理解法をエミュレートするよう LLM に強制する。
  論文  参考訳（メタデータ） (2024-03-24T11:27:16Z)
• If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
  大型言語モデル(LLM)は、自然言語と形式言語(コード)の組み合わせに基づいて訓練される コードは、標準構文、論理一貫性、抽象化、モジュール性を備えた高レベルの目標を実行可能なステップに変換する。
  論文  参考訳（メタデータ） (2024-01-01T16:51:20Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• LPML: LLM-Prompting Markup Language for Mathematical Reasoning [8.995617701116142]
  外部ツール(Python REPL)とChain-of-Thought(CoT)メソッドを統合する新しいフレームワークを提案する。 提案手法は,ゼロショットプロンプトのみを用いて,LLMがマークアップ言語を記述し,高度な数学的推論を行うことを可能にする。
  論文  参考訳（メタデータ） (2023-09-21T02:46:20Z)
• Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning [101.26814728062065]
  大規模言語モデル(LLM)は人間のような推論能力を示しているが、それでも複雑な論理的問題に悩まされている。 本稿では,論理問題の解法を改善するために,LLMとシンボリックソルバを統合した新しいフレームワークであるLogic-LMを紹介する。
  論文  参考訳（メタデータ） (2023-05-20T22:25:38Z)
• Low-code LLM: Graphical User Interface over Large Language Models [115.08718239772107]
  本稿では,人間-LLMインタラクションフレームワークであるLow-code LLMを紹介する。 より制御可能で安定した応答を実現するために、6種類のシンプルなローコードビジュアルプログラミングインタラクションを組み込んでいる。 ユーザフレンドリなインタラクション,制御可能な生成,広い適用性という,低コード LLM の3つの利点を強調した。
  論文  参考訳（メタデータ） (2023-04-17T09:27:40Z)
• PAL: Program-aided Language Models [112.94785609781503]
  自然言語問題を理解するために,プログラム支援言語モデル(PaL)を提案する。 PaLはソリューションステップをPythonインタプリタのようなプログラムランタイムにオフロードする。 私たちは12のベンチマークで新しい最先端の結果を設定しました。
  論文  参考訳（メタデータ） (2022-11-18T18:56:13Z)

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

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