論文の概要: Verified Multi-Step Synthesis using Large Language Models and Monte
Carlo Tree Search
- arxiv url: http://arxiv.org/abs/2402.08147v1
- Date: Tue, 13 Feb 2024 00:55:14 GMT
- ステータス: 処理完了
- システム内更新日: 2024-02-14 16:53:47.379390
- Title: Verified Multi-Step Synthesis using Large Language Models and Monte
Carlo Tree Search
- Title(参考訳): 大規模言語モデルとモンテカルロ木探索を用いたマルチステップ合成の検証
- Authors: David Brandfonbrener, Sibi Raja, Tarun Prasad, Chloe Loughridge,
Jianang Yang, Simon Henniger, William E. Byrd, Robert Zinkov, Nada Amin
- Abstract要約: 本稿では,モンテカルロ木探索(MCTS)を用いて大規模言語モデル(LLM)を誘導し,Dafny,Lean,Coqの検証プログラムを生成する手法を提案する。
提案手法はVMCTSと呼ばれ,各ステップで部分的なプログラムをチェックすることにより,探索アルゴリズム内の検証手法を活用する。
検証済みの5つの問題に対して,VMCTSでは,1時間で再サンプリングした場合でも,基本モデルでは解けない4つの問題に対して,VMCTSは6分以内で解けることがわかった。
- 参考スコア(独自算出の注目度): 5.549780624637388
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present an approach using Monte Carlo Tree Search (MCTS) to guide Large
Language Models (LLMs) to generate verified programs in Dafny, Lean and Coq.
Our method, which we call VMCTS, leverages the verifier inside the search
algorithm by checking partial programs at each step. In combination with the
LLM prior, the verifier feedback raises the synthesis capabilities of open
source models. On a set of five verified programming problems, we find that in
four problems where the base model cannot solve the question even when
re-sampling solutions for one hour, VMCTS can solve the problems within 6
minutes. The base model with VMCTS is even competitive with ChatGPT4 augmented
with plugins and multiple re-tries on these problems. Our code and benchmarks
are available at
https://github.com/namin/llm-verified-with-monte-carlo-tree-search .
- Abstract(参考訳): 本稿では,モンテカルロ木探索(MCTS)を用いて大規模言語モデル(LLM)を誘導し,Dafny,Lean,Coqの検証プログラムを生成する手法を提案する。
提案手法はvmctsと呼ばれ,各ステップで部分プログラムをチェックすることにより,探索アルゴリズム内の検証器を活用する。
llmの事前設定と組み合わせることで、検証者のフィードバックはオープンソースモデルの合成能力を高める。
5つの検証済みプログラミング問題の組において、ベースモデルが1時間ソリューションを再サンプリングしても問題を解くことができない4つの問題において、vmctは6分以内に問題を解決できることがわかった。
VMCTSのベースモデルは、これらの問題に対するプラグインと複数の再試行を備えたChatGPT4と競合する。
私たちのコードとベンチマークは、https://github.com/namin/llm-verified-with-monte-carlo-tree-searchで利用可能です。
関連論文リスト
- Exploring Combinatorial Problem Solving with Large Language Models: A Case Study on the Travelling Salesman Problem Using GPT-3.5 Turbo [4.543552585804991]
旅行セールスマン問題(TSP)の解決に向けた大規模言語モデル(LLM)の可能性について検討する。
GPT-3.5 Turboを微調整して特定の問題サイズを解き、様々なインスタンスサイズを用いてテストした。
微調整されたモデルでは、トレーニングインスタンスと大きさが同じ問題に対して有望な性能を示し、より大きな問題に対してよく一般化された。
論文 参考訳(メタデータ) (2024-05-03T10:54:14Z) - MetaCheckGPT -- A Multi-task Hallucination Detector Using LLM Uncertainty and Meta-models [8.322071110929338]
本稿では,モデル非依存トラックとモデル認識トラックの2つのサブタスクにおいて,勝利解をそれぞれ1位と2位にランク付けした。
モデル評価と統合のためのLCMのメタレグレクタフレームワークを提案する。
論文 参考訳(メタデータ) (2024-04-10T11:56:01Z) - $\texttt{LM}^\texttt{2}$: A Simple Society of Language Models Solves Complex Reasoning [22.810441504080703]
大規模言語モデル(LLMS)は複雑で多段階の推論をしばしば失う。
本稿では,これらの課題に対処するためにLM2を提案する。
LM2は分解、解法、検証を3つの異なる言語モデルにモジュール化する。
論文 参考訳(メタデータ) (2024-04-02T19:23:10Z) - Hint-before-Solving Prompting: Guiding LLMs to Effectively Utilize
Encoded Knowledge [85.17343729885003]
我々は,Hint-before-Solving Prompting (HSP)を導入し,その問題を解くためのヒントを生成する。
HSPは推論タスクの精度を効果的に向上させることができる。
我々はHSPと細調整されたLlemma-7Bに基づいてHSPMATHデータセットを構築し、64.3精度を達成した。
論文 参考訳(メタデータ) (2024-02-22T05:58:03Z) - MT-Eval: A Multi-Turn Capabilities Evaluation Benchmark for Large
Language Models [70.92847554971065]
MT-Evalは,マルチターン対話能力を評価するための総合的なベンチマークである。
人間のLLM会話を解析することにより,インタラクションパターンを,再現,拡張,洗練,フォローアップの4つのタイプに分類する。
11個の有名なLCMを評価したところ、クローズドソースモデルは一般的にオープンソースモデルを上回るが、特定のタスクにおいて特定のオープンソースモデルの方がGPT-3.5-Turboを上回っていることがわかった。
論文 参考訳(メタデータ) (2024-01-30T04:50:28Z) - TAT-LLM: A Specialized Language Model for Discrete Reasoning over
Tabular and Textual Data [77.66158066013924]
我々は,言語モデル(LLM)の驚くべきパワーを活用して課題を解決することを検討する。
LLaMA2を微調整し,既存のエキスパートアノテートデータセットから自動生成したトレーニングデータを用いてTAT-LLM言語モデルを開発する。
論文 参考訳(メタデータ) (2024-01-24T04:28:50Z) - Sequential Monte Carlo Steering of Large Language Models using
Probabilistic Programs [46.721838623748816]
本研究では,大規模言語モデルの出力に対する構文的制約と意味的制約を強制する新しい推論時手法を提案する。
主要なアイデアは、言語生成タスクを離散確率列モデルのクラスにおける後部推論問題として指定することである。
ビームサーチと同様の計算コストのために、SMCは多様なタスクを解決するためにLSMを操ることができる。
論文 参考訳(メタデータ) (2023-06-05T17:55:05Z) - 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) - Learning Hidden Markov Models Using Conditional Samples [72.20944611510198]
本稿では,隠れマルコフモデル(HMM)の学習における計算複雑性について述べる。
本稿では,HMMの条件分布からサンプルを問合せする対話型アクセスモデルを提案する。
具体的には、正確な条件付き確率に対するクエリアクセスが可能な設定において、HMMを学習するための効率的なアルゴリズムを得る。
論文 参考訳(メタデータ) (2023-02-28T16:53:41Z) - Monte Carlo Tree Search: A Review of Recent Modifications and
Applications [0.17205106391379024]
モンテカルロツリー検索(MCTS)は、ゲームプレイボットを設計したり、連続的な決定問題を解決するための強力なアプローチです。
この方法は、探索と搾取のバランスをとるインテリジェントな木探索に依存している。
しかし、この方法はより複雑なゲームでは最先端の技術となっている。
論文 参考訳(メタデータ) (2021-03-08T17:44:15Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。