論文の概要: VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search

• arxiv url: http://arxiv.org/abs/2402.08147v2
• Date: Fri, 24 May 2024 14:51:14 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-27 23:07:01.657845
• Title: VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search
• Title（参考訳）: VerMCTS: 検証器, 大規模言語モデル, 木探索を用いたマルチステッププログラムの合成
• Authors: David Brandfonbrener, Simon Henniger, Sibi Raja, Tarun Prasad, Chloe Loughridge, Federico Cassano, Sabrina Ruixin Hu, Jianang Yang, William E. Byrd, Robert Zinkov, Nada Amin,
• Abstract要約: 大型言語モデル(LLM)は有用なコードを生成することができるが、しばしばそれらが生成するコードは信頼できない。 本稿では,Dafny と Coq で検証プログラムを生成することで,この問題を解決するための VerMCTS を提案する。
• 参考スコア（独自算出の注目度）: 5.389248707675898
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large Language Models (LLMs) can generate useful code, but often the code they generate cannot be trusted to be sound. In this paper, we present VerMCTS, an approach to begin to resolve this issue by generating verified programs in Dafny and Coq. VerMCTS uses a logical verifier in concert with an LLM to guide a modified Monte Carlo Tree Search (MCTS). This approach leverages the verifier to gain intermediate feedback inside the search algorithm by checking partial programs at each step to estimate an upper bound on the value function. To measure the performance of VerMCTS, we develop a new suite of multi-step verified programming problems in Dafny and Coq. In terms of pass@T, a new metric which computes the pass rate given a budget of T tokens sampled from the LLM, VerMCTS leads to more than a 30% absolute increase in average pass@5000 across the suite over repeated sampling from the base language model. Our code and benchmarks are available at https://github.com/namin/llm-verified-with-monte-carlo-tree-search .
• Abstract（参考訳）: 大型言語モデル(LLM)は有用なコードを生成することができるが、しばしばそれらが生成するコードは信頼できない。 本稿では,Dafny と Coq で検証プログラムを生成することで,この問題を解決するための VerMCTS を提案する。 VerMCTS は LLM と協調してモンテカルロ木探索 (MCTS) を誘導する論理検証器を使用する。 提案手法では,各ステップで部分的なプログラムをチェックし,値関数上の上限を推定することにより,検証値を利用して探索アルゴリズム内部の中間フィードバックを得る。 VerMCTSの性能を測定するため,Dafny と Coq のマルチステップ検証プログラム問題スイートを開発した。 LLMからサンプリングされたTトークンの予算が与えられたパスレートを計算する新しいメトリックであるpass@Tでは、VerMCTSはベース言語モデルからの繰り返しサンプリングよりも、スイート全体で平均パス@5000が30%以上増加します。 私たちのコードとベンチマークはhttps://github.com/namin/llm-verified-with-monte-carlo-tree-searchで公開されています。

関連論文リスト

• Benchmarking Uncertainty Quantification Methods for Large Language Models with LM-Polygraph [83.90988015005934]
  不確実性定量化(英: Uncertainty Quantification、UQ)は、機械学習(ML)アプリケーションにおいて重要なコンポーネントである。 最新のUQベースラインの集合を実装した新しいベンチマークを導入する。 我々は、9つのタスクにわたるUQと正規化技術に関する大規模な実証的研究を行い、最も有望なアプローチを特定した。
  論文  参考訳（メタデータ） (2024-06-21T20:06:31Z)
• Validating LLM-Generated Programs with Metamorphic Prompt Testing [8.785973653167112]
  大規模言語モデル(LLM)は、ソフトウェア開発ライフサイクルにますます統合されています。 本稿では,これらの課題に対処するため,メタモルフィック・プロンプト・テストと呼ばれる新しい手法を提案する。 我々のHumanEvalに対する評価は,GPT-4が生成する誤プログラムの75%を,偽陽性率8.6%で検出できることを示す。
  論文  参考訳（メタデータ） (2024-06-11T00:40:17Z)
• Recursive Speculative Decoding: Accelerating LLM Inference via Sampling Without Replacement [11.91629418177851]
  投機的復号法(英: Speculative decoding)は、大規模言語モデルの推論・加速度法である。 近年の作業では、草稿の伐採によってこの方法が進歩している。 再帰的投機的復号法(Recursive Speculative Decoding:RSD)を提案する。
  論文  参考訳（メタデータ） (2024-02-21T22:57:49Z)
• Which Syntactic Capabilities Are Statistically Learned by Masked Language Models for Code? [51.29970742152668]
  精度に基づく測定に依存することで、モデルの能力が過大評価される可能性があることを強調する。 これらの問題に対処するために,SyntaxEval in Syntactic Capabilitiesというテクニックを導入する。
  論文  参考訳（メタデータ） (2024-01-03T02:44:02Z)
• Bridging Code Semantic and LLMs: Semantic Chain-of-Thought Prompting for Code Generation [22.219645213202178]
  本稿では,SeCoT というコードの意味情報を抽出する "Semantic Chain-of-Thought" 手法を提案する。 本研究では,SeCoTが最先端の性能を実現し,大規模モデルやコード生成の可能性を大幅に向上させることを示す。
  論文  参考訳（メタデータ） (2023-10-16T05:09:58Z)
• Sequential Monte Carlo Steering of Large Language Models using Probabilistic Programs [46.721838623748816]
  本研究では,大規模言語モデルの出力に対する構文的制約と意味的制約を強制する新しい推論時手法を提案する。 主要なアイデアは、言語生成タスクを離散確率列モデルのクラスにおける後部推論問題として指定することである。 ビームサーチと同様の計算コストのために、SMCは多様なタスクを解決するためにLSMを操ることができる。
  論文  参考訳（メタデータ） (2023-06-05T17:55:05Z)
• Coarse-Tuning Models of Code with Reinforcement Learning Feedback [0.0]
  コード上で事前訓練されたLarge Language Models (LLM) が、プログラム合成の主流のアプローチとして登場した。 コードの品質を評価する接地関数からのフィードバックを用いて、強化学習により事前学習したLLMをさらに訓練するRCCFを提案する。
  論文  参考訳（メタデータ） (2023-05-25T22:09:08Z)
• ALGO: Synthesizing Algorithmic Programs with LLM-Generated Oracle Verifiers [60.6418431624873]
  大きな言語モデル(LLM)は、機能記述からコードを実装するのに優れているが、アルゴリズムの問題に悩まされている。 我々は,アルゴリズムプログラムを LLM 生成 Oracle で合成するフレームワーク ALGO を提案し,その生成をガイドし,その正確性を検証する。 実験の結果,ALGOを装着すると,Codexモデルよりも8倍,CodeTよりも2.6倍の1サブミッションパス率が得られることがわかった。
  論文  参考訳（メタデータ） (2023-05-24T00:10:15Z)
• Inference with Reference: Lossless Acceleration of Large Language Models [97.04200102556551]
  LLMAは、参照によるLarge Language Model (LLM)推論を高速化するアクセラレータである。 LLMによる復号結果と実世界の多くのシナリオで利用できる参照との間には、多くの同一のテキストが存在していることが観察の動機となっている。
  論文  参考訳（メタデータ） (2023-04-10T09:55:14Z)
• 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)

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

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