論文の概要: 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つの誤ったプログラムを発見した。
関連論文リスト
- Distribution Learning with Valid Outputs Beyond the Worst-Case [25.788559173418363]
妥当性に制約のある分布学習は、学習された分布が、空間の無効な部分において、その質量の確率的に小さな部分を持つことを要求することによって、この問題に対処しようとする。
データ分散がモデルクラスに置かれ、ログロスが最小化されると、妥当性を保証するために必要なサンプルの数は、妥当性要求に弱いことが示される。
論文 参考訳（メタデータ） (2024-10-21T17:56:09Z) - Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。
LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。
本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
論文 参考訳（メタデータ） (2024-10-05T05:21:48Z) - Understanding Defects in Generated Codes by Language Models [0.669087470775851]
本研究では,大規模言語モデルによって生成されたコードスニペットの367の欠陥を分類,解析する。
エラーカテゴリは、LLMが頻繁に失敗する重要な領域を示し、目標とする改善の必要性を強調している。
本稿では,スクラッチパッド・プロンプト・プログラム・オブ・ソート・プロンプト・チェーン・オブ・ソート・プロンプト・チェーン・オブ・ソート・プロンプト・ストラクテッド・オブ・ソート・プロンプト・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・オブ・ソート・プロンプト・プログラム・オブ・ソート・プロンプト・プログラム・オブ・オブ・ソート・プロンプト・プロンプト・アンド・ストラクテッド・オブ・フォーンティング(Structued Chain-of-Thought Prompting)の5つの迅速な技術技術
論文 参考訳（メタデータ） (2024-08-23T21:10:09Z) - LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
本研究では,自然言語フィードバック型検証器Math-Minosを提案する。
実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
論文 参考訳（メタデータ） (2024-06-20T06:42:27Z) - Block Verification Accelerates Speculative Decoding [23.764655044837113]
投機的復号法は高速モデルを用いて、ターゲットモデルによって並列に検証されるトークンのブロックをドラフトする。
以前の作業では、ドラフト検証は独立してトークン・バイ・トークンで行われる。
ブロック全体を共同で検証する単純なドラフト検証アルゴリズムであるBlock Verificationを提案する。
論文 参考訳（メタデータ） (2024-03-15T16:28:22Z) - GPT-HateCheck: Can LLMs Write Better Functional Tests for Hate Speech Detection? [50.53312866647302]
HateCheckは、合成データに対してきめ細かいモデル機能をテストするスイートである。
GPT-HateCheckは,スクラッチからより多彩で現実的な機能テストを生成するフレームワークである。
クラウドソースのアノテーションは、生成されたテストケースが高品質であることを示しています。
論文 参考訳（メタデータ） (2024-02-23T10:02:01Z) - Learning to Check: Unleashing Potentials for Self-Correction in Large Language Models [5.463333911506443]
我々は,タスクチェックのためのトレーニングデータを構築することで,大規模言語モデル(LLM)の自己チェック能力を向上させることを目指している。
ステップCoTチェック(Step CoT Check)と呼ばれる特殊なチェックフォーマットを提案する。
実験により、"Step CoT Check"フォーマットによる微調整により、LCMの自己チェックと自己補正能力が大幅に向上することが示された。
論文 参考訳（メタデータ） (2024-02-20T14:23:23Z) - 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) - Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。
オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。
予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文 参考訳（メタデータ） (2023-11-15T14:41:57Z) - WeCheck: Strong Factual Consistency Checker via Weakly Supervised
Learning [40.5830891229718]
本稿では,複数のリソースを集約して,正確かつ効率的な実測値(WeCheck)をトレーニングする,弱教師付きフレームワークを提案する。
様々なタスクに関する総合的な実験は、平均してTRUEベンチマークにおける従来の最先端手法よりも3.4%の絶対的な改善を実現するWeCheckの強い性能を示す。
論文 参考訳（メタデータ） (2022-12-20T08:04:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。