論文の概要: 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 15:21:58.512285
• 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:
• 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と形式検証を組み合わせたプログラム生成の自動化の可能性を示す。

関連論文リスト

• AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement [25.80131224070207]
  生成したコードが正しいことを数学的に保証するために,形式検証を利用することを目標としている。 LLMによる正式な認証コードの生成は、トレーニングデータの不足と、形式的な証明の複雑さによって妨げられる。 我々は、公式に認証されたコード生成をブートストラップする自己改善フレームワークであるAlphaVerusを紹介した。
  論文  参考訳（メタデータ） (2024-12-09T03:22:35Z)
• Galapagos: Automated N-Version Programming with LLMs [10.573037638807024]
  大規模言語モデルを用いたプログラム変種の自動生成を提案する。 プログラムの変種を生成するツールであるGal'apagosを設計、開発、評価する。 我々は現実世界のCコードのN-Versionコンポーネントを作成することでGal'apagosを評価する。
  論文  参考訳（メタデータ） (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)
• 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)
• 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)
• NAPG: Non-Autoregressive Program Generation for Hybrid Tabular-Textual Question Answering [52.10214317661547]
  現在の数値推論法はプログラムシーケンスを自己回帰的にデコードする。 プログラム生成の精度は、デコードステップがエラー伝搬によって展開されるにつれて急激に低下する。 本稿では,非自己回帰型プログラム生成フレームワークを提案する。
  論文  参考訳（メタデータ） (2022-11-07T11:25:21Z)
• 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)
• Measuring Coding Challenge Competence With APPS [54.22600767666257]
  コード生成のベンチマークであるAPPSを紹介する。 私たちのベンチマークには1万の問題が含まれています。 GPT-Neoのような最近のモデルでは、導入問題のテストケースの約15%をパスできる。
  論文  参考訳（メタデータ） (2021-05-20T17:58:42Z)

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

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