llm-verified-with-monte-carlo-tree-search

项目介绍：基于蒙特卡洛树搜索验证的LLM项目

llm-verified-with-monte-carlo-tree-search项目是一个创新的原型，它结合了巨大语言模型（LLM）和蒙特卡洛树搜索（MCTS）用于生成经过验证的代码。通过这种方法，该项目探索可能的程序生成空间，并在每一步都通过调用验证器来确保生成路径的正确性。

项目背景

在使用LLM生成代码时，一个主要挑战是确保每行代码都符合预期的功能和逻辑。为了解决这个问题，该项目引入了MCTS。通过不断探测不同的代码生成路径并让验证器进行检查，它能够确保代码在每一步都向着正确的方向发展。

使用技术

该项目支持多种编程语言和验证工具，包括Dafny, Coq, Lean, Scala和Rust。这些工具确保生成的代码不仅合乎语法，而且符合逻辑验证规范。

项目特点

• 多语言支持：可在多个编程语言中生成和验证代码。
• 弱模型竞争力：即使是语言掌握较差的模型，也能够通过这一框架参与竞争。
• 日志记录：项目在log目录中记录了示例运行的日志，可以在日志结束部分查看最优解。

安装与运行

环境要求

该项目需要GPU支持，并在多GPU设备（如两个NVIDIA A100）上进行过测试。以下是安装和运行步骤：

1. 克隆仓库：

   git clone --recurse-submodules https://github.com/namin/llm-verified-with-monte-carlo-tree-search.git

2. 环境设置：

   conda create --name llm-verified python=3.10
   conda activate llm-verified
   pip install -r requirements.txt
   huggingface-cli login

3. 执行实验： 使用默认配置运行实验：

   python run.py

4. 参数配置： 可以通过cmdline.py查看可用参数并进行配置，例如切换验证语言：

   python run.py --language Coq

特殊运行模式

• 交互模式：与用户交互的运行：

  python run_user.py

• 验证反馈模式：包含验证信息反馈的运行：

  python run_verifier_feedback.py

• 多路径优化：为生成的代码选择多样化路径：

  python run_diversity.py

创新贡献

通过结合LLM和MCTS，该项目创造了一种新的代码生成与验证机制，不仅提高了生成程序的质量，而且让各种规模的模型都能参与到高质量代码生成的竞争中。这不仅提升了模型的实际应用能力，还为程序合成研究提供了新的思路。

技术详解

项目采用了多种技术方法，其中包括交互式验证、PPO训练器以及DPO训练器等。这些方法可以灵活适应不同实验需求，并针对目标提供有效的解决方案。

结论

llm-verified-with-monte-carlo-tree-search项目通过验证器、巨大语言模型和树搜索的深度结合，为代码生成过程带来了革命性的改进。通过这种途径，它不仅确保了生成代码的正确性以及可靠性，还为未来的代码自动生成研究拓宽了可能性。

对于对该项目感兴趣的技术人员或研究者，可以根据需求选择不同运行配置来尝试更多可能性。该项目也欢迎不同背景的开发者前来参与贡献，共同推进程序合成领域的研究。