能够严格检查的LLMs是否能够生成数学证明？了解LeanDojo：一个开源的AI游乐场，提供工具包、基准测试和模型，用于大型语言模型在Lean证明助手中证明形式化定理

人工智能和机器学习是当今时代的热门领域。随着人工智能取得的巨大进步，新的创新正在改变人类与机器的互动方式。人类智能中的推理是人工智能的重要组成部分。许多定理证明方法已经得到研究，例如自动定理证明（ATP），它是自动为形式逻辑中的定理生成证明的过程。由于搜索空间庞大，ATP具有挑战性，交互式定理证明（ITP）作为一种替代范式出现，其中人类专家与称为证明助手的软件工具进行交互以构造证明。

大型语言模型（LLMs）在代码生成方面表现出色，但在定理证明方面面临事实性和幻觉方面的困难。为了克服这些限制，来自加州理工学院、NVIDIA、麻省理工学院、加州圣塔芭芭拉分校和德克萨斯大学奥斯汀分校的研究人员引入了LeanDojo，这是一个基于LLM的开源工具包，用于定理证明。LeanDojo构建在数学家中流行的Lean证明助手周围，为使用Lean和提取数据提供了资源。

在数据提取中，训练数据是从证明树和原始Lean代码中不立即显现的中间证明状态中收集的。LeanDojo已经能够使模型能够与Lean进行程序化通信。这使它们能够查看证明状态，执行证明操作或策略，并从Lean获得反馈。开源的Lean playground由许多元素组成，包括工具包、数据、模型和基准，以实现与证明环境的编程交互，并从Lean中提取数据。

• 百度Ernie 3.5在中文语言AI领域脱颖而出：但它真的比ChatGPT更好吗？
• 随着OpenFlamingo团队发布了OpenFlamingo v2，该团队在3B、4B和9B规模上推出了五个新的多模态模型，这些模型表现优于之前的模型
• Unity宣布发布Muse：一款文本到视频游戏平台，它使您能够使用自然语言创建纹理、精灵和动画

LeanDojo为证明中的前提提供了细粒度的注释，这对于前提选择是有价值的，它是定理证明中的一个重要瓶颈。通过使用LeanDojo的数据提取功能，研究人员还开发了ReProver，这是第一个具有大型数学库的检索增强LLM证明器。与以前依赖于需要大量计算资源的私有数据集的方法不同，ReProver的设计更具可访问性和成本效益。它需要更少的计算资源，每周只需一个GPU进行训练。

ReProver的检索机制利用LeanDojo的程序分析能力来查找可访问的前提并产生可能出错的具体示例。因此，证明器的性能更好，检索过程更有效。为了评估和进一步研究，该团队开发了一个新的基准数据集，其中包含从Lean的数学库中提取的96962个定理和证明。该基准数据集具有具有挑战性的数据分割，要求证明器对在训练过程中未使用的新前提的定理进行泛化。实验结果表明，在使用该基准数据集进行训练和评估时，ReProver与非检索基线和GPT-4相比表现良好。

总之，基于LLM的定理证明的这种开源解决方案对于未来似乎很有前途。它通过提供可访问的工具包、数据、模型和基准来克服私有代码、数据和大量计算要求的障碍。