VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search

要約

大規模言語モデル (LLM) は有用なコードを生成できますが、多くの場合、生成されるコードが健全であるとは信頼できません。
このペーパーでは、Dafny と Coq で検証済みプログラムを生成することでこの問題の解決を開始するアプローチである VerMCTS を紹介します。
VerMCTS は、LLM と連携して論理検証器を使用して、修正されたモンテカルロ ツリー検索 (MCTS) をガイドします。
このアプローチでは、検証機能を活用して、各ステップで部分プログラムをチェックして値関数の上限を推定することにより、検索アルゴリズム内の中間フィードバックを取得します。
VerMCTS のパフォーマンスを測定するために、Dafny と Coq でマルチステップ検証済みプログラミング問題の新しいスイートを開発しました。
LLM からサンプリングされた T トークンのバジェットを考慮して合格率を計算する新しいメトリックである pass@T に関して、VerMCTS は、ベースからサンプリングを繰り返すことにより、スイート全体の平均 pass@5000 の絶対値 30% 以上の増加につながります。
言語モデル。
コードとベンチマークは https://github.com/namin/llm-verified-with-monte-carlo-tree-search で入手できます。

要約(オリジナル)

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 .

arxiv情報

提供元, 利用サービス

arxiv.jp, Google