論文の概要: SpecPylot: Python Specification Generation using Large Language Models
- arxiv url: http://arxiv.org/abs/2604.16560v1
- Date: Fri, 17 Apr 2026 08:53:02 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-22 14:04:47.793479
- Title: SpecPylot: Python Specification Generation using Large Language Models
- Title（参考訳）: SpecPylot: 大規模言語モデルを使用したPythonの仕様生成
- Authors: Ragib Shahariar Ayon, Shibbir Ahmed,
- Abstract要約: SpecPylotは、Pythonプログラムの実行可能な仕様をアイコン抽出アノテーションとして合成するPythonツールである。
このツールはLSMに頼って候補契約を提案し、クロスヘアを使って検証する。
全体としては、SpecPylotはほとんどのプログラムでクロスヘア互換のコントラクトを生成することができることを示している。
- 参考スコア（独自算出の注目度）: 1.0026496861838448
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Automatically generating formal specifications could reduce the effort needed to improve program correctness, but in practice, this is still challenging. Many developers avoid writing contracts by hand, which limits the use of automated verification tools. Recent large language models (LLMs) can generate specifications from code, but these specifications often fail in terms of verification. The reason is syntax errors, overly strict constraints, or mismatches with program behavior. We present SpecPylot, a Python tool that synthesizes executable specifications for Python programs as icontract annotations and checks them using crosshair's symbolic execution. The tool relies on LLMs to propose candidate contracts and uses crosshair to validate them. When crosshair finds a concrete counterexample, SpecPylot updates only the generated contracts and leaves the program itself untouched. In addition, the tool can produce coverage-driven pytest stubs and keep detailed execution artifacts that are useful during debugging. Overall, the evaluation indicates that SpecPylot is able to generate crosshair-compatible contracts for most programs, but it also highlights the practical limits introduced by bounded symbolic exploration and differences in LLM behavior.
- Abstract（参考訳）: 形式仕様の自動生成は、プログラムの正確性を改善するために必要な労力を削減できますが、実際には、これはまだ難しい作業です。
多くの開発者は手作業でコントラクトを書くことを避け、自動検証ツールの使用を制限する。
最近の大規模言語モデル(LLM)はコードから仕様を生成することができるが、これらの仕様は検証の点で失敗することが多い。
理由は、構文エラー、過度に厳格な制約、プログラムの振る舞いと不一致である。
SpecPylotは、Pythonプログラムの実行可能な仕様をアイコン抽出アノテーションとして合成し、クロスヘアのシンボリック実行を使ってそれらをチェックするPythonツールである。
このツールはLSMに頼って候補契約を提案し、クロスヘアを使って検証する。
クロスヘアが具体的な反例を見つけると、SpecPylotは生成されたコントラクトのみを更新し、プログラム自体に手を加えないままにする。
さらに、このツールはカバレッジ駆動のpytestスタブを生成し、デバッグ時に有用な詳細な実行アーティファクトを保持することができる。
全体としては、SpecPylotはほとんどのプログラムでクロスヘア互換の契約を生成することができるが、有界なシンボル探索とLLMの挙動の違いによってもたらされる実用的限界も強調している。
関連論文リスト
- CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
本稿では,実行ベース評価プロトコルの下で実行可能な動作仕様生成のためのベンチマークであるCodeSpecBenchを紹介する。
CodeSpecBenchは関数レベルとリポジトリレベルのタスクの両方をサポートし、仕様を実行可能なPython関数としてエンコードする。
リポジトリレベルのタスクでは、最高のモデルが20.2%のパス率しか達成できないため、パフォーマンスが大幅に低下するのを観察します。
論文 参考訳（メタデータ） (2026-04-14T04:31:45Z) - PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C [18.52519530244078]
Pythonは汎用プログラミングの主流言語になったが、形式検証のための堅牢なツールが欠けている。
PyVeritasはPythonからCへの高レベルのトランスパイルにLLM(Large Language Models)を利用する新しいフレームワークである。
論文 参考訳（メタデータ） (2025-08-11T16:49:07Z) - A Fast, Reliable, and Secure Programming Language for LLM Agents with Code Actions [28.01600045250939]
我々はQuasarと呼ばれるコードアクションのためのプログラミング言語を提案する。
LLMはPythonのサブセットでコードを書くことができ、自動的にQuasarに変換される。
Quasarアクションを持つLLMは高いパフォーマンスを維持し、可能な限り実行時間を42%削減する。
論文 参考訳（メタデータ） (2025-06-13T20:11:22Z) - VisCoder: Fine-Tuning LLMs for Executable Python Visualization Code Generation [69.35779796364413]
提案するVisCode-200Kは,Pythonによる可視化と自己補正のための大規模インストラクションチューニングデータセットである。
1)オープンソースリポジトリからの検証済みプロットコードと自然言語命令と描画プロットのペア,(2)Code-Feedbackからの45Kのマルチターン補正ダイアログ。
論文 参考訳（メタデータ） (2025-06-04T13:24:44Z) - Effective LLM-Driven Code Generation with Pythoness [0.0]
Pythonessは、大きな言語モデル(LLM)を使用したコード生成のための組み込みドメイン固有言語である。
Pythonessでは、関数やクラス、プログラム全体を記述する際に、開発者は振る舞い仕様のレベルで動作します。
Pythonessは、テストとコード生成の組み合わせをうまく利用して、仕様のみよりも高品質なコードを生成することができることを示す。
論文 参考訳（メタデータ） (2025-01-03T23:14:46Z) - CRUXEval-X: A Benchmark for Multilingual Code Reasoning, Understanding and Execution [50.1875460416205]
CRUXEVAL-Xコード推論ベンチマークには19のプログラミング言語が含まれている。
各言語に対して少なくとも600人の被験者で構成され、合計19Kのコンテンツ一貫性テストがある。
Pythonでのみトレーニングされたモデルでさえ、他の言語で34.4%のPass@1を達成することができる。
論文 参考訳（メタデータ） (2024-08-23T11:43:00Z) - Effective Targeted Testing of Smart Contracts [0.0]
スマートコントラクトは不変であるため、バグを修正することはできない。
我々のフレームワークであるGriffinは、テストデータを生成するためにターゲットとなるシンボル実行技術を用いて、この欠陥に対処する。
本稿では、スマートコントラクトがターゲットとなるシンボル実行におけるレガシーソフトウェアとどのように異なるのか、そしてこれらの違いがツール構造に与える影響について論じる。
論文 参考訳（メタデータ） (2024-07-05T04:38:11Z) - NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
大規模言語モデル(LLM)のコードは通常、プログラムの表面テキスト形式に基づいて訓練される。
NExTは,プログラムの実行トレースを検査し,実行時の動作を判断する手法である。
論文 参考訳（メタデータ） (2024-04-23T01:46:32Z) - Binding Language Models in Symbolic Languages [146.3027328556881]
Binderはトレーニング不要のニューラルシンボリックフレームワークで、タスク入力をプログラムにマッピングする。
解析の段階では、Codexは元のプログラミング言語では答えられないタスク入力の一部を特定することができる。
実行段階では、CodexはAPI呼び出しで適切なプロンプトを与えられた万能機能を実行することができる。
論文 参考訳（メタデータ） (2022-10-06T12:55:17Z) - Fault-Aware Neural Code Rankers [64.41888054066861]
サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。
我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
論文 参考訳（メタデータ） (2022-06-04T22:01:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。