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

📄 arXiv: 2402.08147v2 📥 PDF

作者: David Brandfonbrener, Simon Henniger, Sibi Raja, Tarun Prasad, Chloe Loughridge, Federico Cassano, Sabrina Ruixin Hu, Jianang Yang, William E. Byrd, Robert Zinkov, Nada Amin

分类: cs.SE, cs.AI, cs.LG, cs.LO, cs.PL

发布日期: 2024-02-13 (更新: 2024-05-24)

🔗 代码/项目: GITHUB

💡 一句话要点

提出VerMCTS以解决大语言模型生成代码可信性问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大语言模型 代码生成 逻辑验证 蒙特卡洛树搜索 程序验证 自动化编程

📋 核心要点

  1. 现有的大语言模型生成的代码缺乏可信性，导致其在实际应用中的可靠性受到质疑。
  2. VerMCTS结合逻辑验证器与大语言模型，通过改进的蒙特卡洛树搜索方法，生成经过验证的程序。
  3. 实验结果显示，VerMCTS在pass@5000指标上相比基础模型有超过30%的提升，验证了其有效性。

📝 摘要（中文）

大语言模型（LLMs）能够生成有用的代码，但其生成的代码往往缺乏可信性。本文提出了一种名为VerMCTS的方法，通过结合逻辑验证器和大语言模型，利用改进的蒙特卡洛树搜索（MCTS）来生成经过验证的程序。VerMCTS在搜索算法中利用验证器提供的中间反馈，通过检查部分程序来估计价值函数的上界。为了评估VerMCTS的性能，研究者开发了一套新的多步骤验证编程问题。在pass@T这一新指标下，VerMCTS在多次从基础语言模型抽样的情况下，平均pass@5000的通过率提高了超过30%。

🔬 方法详解

问题定义：本文旨在解决大语言模型生成代码的可信性问题，现有方法往往无法保证生成代码的正确性和可靠性。

核心思路：VerMCTS通过结合逻辑验证器与大语言模型，利用验证器提供的反馈来指导蒙特卡洛树搜索，从而生成经过验证的程序。这样的设计能够在生成过程中实时评估代码的正确性。

技术框架：VerMCTS的整体架构包括三个主要模块：逻辑验证器、大语言模型和改进的蒙特卡洛树搜索。首先，逻辑验证器对生成的部分程序进行验证，提供反馈；然后，大语言模型生成代码；最后，蒙特卡洛树搜索利用反馈优化生成过程。

关键创新：VerMCTS的创新之处在于将逻辑验证器与蒙特卡洛树搜索相结合，利用中间反馈来提高生成程序的正确性。这一方法在生成过程中引入了动态验证机制，与传统的静态验证方法形成鲜明对比。

关键设计：在实现过程中，VerMCTS设置了特定的参数以平衡搜索深度与验证频率，同时采用了适应性损失函数来优化生成的程序质量。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，VerMCTS在pass@5000指标上相比基础语言模型的平均通过率提高了超过30%。这一显著提升验证了VerMCTS在生成经过验证的程序方面的有效性，展示了其在实际应用中的潜力。

🎯 应用场景

VerMCTS的研究成果在多个领域具有潜在应用价值，包括自动化编程、智能合约生成和软件验证等。通过提高生成代码的可信性，VerMCTS能够为开发者提供更可靠的工具，减少代码审查和调试的时间成本，推动智能编程技术的发展。

📄 摘要（原文）

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 .