論文の概要: Towards Formal Verification of LLM-Generated Code from Natural Language Prompts

• arxiv url: http://arxiv.org/abs/2507.13290v1
• Date: Thu, 17 Jul 2025 16:54:42 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-18 20:10:24.581647
• Title: Towards Formal Verification of LLM-Generated Code from Natural Language Prompts
• Title（参考訳）: 自然言語プロンプトからのLLM生成コードの形式的検証に向けて
• Authors: Aaron Councilman, David Fu, Aryan Gupta, Chengxiao Wang, David Grove, Yu-Xiong Wang, Vikram Adve,
• Abstract要約: LLM生成したコードに対して、正式な正当性を保証することを目指している。 本稿では,ユーザの意図を形式的に定義されているが,自然言語的な方法で表現できる形式的なクエリ言語を提案する。 83%のケースで正しいコードを検証でき、92%で間違ったコードを識別できます。
• 参考スコア（独自算出の注目度）: 17.130884318613944
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: In the past few years LLMs have emerged as a tool that can aid programmers by taking natural language descriptions and generating code based on it. However, LLMs often generate incorrect code that users need to fix and the literature suggests users often struggle to detect these errors. In this work we seek to offer formal guarantees of correctness to LLM generated code; such guarantees could improve the experience of using AI Code Assistants and potentially enable natural language programming for users with little or no programming knowledge. To address this challenge we propose to incorporate a formal query language that can represent a user's intent in a formally defined but natural language-like manner that a user can confirm matches their intent. Then, using such a query we propose to verify LLM generated code to ensure it matches the user's intent. We implement these ideas in our system, Astrogator, for the Ansible programming language which includes such a formal query language, a calculus for representing the behavior of Ansible programs, and a symbolic interpreter which is used for the verification. On a benchmark suite of 21 code-generation tasks, our verifier is able to verify correct code in 83% of cases and identify incorrect code in 92%.
• Abstract（参考訳）: 過去数年間、LLMは自然言語記述を取り込み、それに基づいてコードを生成することでプログラマを助けるツールとして登場した。 しかし、LSMは、ユーザーが修正する必要がある間違ったコードを生成することが多く、文献では、ユーザがこれらのエラーを検出するのに苦労していることを示唆している。 このような保証は、AI Code Assistantsの使用経験を改善し、プログラミング知識のほとんど、あるいは全くないユーザのための自然言語プログラミングを可能にする可能性がある。 この課題に対処するために,ユーザの意図を記述可能な形式的なクエリ言語を,ユーザがその意図に一致することを確認可能な,形式的だが自然言語的な方法で組み込むことを提案する。 そして,そのようなクエリを用いてLCM生成したコードを検証し,ユーザの意図に合致するようにすることを提案する。 本システムでは,このような形式的なクエリ言語,Ansibleプログラムの動作を表す計算,検証に使用されるシンボリックインタプリタを含むAnsibleプログラミング言語のAstrogatorを実装している。 21のコード生成タスクのベンチマークスイートでは、83%のケースで正しいコードを検証でき、92%で間違ったコードを識別できます。

関連論文リスト

• IFEvalCode: Controlled Code Generation [69.28317223249358]
  本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。 IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
  論文  参考訳（メタデータ） (2025-07-30T08:08:48Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。 そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。 提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
  論文  参考訳（メタデータ） (2025-04-12T15:03:00Z)
• How Accurately Do Large Language Models Understand Code? [4.817546726074033]
  大規模言語モデル(LLM)は、コードの修復やテストといった開発後のタスクでますます使われています。 コードの理解の定量化は、その抽象的な性質と標準化されたメトリクスの欠如のために難しい。 本稿では,LLMのコード理解能力に関する大規模な実証的研究を行った。
  論文  参考訳（メタデータ） (2025-04-06T05:59:29Z)
• HoarePrompt: Structural Reasoning About Program Correctness in Natural Language [6.0749049701897295]
  HoarePromptは、プログラム分析や検証から自然言語アーティファクトへの基本的な考え方を適応する、新しいアプローチである。 ループを管理するために,モデル検査に広く用いられているk-induction法の適応として,数発のk-inductionを提案する。 実験の結果,HoarePromptはZero-shot-CoTプロンプトを正当性分類に用いた場合に比べて,MCCを62%改善することがわかった。
  論文  参考訳（メタデータ） (2025-03-25T12:30:30Z)
• Dafny as Verification-Aware Intermediate Language for Code Generation [0.0]
  大規模言語モデル(LLM)は、自然言語プロンプトからソースコードを生成する。 その制限の1つは、生成したコードが正しいようにユーザに提示されているにもかかわらず、時に故障する可能性があることである。 ユーザがLSMをガイドして,まず不透明な中間表現を生成することを,検証対応言語であるDafnyで提案する。 正しいDafnyプログラムはターゲット言語にコンパイルされ、ユーザに返される。
  論文  参考訳（メタデータ） (2025-01-10T17:23:14Z)
• Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages [21.18996339478024]
  SPEAC(emphsynthetic programming elicitation and compilation)を紹介する。 SPEACは、より頻繁に、意味的正しさを犠牲にすることなく、構文的に正しいプログラムを生成する。 UCLID5形式検証言語のケーススタディにおいて,SPEACの性能を実証的に評価した。
  論文  参考訳（メタデータ） (2024-06-05T22:16:19Z)
• Code Prompting Elicits Conditional Reasoning Abilities in Text+Code LLMs [65.2379940117181]
  自然言語の問題をコードに変換する一連のプロンプトであるコードプロンプトを導入します。 コードプロンプトは複数のLLMに対して高速に向上することがわかった。 GPT 3.5を解析した結果,入力問題のコードフォーマッティングが性能向上に不可欠であることが判明した。
  論文  参考訳（メタデータ） (2024-01-18T15:32:24Z)
• 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)
• Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions? [17.03841665553565]
  大きな言語モデル(LLM)は、プログラマの意図にマッチする仕様への自然言語の意図の翻訳を容易にする可能性がある。 本稿では,プログラムアサーションとして表現された,非公式な自然言語形式的メソッドのポストコンディションにLLMを活用する問題であるnl2postcondについて述べる。
  論文  参考訳（メタデータ） (2023-10-03T06:55:45Z)
• Fixing Large Language Models' Specification Misunderstanding for Better Code Generation [13.494822086550604]
  muFiXは、大きな言語モデル(LLM)のコード生成性能を改善する新しいプロンプト技術である。 まず、テストケース分析を利用して仕様の理解を得、自己改善プロセスを可能にする。 muFiXはさらに、提供された理解と実際の理解の間のギャップを減らす方向に向けた仕様理解を修正している。
  論文  参考訳（メタデータ） (2023-09-28T02:58:07Z)
• LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
  本稿では,プログラムの実行結果の検証を学習することで,言語からコードへの生成を改善するシンプルな手法であるLEVERを提案する。 具体的には、LLMからサンプリングされたプログラムが、自然言語入力、プログラム自体とその実行結果に基づいて正しいか否かを判定するために、検証者を訓練する。 LEVER はベースコード LLMs (4.6% から 10.9% まで) を継続的に改善し、それらすべてに対して新しい最先端の結果を得る。
  論文  参考訳（メタデータ） (2023-02-16T18:23:22Z)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  大きな言語モデル(LLM)は、非公式な自然言語(NL)の意図からコードを生成する。 自然言語は曖昧であり、形式的な意味論が欠けているため、正確性の概念を定義するのは難しい。 言語に依存しない抽象アルゴリズムと具体的な実装TiCoderについて述べる。
  論文  参考訳（メタデータ） (2022-08-11T17:41:08Z)

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

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