通过提出一种新的流程，我们利用合成数据来将自然语言数学问题转化为 Lean 4 语句，并相应地进行过滤，从而为解决 LLMs 在理解复杂数学问题和证明上的性能提供有用的训练数据。最终数据集包含约 57K 个正式 - 非正式问题对以及来自数学竞赛论坛的搜索证明和 21 个新的 IMO 问题。

Jun, 2024

DS-Prover 是一个用于定理证明的创新动态抽样方法，通过根据剩余时间和总分配时间来调整探索和开发之间的平衡，以提高证明搜索过程的效率，并通过拆分简化和重写策略为具有单个前提的策略来扩充训练数据集，从而在 MiniF2F 和 ProofNet 两个标准数据集上实现了显著的性能提升。

Dec, 2023

本文介绍了 LeanDojo：一个开源、可交互的证明环境，它从 Lean 中提取了证明中的数据及注释，提供了有价值的前提数据，以便于选取前提。 我们使用此数据，开发了 ReProver：第一个增加检索功能的基于 LLM 的证明程序。其成本低廉，只需要一台 GPU 进行一周的训练，并且可以有效地选择定理中的前提。我们构建了一个包含 96962 个定理和证明的新基准，并将其用于培训和评估。实验结果表明，相对于非检索基线和 GPT-4，ReProver 非常有效。我们发布了代码和数据集，以促进进一步的研究。

Jun, 2023

利用 Lean 框架，将复杂的逻辑推理问题形式化为定理后进行求解，以减少逻辑不一致性的风险并提升处理复杂推理任务的能力，取得了在 FOLIO 数据集上的最先进表现，并在 ProofWriter 上接近该水平的成果。值得注意的是，这些结果是在每个数据集的不到 100 个领域内样本进行微调实现的。

Mar, 2024

利用公开可获得的网络数据和 Group Relative Policy Optimization（GRPO）提高 DeepSeekMath 7B 的数学推理能力，使其在 MATH 基准上达到了 51.7% 的竞争水平，并接近了 Gemini-Ultra 和 GPT-4 的性能水平。

Feb, 2024

通过对高质量合成数据的微调，本文通过提出的算术难题问题展示出大型语言模型在多步推理任务上的出色表现，并通过开源的 3B 模型在三个不同的测试数据集上实验结果表明，这种模型不仅在域内数据集上能够达到 0.44 的零样本一次通过率 @1，而且还在域外数据集上展现出一定的泛化能力，对于扩展数字范围和算术难题问题的组合组件分别设计了两个域外数据集，在这两个更难的任务上，经过微调的模型展示出令人鼓舞的表现，零样本一次通过率 @1 分别为 0.33 和 0.35。

Jun, 2024

MathGenie 是一种从小规模的问题解决数据集（称为种子数据）生成多样且可靠的数学问题的新方法，通过增加种子数据的真实解决方案，并训练一个回译模型将增加的解决方案翻译回新问题，从而产生与代码集成的问题解决方案，进而提供理性基础验证策略，该方法通过对新收集的数据训练从 7B 到 70B 范围的预训练模型，形成了 MathGenieLM 系列模型，这些模型在五个代表性数学推理数据集上始终优于以前的开放源语言模型，达到了最新的性能水平，尤其是 MathGenieLM-InternLM2 在 GSM8K 上达到了 87.7％的准确率，在 MATH 上达到了 55.7％的准确率，获得了开放源语言模型的最佳综合得分。

Feb, 2024

基于 GPT-4 的数据合成能力，我们提出了一种通过训练小型语言模型来合成数学问题，以高效生成足够高质量的预训练数据的有效方法，并在数学推理数据集上展现了最先进的性能。

May, 2024

该研究论文介绍了使用大型语言模型作为辅助工具的 Lean Copilot 框架，用于证明定理过程中的自动化，证明步骤建议、自动完成中间证明目标、选择相关前提条件等。实验证明了该方法较现有的基于规则的证明自动化方法在证明定理过程中对人类的辅助和自动化程度的有效性。

Apr, 2024

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

Nov, 2023