論文の概要: VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models
- arxiv url: http://arxiv.org/abs/2411.19275v1
- Date: Thu, 28 Nov 2024 17:12:21 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-12-02 20:28:07.840498
- Title: VeCoGen: Automating Generation of Formally Verified C Code with Large Language Models
- Title（参考訳）: VeCoGen: 大規模言語モデルによる形式検証Cコードの自動生成
- Authors: Merlijn Sevenhuijsen, Khashayar Etemadi, Mattias Nyberg,
- Abstract要約: VeCoGenは、LLM(Large Language Models)と形式検証を組み合わせた新しいツールで、公式に認証されたCプログラムを自動生成する。
VeCoGenは、自然言語仕様であるISO/ISO C Specification Language (ACSL) の正式な仕様と、プログラムの生成を試みるテストケースのセットを採っている。
- 参考スコア（独自算出の注目度）: 1.6249267147413524
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large Language Models (LLMs) have demonstrated impressive capabilities in generating code, yet they often produce programs with flaws or deviations from intended behavior, limiting their suitability for safety-critical applications. To address this limitation, this paper introduces VeCoGen, a novel tool that combines LLMs with formal verification to automate the generation of formally verified C programs. VeCoGen takes a formal specification in ANSI/ISO C Specification Language (ACSL), a natural language specification, and a set of test cases to attempt to generate a program. This program-generation process consists of two steps. First, VeCoGen generates an initial set of candidate programs. Secondly, the tool iteratively improves on previously generated candidates. If a candidate program meets the formal specification, then we are sure the program is correct. We evaluate VeCoGen on 15 problems presented in Codeforces competitions. On these problems, VeCoGen solves 13 problems. This work shows the potential of combining LLMs with formal verification to automate program generation.
- Abstract（参考訳）: LLM(Large Language Models)は、コード生成において印象的な能力を示していますが、多くの場合、意図した振る舞いから欠陥や逸脱したプログラムを生成し、安全クリティカルなアプリケーションに対する適合性を制限します。
この制限に対処するために,LLMと形式検証を組み合わせた新しいツールであるVeCoGenを導入し,Cプログラムの自動生成について述べる。
VeCoGenは、ANSI/ISO C Specification Language (ACSL) の正式な仕様、自然言語仕様、およびプログラムの生成を試みるテストケースのセットを採っている。
このプログラム生成プロセスは2つのステップから構成される。
まず、VeCoGenは候補プログラムの初期セットを生成する。
第2に、このツールは、以前に生成された候補を反復的に改善する。
候補プログラムが正式な仕様を満たしている場合、そのプログラムが正しいことを確信する。
我々は,Codeforcesコンペティションで提示された15の問題についてVeCoGenを評価した。
これらの問題に関して、VeCoGenは13の問題を解決する。
本研究は,LSMと形式検証を組み合わせたプログラム生成の自動化の可能性を示す。
関連論文リスト
- Type-Constrained Code Generation with Language Models [51.03439021895432]
大規模言語モデル(LLM)はコードの形式的な側面をモデル化しないため、コンパイル不可能な出力を生成する。
本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。
提案手法は,コンパイルエラーを半分以上削減し,コード合成,翻訳,修復作業における機能的正しさを向上する。
論文 参考訳（メタデータ） (2025-04-12T15:03:00Z) - C*: Unifying Programming and Verification in C [15.531046191957529]
C* は C プログラミングのための言語設計の証明である。
プログラマが実装コードと並行して証明コードブロックを埋め込むことで、リアルタイムの検証を可能にする。
C* は C を共通言語として使用することで実装と証明コード開発を統合する。
論文 参考訳（メタデータ） (2025-04-03T03:22:22Z) - LLM Benchmarking with LLaMA2: Evaluating Code Development Performance Across Multiple Programming Languages [0.1906498126334485]
本稿では,Llama 2-70Bモデルがプログラミング言語で書かれた科学アプリケーションを自動化する能力について述べる。
コード、ドキュメンテーション、ユニットテストを生成するためのモデルの能力と、既存のコードをプログラミング言語間で翻訳する能力を評価します。
以上の結果から,Llama 2-70Bは,より単純な数値処理のために,構文的に正しい関数コードを生成することが多いが,より複雑で並列化された,あるいは分散計算ではかなりの困難に直面することが示唆された。
論文 参考訳（メタデータ） (2025-03-24T23:46:14Z) - Galápagos: Automated N-Version Programming with LLMs [10.573037638807024]
Gal'apagosは、大規模な言語モデルを使用してプログラムの変種を生成するツールである。
ガラパゴスは機能的に等価であることが証明されたプログラム変種を生成できることを示す。
Gal'apagosが生成した変種は、実際の誤コンパイルバグからCコードを保護することができることを実証する。
論文 参考訳（メタデータ） (2024-08-18T16:44:01Z) - NoviCode: Generating Programs from Natural Language Utterances by Novices [59.71218039095155]
初心者非プログラマによるAPIと自然言語記述を入力とする新しいNLプログラミングタスクであるNoviCodeを提示する。
我々は、NoviCodeがコード合成領域における挑戦的なタスクであることを示し、非技術的命令から複雑なコードを生成することは、現在のText-to-Codeパラダイムを超えている。
論文 参考訳（メタデータ） (2024-07-15T11:26:03Z) - Towards Large Language Model Aided Program Refinement [10.089955747110444]
プログラムの洗練には、正式なハイレベルな仕様文から実行可能なプログラムへの正当性保存の変換が含まれる。
大型言語モデル(LLM)は、非公式な自然言語仕様から自動コード生成を可能にする。
LLM4PRは,形式的プログラム改善手法と非公式なLCMベースの手法を組み合わせたツールである。
論文 参考訳（メタデータ） (2024-06-26T04:29:27Z) - Learning to Reason via Program Generation, Emulation, and Search [33.11955431589091]
言語モデル(LM)によるプログラム合成は、多くの推論能力を解放した。
すべての推論タスクは、コードとして容易に表現できるわけではない。例えば、常識的推論、道徳的意思決定、皮肉な理解を含むタスクである。
我々は,プログラム合成スキルをこのようなタスクに拡張するために,コード生成とエミュレートされた実行(CoGEX)を提案する。
論文 参考訳（メタデータ） (2024-05-25T19:40:50Z) - Python Code Generation by Asking Clarification Questions [57.63906360576212]
本稿では,この課題に対して,より斬新で現実的なセットアップを導入する。
我々は、自然言語記述の過小評価は、明確化を問うことで解決できると仮定する。
我々は、生成した合成明確化質問と回答を含む自然言語記述とコードのペアを含む、CodeClarQAという新しいデータセットを収集し、導入する。
論文 参考訳（メタデータ） (2022-12-19T22:08:36Z) - CryptOpt: Verified Compilation with Randomized Program Search for
Cryptographic Primitives (full version) [12.790826917588575]
暗号は例外であり、多くのパフォーマンスクリティカルなルーチンがアセンブリで直接書かれてきた。
CryptOptは、GCCやClangが生成するものよりもはるかに高速なアセンブリコードに高レベルの暗号関数プログラムを専門とする、最初のコンパイルパイプラインである。
形式検証の面では、FiatOptフレームワーク(関数型プログラムをCライクなIRコードに変換する)に接続し、新たに公式に認証されたプログラム等価チェッカーで拡張する。
論文 参考訳（メタデータ） (2022-11-19T11:07:39Z) - Piloting Copilot and Codex: Hot Temperature, Cold Prompts, or Black
Magic? [5.714553194279462]
2つの言語モデルの様々な入力パラメータについて検討し、これらの入力パラメータの変動が生成したプログラムの品質に重大な影響を及ぼすかどうかを理解するために研究を行う。
その結果,入力パラメータの変動は言語モデルの性能を著しく向上させることができることがわかった。
論文 参考訳（メタデータ） (2022-10-26T13:28:14Z) - Fault-Aware Neural Code Rankers [64.41888054066861]
サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。
我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
論文 参考訳（メタデータ） (2022-06-04T22:01:05Z) - Natural Language to Code Translation with Execution [82.52142893010563]
実行結果-プログラム選択のための最小ベイズリスク復号化。
そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
論文 参考訳（メタデータ） (2022-04-25T06:06:08Z) - A Conversational Paradigm for Program Synthesis [110.94409515865867]
本稿では,大規模言語モデルを用いた対話型プログラム合成手法を提案する。
私たちは、自然言語とプログラミング言語のデータに基づいて、CodeGenと呼ばれる大規模な言語モデルのファミリーを訓練します。
本研究は,会話能力の出現と,提案した会話プログラム合成パラダイムの有効性を示すものである。
論文 参考訳（メタデータ） (2022-03-25T06:55:15Z) - AVATAR: A Parallel Corpus for Java-Python Program Translation [77.86173793901139]
プログラム翻訳とは、ある言語から別の言語へソースコードを移行することを指す。
AVATARは9,515のプログラミング問題とそのソリューションをJavaとPythonという2つの人気のある言語で記述したものです。
論文 参考訳（メタデータ） (2021-08-26T05:44:20Z) - Measuring Coding Challenge Competence With APPS [54.22600767666257]
コード生成のベンチマークであるAPPSを紹介する。
私たちのベンチマークには1万の問題が含まれています。
GPT-Neoのような最近のモデルでは、導入問題のテストケースの約15%をパスできる。
論文 参考訳（メタデータ） (2021-05-20T17:58:42Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。