Fugu-MT 論文翻訳(概要): Clover: Closed-Loop Verifiable Code Generation

論文の概要: Clover: Closed-Loop Verifiable Code Generation

arxiv url: http://arxiv.org/abs/2310.17807v3
Date: Mon, 3 Jun 2024 16:59:37 GMT
ステータス: 処理完了
システム内更新日: 2024-06-04 20:31:18.121017
Title: Clover: Closed-Loop Verifiable Code Generation
Title（参考訳）: Clover: クローズドループで検証可能なコード生成
Authors: Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett,
Abstract要約: 整合性チェックのよりアクセスしやすい問題に対する正当性チェックを削減できるCloverパラダイムを提案する。 Cloverの中核には、コード、ドキュストリング、フォーマルアノテーション間の一貫性チェックを実行するチェッカーがある。注釈付きDafnyプログラムを教科書の難易度で記述した手書きデータセットの有効性を実証的に検討した。
参考スコア（独自算出の注目度）: 2.5369596232063896
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: The use of large language models for code generation is a rapidly growing trend in software development. However, without effective methods for ensuring the correctness of generated code, this trend could lead to any number of undesirable outcomes. In this paper, we lay out a vision for addressing this challenge: the Clover paradigm, short for Closed-Loop Verifiable Code Generation, which reduces correctness checking to the more accessible problem of consistency checking. At the core of Clover lies a checker that performs consistency checks among code, docstrings, and formal annotations. The checker is implemented using a novel integration of formal verification tools and large language models. We provide a theoretical analysis to support our thesis that Clover should be effective at consistency checking. We also empirically investigate its feasibility on a hand-designed dataset (CloverBench) featuring annotated Dafny programs at a textbook level of difficulty. Experimental results show that for this dataset, (i) LLMs are reasonably successful at automatically generating formal specifications; and (ii) our consistency checker achieves a promising acceptance rate (up to 87%) for correct instances while maintaining zero tolerance for incorrect ones (no false positives).
Abstract（参考訳）: コード生成に大規模言語モデルを使用することは、ソフトウェア開発の急速な増加傾向である。しかし、生成されたコードの正確性を保証する効果的な方法がなければ、この傾向は望ましくない結果を何回も引き起こす可能性がある。本稿では,Cloverパラダイム(Closed-Loop Verifiable Code Generation)の略で,一貫性チェックのよりアクセスしやすい問題に対する正当性チェックの削減を図っている。 Cloverの中核には、コード、ドキュストリング、フォーマルアノテーション間の一貫性チェックを実行するチェッカーがある。このチェッカーは,形式検証ツールと大規模言語モデルの新たな統合によって実装されている。我々はCloverが整合性チェックに有効であるべきだという私たちの主張を支持する理論的分析を提供する。また,注記Dafnyプログラムを教科書の難易度で記述した手書きデータセット(CloverBench)の実現可能性についても実証的に検討した。実験結果から, このデータセットについて検討した。一 LLM は、形式仕様を自動生成するのに適当に成功し、 (i) 整合性チェッカーは, 正しいインスタンスに対して有望な受け入れ率(最大87%)を達成し, 不正なインスタンスに対する耐性をゼロに維持する(偽陽性は発生しない)。

関連論文リスト

Let the Code LLM Edit Itself When You Edit the Code [50.46536185784169]
underlinetextbfPositional textbfIntegrity textbfEncoding (PIE) PIEは、標準的な完全再計算手法に比べて計算オーバーヘッドを85%以上削減する。その結果、PIEは計算オーバーヘッドを標準の完全再計算手法に比べて85%以上削減することを示した。
論文参考訳（メタデータ） (2024-07-03T14:34:03Z)
Clover: Regressive Lightweight Speculative Decoding with Sequential Knowledge [24.203554078434365]
並列復号処理にシーケンシャルな知識を統合する新しい投機的復号アルゴリズムであるCloverを提案する。クローバーは、バイチュアン=スモールでは91%、バイチュアン=ラージュでは146%でベースラインを上回っている。
論文参考訳（メタデータ） (2024-05-01T00:46:22Z)
Fact Checking Beyond Training Set [64.88575826304024]
本稿では,レトリバーリーダが,あるドメインのラベル付きデータに基づいてトレーニングし,別のドメインで使用する場合,性能劣化に悩まされることを示す。本稿では,レトリバー成分を分散シフトに対して頑健にするための逆アルゴリズムを提案する。次に、これらのデータセットから8つの事実チェックシナリオを構築し、モデルと強力なベースラインモデルのセットを比較します。
論文参考訳（メタデータ） (2024-03-27T15:15:14Z)
Trained Without My Consent: Detecting Code Inclusion In Language Models Trained on Code [13.135962181354465]
コード監査は、開発済みのコードが標準、規制、著作権保護に準拠していることを保証する。ソフトウェア開発プロセスにおけるコーディングアシスタントとしての最近のLarge Language Models(LLM)の出現は、コード監査に新たな課題をもたらしている。 LLMのトレーニングデータセットにコードを含むことを検出するモデルに依存しない、解釈可能な方法であるTraWiCを提案する。
論文参考訳（メタデータ） (2024-02-14T16:41:35Z)
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文参考訳（メタデータ） (2024-02-14T05:57:58Z)
Deductive Closure Training of Language Models for Coherence, Accuracy, and Updatability [58.582216812183496]
言語モデル(LM)は、実際に正しいテキストを生成し、個々のクレームの真理値を推定することがある。現在のLMは誤った内容や非意味な内容を生成しており、編集や更新は困難である。本稿では,DCT(Deductive Closure Training)と呼ばれる手法を提案する。
論文参考訳（メタデータ） (2024-01-16T18:58:37Z)
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)
Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文参考訳（メタデータ） (2023-11-15T14:41:57Z)
Precise Zero-Shot Dense Retrieval without Relevance Labels [60.457378374671656]
仮説文書埋め込み(英: hypothetical Document Embeddings, HyDE)は、ゼロショット高密度検索システムである。我々は,HyDEが最先端の非教師付き高密度検索器であるContrieverを著しく上回っていることを示す。
論文参考訳（メタデータ） (2022-12-20T18:09:52Z)
WeCheck: Strong Factual Consistency Checker via Weakly Supervised Learning [40.5830891229718]
本稿では,複数のリソースを集約して,正確かつ効率的な実測値(WeCheck)をトレーニングする,弱教師付きフレームワークを提案する。様々なタスクに関する総合的な実験は、平均してTRUEベンチマークにおける従来の最先端手法よりも3.4%の絶対的な改善を実現するWeCheckの強い性能を示す。
論文参考訳（メタデータ） (2022-12-20T08:04:36Z)
Converge to the Truth: Factual Error Correction via Iterative Constrained Editing [30.740281040892086]
最小限の編集で事実誤り訂正(FEC)を行う新しい手法であるVENCEを提案する。 VENCEは、FEC問題を目標密度関数に対する反復サンプリング編集動作として定式化する。公開データセットでの実験では、VENCEは以前の最遠距離で監督された手法よりもよく測定されたSARIの基準を5.3(または11.8%の相対的な改善)改善している。
論文参考訳（メタデータ） (2022-11-22T10:03:13Z)

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

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