論文の概要: PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C

• arxiv url: http://arxiv.org/abs/2508.08171v1
• Date: Mon, 11 Aug 2025 16:49:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-08-12 21:23:29.216752
• Title: PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C
• Title（参考訳）: PyVeritas: LLMベースのトランスパイルと境界モデルチェックによるPythonの検証について
• Authors: Pedro Orvalho, Marta Kwiatkowska,
• Abstract要約: Pythonは汎用プログラミングの主流言語になったが、形式検証のための堅牢なツールが欠けている。 PyVeritasはPythonからCへの高レベルのトランスパイルにLLM(Large Language Models)を利用する新しいフレームワークである。
• 参考スコア（独自算出の注目度）: 18.52519530244078
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Python has become the dominant language for general-purpose programming, yet it lacks robust tools for formal verification. In contrast, programmers working in languages such as C benefit from mature model checkers, for example CBMC, which enable exhaustive symbolic reasoning and fault localisation. The inherent complexity of Python, coupled with the verbosity and low-level nature of existing transpilers (e.g., Cython), have historically limited the applicability of formal verification to Python programs. In this paper, we propose PyVeritas, a novel framework that leverages Large Language Models (LLMs) for high-level transpilation from Python to C, followed by bounded model checking and MaxSAT-based fault localisation in the generated C code. PyVeritas enables verification and bug localisation for Python code using existing model checking tools for C. Our empirical evaluation on two Python benchmarks demonstrates that LLM-based transpilation can achieve a high degree of accuracy, up to 80--90% for some LLMs, enabling effective development environment that supports assertion-based verification and interpretable fault diagnosis for small yet non-trivial Python programs.
• Abstract（参考訳）: Pythonは汎用プログラミングの主流言語になったが、形式検証のための堅牢なツールが欠けている。 対照的に、C言語のような言語で働くプログラマは、CBMCのような成熟したモデルチェッカーの恩恵を受ける。 Pythonの本質的な複雑さは、既存のトランスパイラ(例えば、Cython)の冗長性と低レベルの性質と相まって、Pythonプログラムへの形式検証の適用性を歴史的に制限してきた。 本稿では,PythonからCへの高レベルトランスパイルにLarge Language Models(LLM)を利用する新しいフレームワークであるPyVeritasを提案する。 PyVeritasは、Pythonコードの検証とバグのローカライズを可能にする。2つのPythonベンチマークでの実証的な評価は、LLMベースのトランスパイルによって、いくつかのLLMで最大80-90%の精度を達成できることを示し、アサーションベースの検証と非自明なPythonプログラムの解釈可能な障害診断をサポートする効果的な開発環境を実現している。

関連論文リスト

• 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)
• Effective LLM-Driven Code Generation with Pythoness [0.0]
  Pythonessは、大きな言語モデル(LLM)を使用したコード生成のための組み込みドメイン固有言語である。 Pythonessでは、関数やクラス、プログラム全体を記述する際に、開発者は振る舞い仕様のレベルで動作します。 Pythonessは、テストとコード生成の組み合わせをうまく利用して、仕様のみよりも高品質なコードを生成することができることを示す。
  論文  参考訳（メタデータ） (2025-01-03T23:14:46Z)
• PyPulse: A Python Library for Biosignal Imputation [58.35269251730328]
  PyPulseは,臨床およびウェアラブルの両方のセンサ設定において生体信号の計算を行うPythonパッケージである。 PyPulseのフレームワークは、非機械学習バイオリサーバーを含む幅広いユーザーベースに対して、使い勝手の良いモジュラーで拡張可能なフレームワークを提供する。 PyPulseはMITライセンスでGithubとPyPIでリリースしました。
  論文  参考訳（メタデータ） (2024-12-09T11:00:55Z)
• 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)
• ESBMC-Python: A Bounded Model Checker for Python Programs [8.980206368890013]
  本稿では,Pythonプログラムの検証ツールを紹介する。 入力プログラムを抽象構文木に変換し、型情報を推論し追加する。 この記述を、満足度モジュラー理論の解法を用いて評価された公式に変換する。
  論文  参考訳（メタデータ） (2024-07-03T19:38:14Z)
• Python is Not Always the Best Choice: Embracing Multilingual Program of Thoughts [51.49688654641581]
  本稿では,多言語からの強みと多様性を生かしたMultiPoTというタスクとモデル非依存のアプローチを提案する。 実験の結果、Python Self-Consistencyを著しく上回ることがわかった。 特にMultiPoTはChatGPT(gpt-3.5-turbo-0701)で平均4.6%以上の改善を実現している。
  論文  参考訳（メタデータ） (2024-02-16T13:48:06Z)
• Transactional Python for Durable Machine Learning: Vision, Challenges, and Feasibility [5.669983975369642]
  Pythonアプリケーションは、トレーニングされたモデルや抽出された機能などの重要なデータを失う可能性がある。 本稿では,ユーザプログラムやPythonカーネルにコード修正を加えることなくDARTを提供するトランザクショナルPythonのビジョンについて述べる。 公開PyTorchおよびScikit-learnアプリケーションによる概念実証実装の評価は、DARTが1.5%～15.6%のオーバーヘッドで提供可能であることを示している。
  論文  参考訳（メタデータ） (2023-05-15T16:27:09Z)
• Using Python for Model Inference in Deep Learning [0.6027358520885614]
  pythonで推論を実行しながら、パフォーマンスとパッケージングの制約を満たす方法を示します。 複数のPythonインタプリタを単一のプロセスで使用して,スケーラブルな推論を実現する方法を提案する。
  論文  参考訳（メタデータ） (2021-04-01T04:48:52Z)
• OPFython: A Python-Inspired Optimum-Path Forest Classifier [68.8204255655161]
  本稿では,OPFythonと表記されるPythonベースのOptimum-Path Forestフレームワークを提案する。 OPFythonはPythonベースのライブラリなので、C言語よりもフレンドリーな環境とプロトタイピングの作業スペースを提供する。
  論文  参考訳（メタデータ） (2020-01-28T15:46:19Z)

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

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