論文の概要: AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement

• arxiv url: http://arxiv.org/abs/2412.06176v1
• Date: Mon, 09 Dec 2024 03:22:35 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-10 14:57:18.568006
• Title: AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement
• Title（参考訳）: AlphaVerus: 自己改善翻訳とツリーファインメントによる形式的検証コード生成のブートストラップ
• Authors: Pranjal Aggarwal, Bryan Parno, Sean Welleck,
• Abstract要約: 生成したコードが正しいことを数学的に保証するために,形式検証を利用することを目標としている。 LLMによる正式な認証コードの生成は、トレーニングデータの不足と、形式的な証明の複雑さによって妨げられる。 我々は、公式に認証されたコード生成をブートストラップする自己改善フレームワークであるAlphaVerusを紹介した。
• 参考スコア（独自算出の注目度）: 25.80131224070207
• License:
• Abstract: Automated code generation with large language models has gained significant traction, but there remains no guarantee on the correctness of generated code. We aim to use formal verification to provide mathematical guarantees that the generated code is correct. However, generating formally verified code with LLMs is hindered by the scarcity of training data and the complexity of formal proofs. To tackle this challenge, we introduce AlphaVerus, a self-improving framework that bootstraps formally verified code generation by iteratively translating programs from a higher-resource language and leveraging feedback from a verifier. AlphaVerus operates in three phases: exploration of candidate translations, Treefinement -- a novel tree search algorithm for program refinement using verifier feedback, and filtering misaligned specifications and programs to prevent reward hacking. Through this iterative process, AlphaVerus enables a LLaMA-3.1-70B model to generate verified code without human intervention or model finetuning. AlphaVerus shows an ability to generate formally verified solutions for HumanEval and MBPP, laying the groundwork for truly trustworthy code-generation agents.
• Abstract（参考訳）: 大きな言語モデルによる自動コード生成は大きな注目を集めているが、生成したコードの正確性については保証されていない。 生成したコードが正しいことを数学的に保証するために,形式検証を利用することを目標としている。 しかし、LLMによる形式的検証コードの生成は、トレーニングデータの不足と形式的証明の複雑さによって妨げられる。 この課題に対処するために、我々はAlphaVerusという自己改善フレームワークを紹介した。このフレームワークは、高いソース言語からプログラムを反復的に翻訳し、検証者からのフィードバックを活用することで、公式に検証されたコード生成をブートストラップする。 AlphaVerusは3つのフェーズで運用されている: 候補翻訳の探索、Treefinement -- バリデーションフィードバックを使ったプログラムの洗練のための新しいツリー検索アルゴリズム、報酬のハッキングを防ぐためのミスマッチした仕様とプログラムのフィルタリング。 この反復的なプロセスを通じて、AlphaVerusはLLaMA-3.1-70Bモデルで人間の介入やモデルの微調整なしに検証コードを生成することができる。 AlphaVerusは、HumanEvalとMBPPの正式な検証されたソリューションを生成する能力を示し、真に信頼できるコード生成エージェントの基礎を築いた。

関連論文リスト

• From Scientific Texts to Verifiable Code: Automating the Process with Transformers [2.536225150399618]
  トランスフォーマーは 研究論文を読めます 正式な証明を持つアルゴリズムを 提案し これらの証明を 検証可能なコードに翻訳します このアプローチは形式的検証の障壁を大幅に減らすことができると我々は主張する。
  論文  参考訳（メタデータ） (2025-01-09T14:03:35Z)
• CodeSift: An LLM-Based Reference-Less Framework for Automatic Code Validation [3.22798929957223]
  大規模言語モデル(LLM)はコード生成を大いに促進してきたが、生成されたコードの機能的正確性を保証することは依然として課題である。 従来のバリデーション手法は、多くの場合、大量のコードに対して時間がかかり、エラーが発生し、実用的ではない。 コード検証のファーストラインフィルタとしてLLMを活用する新しいフレームワークであるCodeSiftを紹介します。
  論文  参考訳（メタデータ） (2024-08-28T08:32:21Z)
• Understanding Defects in Generated Codes by Language Models [0.669087470775851]
  本研究では,大規模言語モデルによって生成されたコードスニペットの367の欠陥を分類,解析する。 エラーカテゴリは、LLMが頻繁に失敗する重要な領域を示し、目標とする改善の必要性を強調している。 本稿では,スクラッチパッド・プロンプト・プログラム・オブ・ソート・プロンプト・チェーン・オブ・ソート・プロンプト・チェーン・オブ・ソート・プロンプト・ストラクテッド・オブ・ソート・プロンプト・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・プログラム・オブ・オブ・ソート・プロンプト・プロンプト・アンド・ストラクテッド・オブ・フォーンティング(Structued Chain-of-Thought Prompting)の5つの迅速な技術技術
  論文  参考訳（メタデータ） (2024-08-23T21:10:09Z)
• CodeRAG-Bench: Can Retrieval Augment Code Generation? [78.37076502395699]
  検索拡張生成を用いたコード生成の系統的,大規模な解析を行う。 まず、コード生成タスクの3つのカテゴリを含む総合的な評価ベンチマークであるCodeRAG-Benchをキュレートする。 CodeRAG-Bench上のトップパフォーマンスモデルについて、1つまたは複数のソースから検索したコンテキストを提供することにより検討する。
  論文  参考訳（メタデータ） (2024-06-20T16:59:52Z)
• Decoding at the Speed of Thought: Harnessing Parallel Decoding of Lexical Units for LLMs [57.27982780697922]
  大規模言語モデルは、自然言語の理解と生成において例外的な能力を示した。 しかし、それらの生成速度は、その復号過程の本質的にシーケンシャルな性質によって制限される。 本稿では,データ駆動方式で実装された新しいデコーディング手法であるLexical Unit Decodingを紹介する。
  論文  参考訳（メタデータ） (2024-05-24T04:35:13Z)
• CodeIP: A Grammar-Guided Multi-Bit Watermark for Large Language Models of Code [56.019447113206006]
  大規模言語モデル(LLM)はコード生成において顕著な進歩を遂げた。 CodeIPは、新しいマルチビット透かし技術で、出所の詳細を保持するために追加情報を挿入する。 5つのプログラミング言語にまたがる実世界のデータセットで実施された実験は、CodeIPの有効性を実証している。
  論文  参考訳（メタデータ） (2024-04-24T04:25:04Z)
• StepCoder: Improve Code Generation with Reinforcement Learning from Compiler Feedback [58.20547418182074]
  2つの主要コンポーネントからなるコード生成の新しいフレームワークであるStepCoderを紹介します。 CCCSは、長いシーケンスのコード生成タスクをCurriculum of Code Completion Subtaskに分割することで、探索課題に対処する。 FGOは、未実行のコードセグメントをマスクすることでのみモデルを最適化し、Fine-Grained Optimizationを提供する。 提案手法は,出力空間を探索し,対応するベンチマークにおいて最先端の手法より優れた性能を発揮する。
  論文  参考訳（メタデータ） (2024-02-02T13:14:31Z)
• Rewriting the Code: A Simple Method for Large Language Model Augmented Code Search [7.822427053078387]
  Generation-Augmented Retrieval (GAR)フレームワークは、クエリを拡張するための例のコードスニペットを生成する。 本稿では、forスタイルの正規化内でコード(ReCo)を書き換える、シンプルで効果的な方法を提案する。 コードスタイル類似度(Code Style similarity)は、コード内のスタイリスティック類似度を定量化するための最初のメートル法である。
  論文  参考訳（メタデータ） (2024-01-09T12:12:50Z)
• 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)
• ReCode: Robustness Evaluation of Code Generation Models [90.10436771217243]
  コード生成モデルのための総合的ロバストネス評価ベンチマークであるReCodeを提案する。 ドクストリング、関数と変数名、コード構文、コードフォーマットのコードに特化して、30以上の変換をカスタマイズします。 ヒトのアノテータでは、摂動プロンプトの90%以上が本来のプロンプトの意味を変えていないことが確認された。
  論文  参考訳（メタデータ） (2022-12-20T14:11:31Z)

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

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