Jul, 2022

CD工具——简化引理证明的削减和结构生成（系统描述）

HTML
PDF
TL;DRCD Tools是一个使用证明结构为中心的形式化视图来实践压缩分离的Prolog库，其中包括基于证明结构枚举的专门证明器，其中SGCD具有特别灵活的混合证明搜索方式，并在实验中显示了该方法的特征和应用潜力。
发现论文，激发创造
  • Thor: 锤炼联合语言模型和自动定理证明器

    该论文介绍了Thor，一个集成语言模型和自动定理证明器的框架，它采用一种称为“hammers”的方法来选择前提，从而增加了语言模型在PISA数据集上的成功率并解决了相当一部分问题，同时比现有最佳方法在MiniF2F数据集上具有更小的计算量。

    May, 2022

  • 谁发现了短证明？使用高阶自动定理证明器探索Boolos的奇怪推理变体

    应用高阶自动推理证明器探索 Boolos' Curious 推论，通过提供适当的简写符号以发现短证明所需的高阶引理，并提出全证明自动化的可能性。

    Aug, 2022

  • 生成压缩组合证明结构——一种自动一阶定理证明方法

    本文介绍了一种将组合子术语表示为证明树的方法，并引入了基于参数化组合子术语定义的证明模式，实现了基于连接结构演算的特征的自动化一阶证明的实现和第一批实验结果。

    Sep, 2022

  • 证明结构研究

    提出并阐述了一种新的证明操纵和分析形式主义，为证明检索方式提高了效率，实现了较短证明的自动化，特别是在首阶问题上的历史证明中进行了一项全面的形式重建分析。

    Feb, 2023

  • 句子表格法进行范围受限插值

    本研究通过对克雷格插值的输入和输出进行限制，并结合一阶 ATP 推导系统的子句平板验证方法，证明了在一阶逻辑中可以传递范围限制和 Horn 属性。同时，我们还展现了一种解决限制子句平板结构一般问题的方法，并将其应用于查询综合和插值重构。该方法结合了证明结构操作和高度优化的一阶推理器，具有可行的实现前景。

    Jun, 2023

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

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

    Jun, 2023

  • LEGO证明器：具有增长库的神经定理证明

    LEGO-Prover使用技能库，通过模块化构建证明以及生成新技能，提高了大型语言模型在定理证明中的能力，并进一步推进了数学领域的研究。

    Oct, 2023

  • SymBa：用于多步自然语言推理的符号式向后推理

    通过引入符号性的自上而下求解器，与大型语言模型的集成，SymBa在多步推理基准测试中（ProofWriter，Birds-Electricity，GSM8k，CLUTRR-TF，ECtHR Article 6）相对于基线算法实现了性能、证明准确性和效率的显著提升。

    Feb, 2024

  • 基于理论的规范决策图

    决策图是一种有效表达命题公式的强大工具，本文介绍了一种通用技术将决策图应用于SMT级别，并可产生理论规范的T-DD，从而解决了现有技术的一些限制。

    Apr, 2024

  • DeepSeek-Prover-V1.5：利用证明助手反馈提升强化学习和蒙特卡洛树搜索

    本研究提出了DeepSeek-Prover-V1.5，一个用于Lean 4的开源语言模型，针对定理证明进行了优化，解决了训练和推理过程中的效率问题。创新性地采用了来自证明助手反馈的强化学习方法，并引入RMaxTS变体，以多样化的证明路径生成为目标。结果显示该模型在中学和本科水平的基准测试中取得了显著的成绩提升，展示了其在推理任务中的潜在影响。

    Aug, 2024