論文の概要: TrustedCode: Evaluating Large Language Models for Developing Trusted Code through Automated Program Verification

• arxiv url: http://arxiv.org/abs/2610.30432v1
• Date: Wed, 21 Oct 2026 20:40:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-24 02:08:44.131837
• Title: TrustedCode: Evaluating Large Language Models for Developing Trusted Code through Automated Program Verification
• Title（参考訳）: TrustedCode: プログラムの自動検証による信頼されたコード開発のための大規模言語モデルの評価
• Abstract要約: 我々は、AI生成したPythonコードを検証する自動化フレームワークであるTrustedCodeを紹介した。 分析の結果、観察されたエラーの50%はドメイン知識のギャップによるもので、30%は構文上の不正確性によるもので、残りの20%は意味や型に関する問題によるものであることが判明した。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent reports, such as "Who is using AI to code?", indicate that approximately 30\% of Python code contributions to GitHub are AI-generated. Given the inherent unreliability of this code, formal verification emerges as a promising approach to establish trust in software correctness. Although leveraging large language models (LLMs) for formal verification has garnered increasing attention, practical adoption remains limited due to the challenges in writing formal specifications and verifying program correctness against them. Existing tools predominantly support verification for languages such as Java and C, with minimal support for Python. We present TrustedCode, an automated framework for verifying AI-generated Python code. TrustedCode uses LLMs to (i) type-check Python code, (ii) translate it into WhyML via the Why3 framework, and (iii) verify it against formal specifications using Why3 back-end automated theorem provers. Our method integrates chain-of-thought prompting through LangGraph to identify and address LLM limitations in specification generation and proving the specified programs. To evaluate TrustedCode, we conducted experiments on ten Python programs of varying complexity. Our analysis reveals that 50\% of the observed errors stem from domain knowledge gaps, 30\% from syntactic inaccuracies, and the remaining 20\% from semantic and type-related issues. These findings underscore the importance of targeted improvements in LLM-guided formal verification workflows for Python. TrustedCode is an open source tool available at: \href{github.com/mtaimoorkhan/TrustedCode}{github.com/mtaimoorkhan/TrustedCode}. The video demonstration is available at: \href{youtu.be/Nr5I2g8ec-s}{youtu.be/Nr5I2g8ec-s}
• Abstract（参考訳）: のような最近のレポートは、GitHubへのPythonコードのコントリビューションの約30%がAI生成であることを示している。 このコードの本質的な信頼性の欠如を考えると、形式的検証はソフトウェア正当性に対する信頼を確立するための有望なアプローチとして現れます。 大型言語モデル(LLM)を形式的検証に活用することは注目度が高まっているが、形式的な仕様記述やプログラムの正当性検証の難しさから、実際的な採用は限られている。 既存のツールは、主にJavaやCのような言語の検証をサポートし、Pythonを最小サポートしている。 我々は、AI生成したPythonコードを検証する自動化フレームワークであるTrustedCodeを紹介した。 TrustedCode は LLM を使っています (i) Python コードの型チェック (ii)Why3フレームワークを介してWhyMLに翻訳し、 三 バックエンド自動定理証明器を用いて形式的な仕様に対して検証すること。 提案手法は,LangGraph を通じて,仕様生成における LLM の制限を識別および対処し,指定されたプログラムを証明するためのチェーン・オブ・シント・プロンプトを統合している。 TrustedCodeを評価するために、我々は複雑さの異なる10のPythonプログラムの実験を行った。 分析の結果、観察されたエラーの50%はドメインの知識ギャップによるもので、30%は構文上の不正確性によるもので、残りの20%は意味的・型的問題によるものであることが判明した。 これらの知見は、Python用のLLMガイダンス形式検証ワークフローにおいて、ターゲットとなる改善の重要性を浮き彫りにしている。 TrustedCodeは、以下のオープンソースツールで利用可能である。 ビデオデモは以下の通り。 \href{youtu.be/Nr5I2g8ec-s}{youtu.be/Nr5I2g8ec-s}

関連論文リスト

• Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning [7.228124845671868]
  ニューロフォーマル検証(NFV)は、主流プログラミング言語の開発者の自動化を活用する。 AI符号化エージェントが翻訳し、確立された検証者が決定し、機械チェックされた証明により、音質よりも経験的精度で、主流言語で提起された質問にプッシュボタンで回答する。 正誤のPython問題のデータセットの結果は、llm-as-judgeベースラインと比較して推奨されている。
  論文  参考訳（メタデータ） (2026-08-21T18:00:02Z)
• 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)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。 IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
  論文  参考訳（メタデータ） (2025-07-30T08:08:48Z)
• 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)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  大きな言語モデル(LLM)は、非公式な自然言語(NL)の意図からコードを生成する。 自然言語は曖昧であり、形式的な意味論が欠けているため、正確性の概念を定義するのは難しい。 言語に依存しない抽象アルゴリズムと具体的な実装TiCoderについて述べる。
  論文  参考訳（メタデータ） (2022-08-11T17:41:08Z)

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

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