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

• arxiv url: http://arxiv.org/abs/2310.17807v4
• Date: Sat, 16 Nov 2024 21:57:49 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-19 14:31:38.132035
• Title: Clover: Closed-Loop Verifiable Code Generation
• Title（参考訳）: Clover: クローズドループで検証可能なコード生成
• Authors: Chuyue Sun, Ying Sheng, Oded Padon, Clark Barrett,
• Abstract要約: 整合性チェックを使用して、不正なコードに対して強力なフィルタを提供するCloverパラダイムを導入します。 Cloverは、コード、ドキュストリング、フォーマルアノテーション間の一貫性チェックを実行する。 クローバーはまた、既存の人書きデータセットMBPP-DFY-50で6つの誤ったプログラムを発見した。
• 参考スコア（独自算出の注目度）: 2.5369596232063896
• License:
• 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 undesirable outcomes. In this paper, we introduce a new approach for addressing this challenge: the Clover paradigm, short for Closed-Loop Verifiable Code Generation, which uses consistency checking to provide a strong filter for incorrect code. Clover 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 performance 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 adversarial incorrect ones (no false positives). Clover also discovered 6 incorrect programs in the existing human-written dataset MBPP-DFY-50.
• Abstract（参考訳）: コード生成に大規模言語モデルを使用することは、ソフトウェア開発の急速な増加傾向である。 しかし、生成されたコードの正確性を保証する効果的な方法がなければ、この傾向は望ましくない結果をもたらす可能性がある。 本稿では,この課題に対処する新しいアプローチを提案する。Cloverパラダイムは,整合性チェックを用いて不正コードに対する強力なフィルタを提供するClover-Loop Verifiable Code Generationの略である。 Cloverは、コード、ドキュストリング、フォーマルアノテーション間の一貫性チェックを実行する。 このチェッカーは,形式検証ツールと大規模言語モデルの新たな統合によって実装されている。 我々はCloverが整合性チェックに有効であるべきだという私たちの主張を支持する理論的分析を提供する。 また,手書きのデータセット(CloverBench)において,注釈付きDafnyプログラムを教科書レベルでの難易度で解析した。 実験結果は、このデータセットについて示す。 一 LLM は、形式仕様を自動生成するのに適当に成功し、 (i) 整合性チェッカーは, 正のインスタンスに対して有望な受け入れ率(最大87%)を達成し, 逆の不正なインスタンスに対する耐性をゼロに維持する(偽陽性ではない)。 クローバーはまた、既存の人書きデータセットMBPP-DFY-50で6つの誤ったプログラムを発見した。

関連論文リスト

• 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)

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

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