基于大规模合成数据，使用 Lean 4 proof 数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高 LLMs 中的定理证明能力的潜力。

May, 2024

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

Mar, 2024

自然语言处理和大型语言模型在教育和指导方法领域取得了快速进展，特别在解决数学问题的应用方面，其中 MAmmoTH-13B 表现出了最高的能力水平，成为解决 NCERT 数学问题的可靠基准。

Apr, 2024

本研究使用大型语言模型 (Codex) 探讨将使用自然语言书写的数学（即定义，定理陈述和证明）转化为可以被程序检查正确性的形式语言的能力，并发现对于 120 个定理，Codex 可以在本科水平上以近 75％的准确率进行短数学陈述的形式化。同时在选择合适的输入和后处理策略下，Codex 可以以自然语言形式翻译本科水平的 13 个定理的证明，这些具有两到三自然段长度的证明可以在 12 次中有至少一次完成翻译，这表明大型语言模型是完全或部分自动化形式化的有前景的途径。

Nov, 2022

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

Jun, 2024

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

Jun, 2023

数学推理是评估人类智能基本认知能力的基石。该研究调查了大型语言模型在解决数学问题方面的真正进展、障碍、数学问题类型和相关数据集、解决数学问题的 LLM 技术范围、影响 LLMs 解决数学问题的因素和问题，并提供了这一快速发展领域中的现状、成就和未来挑战的整体观点。

Jan, 2024

大型语言模型 (LLMs) 具有彻底改变自动形式化的潜力。引入数学编程语言 Lean4 为评估 LLMs 的自动形式化能力提供了前所未有的机会。本文介绍了一种专为 Lean4 设计的新型评估基准，将其应用于测试包括 GPT-3.5、GPT-4 和 Gemini Pro 在内的最先进的 LLMs 的能力。我们全面的分析发现，尽管最近有所进展，这些 LLMs 在自动形式化方面仍存在局限性，尤其是在更复杂的数学领域。这些发现强调了需要进一步发展 LLMs，以充分发挥它们在科学研究和开发中的潜力。本研究不仅为当前的 LLM 能力设立了基准，还为自动形式化的未来增强奠定了基础。

Jun, 2024

我们提出了 Llemma 这个大型数学语言模型，通过将 Code Llama 进行预训练得到了 Llemma，并在 MATH 基准测试中表现优于所有已知的开源基础模型，同时还能进行工具使用和形式定理证明而无需进一步微调。

Oct, 2023

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

Apr, 2024