Jul, 2024

Lean-STaR：学习交替思考与证明

HTML
PDF
TL;DR传统基于语言模型的定理证明假设在足够数量的形式证明数据上训练后，模型将学会证明定理。研究观察到非形式证明中蕴含的丰富信息对于学习证明定理是有用的。因此，使用回顾性的真实策略生成合成思考来训练语言模型，Lean-STaR框架通过在每个证明步骤的预测策略之前直接生成思考来提升模型的证明定理能力，并通过专家迭代进一步微调模型。在Lean定理证明环境中，Lean-STaR在miniF2F-test基准上取得了最先进的结果，显著优于基准模型（$43.4% ightarrow 46.3%，$ Pass@64），同时对增强思考对定理证明过程的各个方面的影响进行了分析，提供了洞察力。
发现论文，激发创造
  • 利用语言模型进行定理证明的证明工件协同训练

    本文介绍了 PACT 的一般方法，通过自我监督学习从内核级证明术语中提取丰富的数据，以协同常规战术预测目标，以提高定理证明的成功率。

    Feb, 2021

  • 自然证明器：基于语言模型的数学证明生成

    通过人工提供或查找背景参考条件，NaturalProver 能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量，在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过40%的正确和有用率。

    May, 2022

  • LeanDojo：具备检索增强语言模型的定理证明

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

    Jun, 2023

  • 通过数据增强和动态采样方法提升神经定理证明

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

    Dec, 2023

  • LeanReasoner: 用Lean增强复杂逻辑推理

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

    Mar, 2024

  • 借鉴失败：使用试错数据对直觉命题逻辑证明进行微调的LLM

    通过从失败的搜索路径中学习，我们展示了训练模型的益处。我们与仅使用正确路径训练的模型进行比较，并发现前者以更少的搜索次数解决了更多未见过的定理。

    Apr, 2024

  • 迈向在Lean中进行定理证明的大型语言模型作为副驾驶

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

    Apr, 2024

  • DeepSeek-Prover: 通过大规模合成数据推进LLMs中的定理证明

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

    May, 2024

  • TheoremLlama: 通用 LLM 转换为 Lean4 专家

    使用Lean等计算机可验证形式语言来证明数学定理具有重大影响，本文提出了TheoremLlama框架，通过生成对齐的数据集和训练方法，使大型语言模型成为Lean4专家，实现了高于GPT-4基准的累积准确率。

    Jul, 2024

  • LeanAgent：用于形式定理证明的终身学习

    本研究解决了现有大语言模型在高等数学定理证明中缺乏广泛适应性的问题。LeanAgent提出了一种新的终身学习框架，通过动态数据库和课程学习策略，有效管理和拓展数学知识。研究发现，LeanAgent在挑战性定理证明上表现优异，其性能比传统模型高出11倍，展现了显著的学习进步和知识迁移能力。

    Oct, 2024