論文の概要: Can LLMs Enable Verification in Mainstream Programming?
- arxiv url: http://arxiv.org/abs/2503.14183v1
- Date: Tue, 18 Mar 2025 11:58:00 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-03-19 14:18:08.160816
- Title: Can LLMs Enable Verification in Mainstream Programming?
- Title(参考訳): LLMは主流プログラミングにおける検証を可能にするか?
- Authors: Aleksandr Shefer, Igor Engel, Stanislav Alekseev, Daniil Berezun, Ekaterina Verbitskaia, Anton Podkopaev,
- Abstract要約: LLMが3つの検証言語で検証コードを生成する能力について検討する。
そのために、最先端のPythonベンチマークであるHumanEvalから派生した、手動でキュレートされたデータセットを使用します。
- 参考スコア(独自算出の注目度): 37.69303106863453
- License:
- Abstract: Although formal methods are capable of producing reliable software, they have seen minimal adoption in everyday programming. Automatic code generation using large language models is becoming increasingly widespread, but it rarely considers producing strong correctness guarantees. In this study, we explore the ability of LLMs to produce verified code in three verification languages (Dafny, Nagini, and Verus). To do so, we use manually curated datasets derived from the state-ofthe-art Python benchmark, HumanEval. We also assess what types of information are sufficient to achieve good-quality results.
- Abstract(参考訳): 形式的手法は信頼性の高いソフトウェアを作成できるが、日々のプログラミングにはほとんど採用されていない。
大規模言語モデルを用いた自動コード生成はますます広まりつつあるが、強い正確性を保証することはめったにない。
本研究では,3つの検証言語(Dafny,Nagini,Verus)において,LLMが検証コードを生成する能力について検討した。
そのために、最先端のPythonベンチマークであるHumanEvalから派生した、手動でキュレートされたデータセットを使用します。
また、良質な結果を得るのに十分な種類の情報も評価する。
関連論文リスト
- Dafny as Verification-Aware Intermediate Language for Code Generation [0.0]
大規模言語モデル(LLM)は、自然言語プロンプトからソースコードを生成する。
その制限の1つは、生成したコードが正しいようにユーザに提示されているにもかかわらず、時に故障する可能性があることである。
ユーザがLSMをガイドして,まず不透明な中間表現を生成することを,検証対応言語であるDafnyで提案する。
正しいDafnyプログラムはターゲット言語にコンパイルされ、ユーザに返される。
論文 参考訳(メタデータ) (2025-01-10T17:23:14Z) - Effective LLM-Driven Code Generation with Pythoness [0.0]
Pythonessは、大きな言語モデル(LLM)を使用したコード生成のための組み込みドメイン固有言語である。
Pythonessでは、関数やクラス、プログラム全体を記述する際に、開発者は振る舞い仕様のレベルで動作します。
Pythonessは、テストとコード生成の組み合わせをうまく利用して、仕様のみよりも高品質なコードを生成することができることを示す。
論文 参考訳(メタデータ) (2025-01-03T23:14:46Z) - CodeGRAG: Bridging the Gap between Natural Language and Programming Language via Graphical Retrieval Augmented Generation [58.84212778960507]
我々は,LLMの性能を高めるため,グラフィカル検索拡張コード生成フレームワークであるCodeGRAGを提案する。
CodeGRAGは、制御フローとデータフローに基づいて、コードブロックのグラフィカルなビューを構築し、プログラミング言語と自然言語のギャップを埋める。
ハードメタグラフプロンプト、ソフトプロンプト技術、事前訓練されたGNN専門家の目的の有効性を検証するために、C++言語とピソン言語の両方を含む4つのデータセットで様々な実験と改善が行われた。
論文 参考訳(メタデータ) (2024-05-03T02:48:55Z) - Large Language Model-Aware In-Context Learning for Code Generation [75.68709482932903]
大規模言語モデル(LLM)は、コード生成において印象的なコンテキスト内学習(ICL)能力を示している。
コード生成のためのLAIL (LLM-Aware In-context Learning) という新しい学習ベース選択手法を提案する。
論文 参考訳(メタデータ) (2023-10-15T06:12:58Z) - How Effective are Large Language Models in Generating Software Specifications? [14.170320751508502]
大規模言語モデル(LLM)は多くのソフトウェア工学(SE)タスクにうまく適用されている。
ソフトウェアコメントやドキュメンテーションからソフトウェア仕様を生成するためのLCMの能力を評価するための、最初の実証的研究を行う。
論文 参考訳(メタデータ) (2023-06-06T00:28:39Z) - SelfEvolve: A Code Evolution Framework via Large Language Models [5.6607714367826105]
大きな言語モデル(LLM)は、公開コードデータで事前訓練された後、コード生成に革命をもたらした。
本稿では,LLMを知識提供者と自己表現型プログラマの両方として活用する,autoknowと呼ばれる新しい2段階パイプラインを提案する。
データサイエンスコードのDS-1000、ソフトウェアエンジニアリングコードのHumanEval、C++からPythonへの翻訳のためのTransCoderの3つの自動知識生成データセットを評価した。
論文 参考訳(メタデータ) (2023-06-05T14:12:46Z) - Self-Checker: Plug-and-Play Modules for Fact-Checking with Large Language Models [75.75038268227554]
Self-Checkerはファクトチェックを容易にするプラグインとプレイモジュールからなるフレームワークである。
このフレームワークは、低リソース環境でファクトチェックシステムを構築するための、高速で効率的な方法を提供する。
論文 参考訳(メタデータ) (2023-05-24T01:46: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) - X-FACTR: Multilingual Factual Knowledge Retrieval from Pretrained
Language Models [103.75890012041366]
言語モデル(LM)は、事実の知識を捉えるのに驚くほど成功した。
しかし、LMの実際の表現能力の研究は、ほぼ間違いなく英語で行われている。
我々は23の語型的多様言語に対するクローゼスタイルプローブのベンチマークを作成する。
論文 参考訳(メタデータ) (2020-10-13T05:29:56Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。