Feb, 2024

基于大型语言模型和蒙特卡洛树搜索的多步骤合成验证

PDF
TL;DR使用蒙特卡洛树搜索指导大型语言模型生成在 Dafny、Lean 和 Coq 中验证的程序的方法，该方法称为 VMCTS，在组合 LLM 先验知识和验证器反馈的情况下，提高了开源模型的综合能力，在五个验证编程问题中，VMCTS 以 6 分钟内解决了四个问题，与具有插件和多次尝试的 ChatGPT4 在这些问题上具有竞争力。
monte carlo tree searchlarge language modelsverified programssynthesis capabilitieschatgpt4
发现论文，激发创造
  • 基于蒙特卡罗树搜索指导的大型语言模型生成代码世界模型

    通过利用蒙特卡洛树搜索策略（GIF-MCTS）进行生成、改进和修复，我们成功地解决了利用大型语言模型生成代码世界模型（Code World Models）的挑战，并且在多个基准测试中超越了其他方法，在模型为基础的强化学习方面取得了显著的样本效率和推理速度提升。

    May, 2024

  • LLM4PLC：工控系统中基于大型语言模型的可验证 PLC 编程

    提出 LLM4PLC 的用户引导迭代流程，通过用户反馈和外部验证工具来改善大型语言模型（LLM）生成的代码的可验证性，提高成功生成的比例并提高代码质量。

    Jan, 2024

  • 在 Rust 中利用大型语言模型进行自动证明合成

    基于大型语言模型（LLMs）和静态分析相结合，开发了一个基于 Rust 的形式验证框架 Verus 的原型。通过将验证任务分解为多个较小的任务，迭代地查询 GPT-4，并将其输出与轻量级静态分析相结合，这个原型显著减少了编写入门级证明代码的人力工作。

    Nov, 2023

  • Laurel：使用大型语言模型生成 Dafny 断言

    Laurel 是一种使用大型语言模型（LLMs）自动生成 Dafny 程序的辅助断言的工具，通过两种领域特定的提示技术，能够提高 LLMs 在此任务中的成功率，从而使 LLMs 成为进一步自动化实际程序验证的可用且经济实惠的工具。

    May, 2024

  • 蒙特卡洛思维搜索：大型语言模型在催化剂设计中进行复杂科学推理

    通过蒙特卡洛树搜索方法与科学推理，提出了一种新的驱动组合搜索的方法，可以增强科学家的推理和发现过程。

    Oct, 2023

  • 发挥每一步的价值：基于 LLM 的高质量 RTL 代码生成使用 MCTS

    通过引入蒙特卡罗树搜索，并将其与自动转换器解码算法相结合，以解决现有大型语言模型在寄存器传输级代码生成中遇到的问题，从而实现能够生成可编译、功能正确且功耗性能区域（PPA）优化的代码。经实证评估，我们的技术在 RTL 代码集上通过对细调的语言模型进行评估，相对于仅使用提示的方法，一直能够生成功能正确的代码，并有效解决了朴素大型语言模型的 PPA 非感知缺陷。对于由最先进的大型语言模型（16 位加法器）生成的最大设计，我们的技术可以在延迟面积乘积方面实现 31.8% 的改进。

    Feb, 2024

  • 大型语言模型能否玩游戏？一种自我对弈方法的案例研究

    结合蒙特卡洛树搜索和大型语言模型的创新方法可有效解决决策型游戏问题，提高大型语言模型的性能并处理蒙特卡洛树搜索无法应对的挑战。

    Mar, 2024

  • DafnyBench: 形式软件验证基准

    我们介绍了 DafnyBench，这是一个用于训练和评估形式软件验证的机器学习系统的最大基准测试。我们测试了 LLM（如 GPT-4 和 Claude 3）生成足够的提示来让 Dafny 形式验证引擎成功验证 750 多个程序，代码行数约为 53,000 行。最佳模型和提示方案的成功率达到 68%，我们量化了通过错误信息反馈重试时成功率的提高，以及所需代码和提示数量的恶化。我们希望 DafnyBench 能够在 LLMs 和验证技术质量提高时，从这个基准得到快速改进。

    Jun, 2024

  • 通过 Monte Carlo 树自我精化和 LLaMa-3 8B 获得 GPT-4 级数学奥赛解题方法

    这篇论文介绍了 MCT Self-Refine (MCTSr) 算法，它是大型语言模型（LLM）与蒙特卡洛树搜索（MCTS）的创新集成，在复杂的数学推理任务中提高性能。通过解决 LLM 在战略和数学推理中的准确性和可靠性挑战，MCTSr 利用系统化的探索和启发式自我精炼机制来改进 LLM 内的决策框架。该算法通过选择、自我精炼、自我评估和反向传播的迭代过程构建蒙特卡洛搜索树，利用改进的 Upper Confidence Bound（UCB）公式优化探索 - 利用平衡。广泛的实验证明了 MCTSr 在解决奥林匹克数学问题方面的效果，显著提高了多个数据集的成功率，包括 GSM8K、GSM Hard、MATH 以及 Math Odyssey、AIME 和 OlympiadBench 等奥林匹克级别基准。该研究推动了 LLM 在复杂推理任务中的应用，为未来的人工智能集成奠定了基础，提高了 LLM 驱动应用中的决策准确性和可靠性。

    Jun, 2024

  • 我说，你验证：朝向值得信赖的神经程序合成

    本文基于大型语言模型，提出了一种改进程序综合器可靠性和总体准确性的方法，通过语言模型自然语言描述求解程序问题，并且学习分析程序和断言的一致性，以判断哪个程序最有可能是正确的，从而通过提供可信的解决方案来改善可靠性

    Sep, 2022