Jul, 2024

PutnamBench: 在Putnam数学竞赛上评估神经定理证明器

HTML
PDF
TL;DRPutnamBench是一个多语言基准测试，用于评估神经定理证明器解决竞赛数学问题的能力，它包含了来自北美顶级本科数学竞赛William Lowell Putnam Mathematical Competition的640个定理的1697个手工构造形式化的表述，并用Lean 4和Isabelle进行了全部定理的形式化，其中还有一个相当大的子集有Coq形式化。该基准测试用于评估几种已有的神经和符号定理证明器，这些方法只能解决很少一部分的PutnamBench问题，从而将该基准测试确立为神经定理证明研究中的一个具有挑战性的开放问题。
发现论文，激发创造
  • 面向大规模神经定理证明

    提出了一种新型的神经定理证明器，通过仅考虑最高证明分数相关的证明路径，可以在以前无法应用的知识库上进行推理和学习。

    Jul, 2018

  • 利用语言模型进行定理证明的证明工件协同训练

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

    Feb, 2021

  • MiniF2F：面向正式奥林匹克数学的跨系统基准测试

    miniF2F是一个Olympiad级别的数学问题数据集，用于在神经定理证明中提供统一的跨系统基准。使用GPT-f作为神经定理证明的基线调用miniF2F，并提供了性能分析。

    Aug, 2021

  • Isabelle密码机

    该研究结合学习与定理证明的多种方式显著提高了E自动定理证明器在Isabelle Sledgehammer问题上的性能，特别是在ENIGMA指导，神经前提选择和E的有针对性策略的开发方法上。最终的ENIGMA和前提选择系统在15秒内比E的最佳先前版本提高了25.3％，也优于所有其他先前的ATP和SMT系统。该方法可在从Isabelle提取的数十万个一阶未分类和已分类问题的几次迭代训练中进行训练。

    May, 2022

  • Magnushammer: 基于Transformer的前提选择方法

    本文介绍了一个基于神经变换器的自动定理证明方法Magnushammer，使用PISA基准测试，证明率达到59.5％，超过了目前最成熟和最流行的基于符号的求解器Sledgehammer的38.3％，并通过与基于语言模型的神经形式证明器相结合，将先前的最先进证明率从57.0％提高到71.0％。

    Mar, 2023

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

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

    Oct, 2023

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

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

    Dec, 2023

  • 重构：从证明中学习提取定理

    通过使用REFACTOR方法，我们能够训练神经网络以模仿人类数学家在形式化数学定理证明中识别出的模块化和可重用的定理，从而提取出不同领域的新定理，这些新定理在证明过程中使用频率较高，并有助于缩短证明的长度，并最终使得在新定理重构的数据集上训练的证明器能够证明更多的测试定理并且胜过其他最先进的基线模型。

    Feb, 2024

  • 深度学习在定理证明中的调查

    该论文提供了一项深度学习在定理证明中的全面调研，包括现有方法的综述、数据集和策略的详细总结、评估指标和最先进技术的性能分析，以及未来研究的挑战和发展方向的批判性讨论。该调研旨在成为深度学习在定理证明中的基础参考，促进这个迅速发展领域的进一步研究。

    Apr, 2024

  • miniCTX：具备（长）上下文的神经定理证明

    本研究解决了神经定理证明模型在未见过的上下文下证明数学定理的能力问题。提出的miniCTX框架通过引入上下文信息，并结合文件调优方法，大幅提升了模型的证明性能，特别是在标准miniF2F基准上的通过率达到了33.61%，创造了1.3亿参数模型的新纪录。该工作为神经定理证明领域提供了一个新的评估视角。

    Aug, 2024