3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
Australian National University（澳大利亚国立大学）；Defence Science and Technology Group（国防科学与技术集团）；Google DeepMind（谷歌DeepMind）；BIMLOGIQ
针对自动定理证明搜索空间过大的问题，提出3D-Prover方法，通过行列式点过程筛选语义多样的高质量证明策略，可增强各类证明LLM，在多个基准上提升了证明效率与成功率。
2025-10-28 cs.AI cs.LO
Proving Theorems using Incremental Learning and Hindsight Experience Replay
DeepMind
传统的一阶逻辑自动定理证明器依赖于速度优化的搜索和许多手工设计的算法，这些算法被设计成在广泛的领域中工作得最好。文献中的机器学习方法要么依赖于这些传统的证明器来引导自己，要么无法达到可比的性能。在本文中，我们提出了一个一般的增量学习算法的训练域特定的证明一阶逻辑没有等式，只基于一个基本的给定子句算法，但使用一个学习子句评分功能。子句被表示为图，并呈现给具有谱特征的Transformer网络。为了解决稀疏性和初始缺乏训练数据以及缺乏自然课程，我们将事后经验重放适应于定理证明，以便即使在没有证据的情况下也能够学习。我们表明，以这种方式训练的证明者可以在证明的数量和质量方面与TPTP数据集上的最先进的传统证明者相匹配，有时甚至超过。
2021-12-20 cs.AI cs.LO
Training a First-Order Theorem Prover from Synthetic Data
DeepMind
将机器学习应用于自动化定理证明的一个主要挑战是训练数据的稀缺性，这是训练成功的深度学习模型的关键因素。为了解决这个问题，我们提出了一种方法，该方法依赖于纯粹使用合成生成的定理进行训练，除了公理之外没有任何人类数据。我们使用这些定理来训练一个神经指导的饱和度为基础的证明。我们的神经证明器在时间和搜索步骤上都优于最先进的E-prover，并且显示出从TPTP库中转移到看不见的人类书面定理的显着转移，在那里它解决了72%的一阶问题而没有等式。
2021-04-06 cs.AI
Learning to Guide a Saturation-Based Theorem Prover
IBM Research（IBM研究院）；Northwestern University（西北大学）；Arizona State University（亚利桑那州立大学）；The University of Auckland（奥克兰大学）
传统的自动定理证明器依赖于手动调整的算法来指导它们如何执行证明搜索。然而，最近，有一个学习机制，可以集成到定理证明，以提高其性能自动设计的兴趣激增。在这项工作中，我们介绍了TRAIL，这是一种基于深度学习的定理证明方法，它在神经框架内表征了基于饱和的定理证明的核心元素。TRAIL利用（a）一个有效的图神经网络表示逻辑公式，（b）一个新的神经表示的状态的基于饱和的定理证明在处理条款和可用的行动，和（c）一个新的表示的推理选择过程作为一个基于注意力的行动政策。我们通过系统分析表明，这些组件使TRAIL在两个标准基准数据集上的性能显著优于以前基于强化学习的定理证明器（证明的定理增加了36%）。此外，据我们所知，TRAIL是第一个基于强化学习的方法，在标准定理证明基准上超过最先进的传统定理证明器的性能（解决高达17%的问题）。
2021-06-07 cs.AI cs.LO
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
Google Research（谷歌研究院）
我们提出了一个环境，基准测试，和深度学习驱动的自动定理证明高阶逻辑。高阶交互式定理证明器使任意数学理论的形式化成为可能，从而为深度学习提出了一个有趣的、开放式的挑战。我们提供了一个基于HOL Light定理证明器的开源框架，可用作强化学习环境。HOL Light广泛覆盖了微积分的基本数学定理和开普勒猜想的正式证明，从中我们获得了自动推理的挑战性基准。我们还提出了一个深度强化学习驱动的自动定理证明器DeepHOL，在这个基准测试中取得了很好的初步结果。
2019-11-01 cs.AI cs.LG cs.LO
Partial Label Learning for Automated Theorem Proving
Alfréd Rényi Institute of Mathematics（阿尔弗雷德·雷尼数学研究所）；Eötvös Loránd University（欧多尼·劳尔德大学）
本文首次将学习引导的自动定理证明建模为偏标签学习，提出处理备选证明的理论框架，并用 plCoP 证明器验证偏标签学习方法能提升学习辅助定理证明器的性能。
2025-07-04 cs.AI cs.LO
Integrating Testing and Interactive Theorem Proving
Northeastern University（东北大学）；University of Texas at Austin（德克萨斯大学奥斯汀分校）
使用交互式定理证明器来推理程序涉及一系列交互，其中用户用图解来挑战定理证明器。然而，许多提出的证明实际上是错误的，用户在意识到这一点之前经常花费相当大的精力来检查定理证明器的输出。我们提出了一个协同集成的测试与定理证明，实现在ACL2轿车（ACL2），自动生成具体的反例。我们的方法使用的全部权力的定理证明和相关的库来简化代数，这种简化可以转换代数，找到反例是很难的代数，找到反例是平凡的。事实上，我们的方法甚至会导致更好的定理证明，例如，如果测试表明推广步骤导致错误的猜想，我们会迫使定理证明器回溯，允许它追求更富有成效的选择，可能会产生证明。本文的重点是工程的协同集成测试与交互式定理证明，这包括扩展ACL 2的新功能，我们希望是普遍感兴趣的。我们还讨论了我们的经验，在使用ACL2教新生如何对他们的程序的原因。
2011-10-21 cs.AI cs.LO cs.SE
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
DeepSeek（深度求索）；Sun Yat-sen University（中山大学）；University of Edinburgh（爱丁堡大学）；MBZUAI（穆罕默德·本·扎耶德人工智能大学）
本研究提出利用大规模合成数据（800万条形式化证明）微调 DeepSeekMath 7B，显著提升大语言模型在 Lean 4 定理证明上的性能，超越 GPT-4 和树搜索方法。
2024-05-23 cs.AI
Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
Princeton University（普林斯顿大学）；NVIDIA（英伟达）；Tsinghua University（清华大学）；Stanford University（斯坦福大学）；Meta FAIR；Amazon（亚马逊）；Shanghai Jiao Tong University（上海交通大学）；Peking University（北京大学）
Goedel-Prover-V2通过脚手架式数据合成、验证器引导的自我修正和模型平均，在自动定理证明中达到新SOTA，8B模型超越671B模型，32B模型在MiniF2F上达90.4%。
2025-08-05 cs.AI cs.LG
CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)
University of Potsdam（波茨坦大学）
CD Tools是一个Prolog库，用于在一阶ATP中试验凝聚分离，它将最近围绕证明结构的正式观点付诸实践。从一阶ATP的观点来看，凝聚分离提供了一个相对简单但具有基本特征和重要应用的环境，使其成为开发和评估新技术的基础。CD Tools包含基于枚举证明结构的专用证明器。我们在这里集中在其中之一，SGCD，它允许混合目标和公理驱动的证明搜索特别灵活的方式。在纯目标驱动的配置中，它的作用类似于子句表或连接方法家族的证明者。在混合配置中，它的性能要强得多，接近最先进的证明器，同时发出相对较短的证明。实验表明了该证明器实现的结构生成方法的特点和应用的可能性。对于ATP中经常研究的一个历史性问题，它产生了一个新的证明，比任何已知的证明都要短得多。
2022-07-18 cs.AI cs.LO
InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search
Shanghai AI Laboratory（上海人工智能实验室）；The Chinese University of Hong Kong（香港中文大学）；Tsinghua University（清华大学）；University of Southern California（美国南加州大学）
针对大语言模型定理证明中最佳优先搜索忽略轨迹偏好信息的问题，提出评论家引导搜索的方法，结合大规模专家迭代训练的InternLM2.5-StepProver显著提升证明性能，并开源相关资源。
2025-10-21 cs.AI cs.CL
Gym-saturation: an OpenAI Gym environment for saturation provers
CNRS（法国国家科学研究中心）；Université Côte d’Azur（蔚蓝海岸大学）
“gym-saturation”是一个OpenAI Gym环境，用于能够证明定理的强化学习（RL）代理。目前，只支持以子句范式（CNF）的Thousands of Problems for Theorem Provers（TPTP）库中的形式语言编写的定理。`gym-saturation`实现了'given clause'算法（类似于Vampire和E Prover中使用的算法）。用Python编写的`gym-saturation`受到PyRes的启发。与典型的自动定理证明器（ATP）的整体架构相比，“健身房饱和度”为不同的代理人提供了自己选择条款的机会，并根据他们的经验进行训练。与特定的代理相结合，“健身饱和”可以作为ATP工作。即使使用基于遗传学的未经训练的代理，“gym-saturation”也可以从TPTP v7.5.0中找到688个（8257个）CNF问题的反驳。
2022-03-09 cs.AI
Designing Game of Theorems
CIIRC（捷克信息学、机器人学与控制论研究所）；CTU（捷克技术大学）；The University of Innsbruck（因斯布鲁克大学）
“定理证明类似于围棋。所以，我们可以使用深度学习来改进我们的证明器，就像DeepMind开发的超级计算机围棋程序AlphaGo一样。“这种乐观情绪在AITP 2017的参与者中得到了观察。但定理证明真的和围棋相似吗？在本文中，我们首先确定它们之间的相似性和差异，然后提出了一个系统，在该系统中，各种证明者不断相互竞争，不断改变自己，直到他们证明用户提供的证明。
2019-06-20 cs.AI
Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
ByteDance Seed（字节跳动Seed团队）；AI4Math
本研究提出引理式全证明推理模型Seed-Prover与几何推理引擎Seed-Geometry，通过形式化验证结合长思维链强化学习实现深度广度推理，在多个数学定理证明基准上大幅超越SOTA，还在2025年IMO中证明6题中的5题。
2025-08-01 cs.AI cs.CL
Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
Princeton Language and Intelligence, Princeton University（普林斯顿语言与智能，普林斯顿大学）；Tsinghua University（清华大学）；Amazon（亚马逊）；Meta FAIR；Numina
本文提出开源模型Goedel-Prover，通过构建大规模形式化陈述与证明数据集并进行监督微调，在自动定理证明上达到最先进性能，显著超越先前模型。
2025-04-19 cs.AI cs.LG
A Minimal Agent for Automated Theorem Proving
本文提出一个最小代理基准，用于比较不同AI定理证明器架构。通过迭代证明细化、库搜索和上下文管理核心功能，展示了与前沿方法相媲美的性能，同时架构更简单且成本更低。
2026-05-14 cs.AI
Cooperation between Top-Down and Bottom-Up Theorem Provers
自顶向下和自自底向上的【形】的定理证明方法各有其优缺点。自底向上的【形】证明器得益于强冗余控制，但缺乏目标导向，而自顶向下的证明器是目标导向的，但往往有弱演算时，他们的证明长度被认为是。为了整合这两种方法，我们试图实现自上而下和自自底向上的【形】的证明器之间的合作，在两种不同的方式：第一种技术的目的是支持自自底向上的【形】的自上而下的证明器。自顶向下的证明器生成子目标子句，然后由自自底向上的【形】的证明器进行处理。第二种技术是在自顶向下的证明器中使用自自底向上的【形】生成的引理。我们将我们的概念应用于模型消除和叠加领域。我们讨论了我们的技术，以缩短证明，以及重新排序的搜索空间以适当的方式的能力。此外，为了确定子目标条款和引理，这实际上是相关的证明任务，我们开发了一个基于相关性的过滤方法。与证明SETHEO和SPASS在问题库TPTP中进行的实验揭示了我们的合作方法的高潜力。
2011-05-27 cs.AI
Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models
Microsoft Research（微软研究院）；University of Science and Technology of China（中国科学技术大学）；Nanjing University（南京大学）；Rice University（莱斯大学）
该研究提出无需额外训练的神经符号增强框架DSP+，通过优化草拟、概化与证明三阶段流程，在多个定理证明基准上取得媲美主流RL训练方法的性能，还发现了数据集中的形式化错误。
2025-06-13 cs.AI
Holophrasm: a neural Automated Theorem Prover for higher-order logic
Stanford University（斯坦福大学）
我提出了一个使用深度学习和避免手工构造特征的高阶逻辑中的自动定理证明系统。Holophrasm利用Metamath语言的形式主义，并使用神经网络增强的强盗算法和序列到序列模型进行动作枚举来探索部分证明树。该系统从Metamath的set.mm模块中证明了14%的测试定理。
2016-08-10 cs.AI cs.LO
Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning
Preferred Networks, Inc.（首选网络公司）
自动定理证明（ATP）中的问题求解可以被解释为证明者逐步构造证明树的搜索问题。本文提出了一种用于直觉命题逻辑中证明搜索的深度强化学习算法。将深度学习应用于ATP的最大挑战是缺乏大型公共定理数据库。然而，我们通过在强化学习的每次迭代中应用新的数据增强过程来克服这个问题。我们还提高了算法的效率，通过一种新的紧凑图表示公式的语法结构。使用大量的扩充数据，我们训练高度精确的图神经网络，其近似公式的语法结构的集合的价值函数。我们的方法在计算时间方面也具有成本效益。我们将展示我们的证明器优于Coq的$\texttt{tauto}$策略，这是一种基于人类工程学的证明器。在指定的时间限制内，我们的证明器解决了基准库中84%的定理，而$\texttt{tauto}$只能解决52%。
2018-11-02 cs.AI cs.LG cs.LO
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
University of Cambridge（剑桥大学）；University of Warsaw（华沙大学）；IDEAS NCBR（IDEAS国家生物医学研究中心）；Polish Academy of Sciences（波兰科学院）；Google Research（谷歌研究院）；Stanford University（斯坦福大学）
在定理证明中，从一个大的库中选择有用的前提来解开一个给定猜想的证明是至关重要的。这对所有定理证明器提出了挑战，特别是那些基于语言模型的定理证明器，因为它们相对无法以文本形式推理大量前提。本文介绍了托尔，框架集成语言模型和自动定理证明，以克服这一困难。在Thor中，一种称为锤子的方法利用了自动定理证明器的功能，用于前提选择，而所有其他任务都指定给语言模型。Thor将语言模型在PISA数据集上的成功率从$39\%$提高到$57\%$，同时解决语言模型和自动定理证明器都无法解决的问题的$8.2\%$。此外，由于计算预算明显较小，Thor可以在MiniF2F数据集上实现与现有最佳方法相当的成功率。Thor可以通过我们提供的简单协议为大多数流行的交互式定理证明器实例化。
2022-05-22 cs.AI
The Mathematical Game
Université Paris Dauphine - PSL（巴黎多芬大学-PSL大学）；CNRS（法国国家科学研究中心）
本文提出用其他博弈树搜索算法改进结合 MCTS 与神经网络的 Holophrasm 定理证明器，以提升自动定理证明性能。
2023-09-22 cs.AI
OProver: A Unified Framework for Agentic Formal Theorem Proving
Lean 4
本文提出OProver，一个用于Lean 4的统一框架，通过迭代修订检索到的编译器验证证明和Lean编译器反馈来改进代理证明，通过持续预训练和迭代后训练，使OProver-32B在多个基准测试中取得最佳成绩。
2026-05-17 cs.AI cs.CL
FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
Koç University, Department of Computer Science and Engineering（科克大学计算机科学与工程系）；Codeway Studios（Codeway工作室）；Boğaziçi University, Department of Computer Engineering（博雅奇大学计算机工程系）；Friedrich-Alexander-Universität Erlangen-Nürnberg, Intelligent Language Systems（埃尔兰根-纽伦堡弗里德里希-亚历山大大学智能语言系统）
本文提出FormalRewardBench，通过250对偏好数据评估奖励模型，发现前沿LLM在证明评估中表现最佳，而专门定理证明模型表现最差，揭示了证明能力与评估能力的差异。
2026-05-11 cs.AI
Do Theorem Provers Need Theorem-Proving Agents? mini-Lean-agent: A Coding-Agent Baseline for Lean
Princeton Language and Intelligence（普林斯顿语言与智能中心）；Princeton University（普林斯顿大学）；Rutgers University（罗格斯大学）
该研究针对Lean定理证明任务推出极简智能体mini-Lean-agent，对比实验显示其在Putnam 2025基准上性能优于部分现有智能体，可作为定理证明基础设施评估的标准基线。
2026-10-14 cs.AI cs.LO
Generative Language Modeling for Automated Theorem Proving
OpenAI
我们探讨了基于transformer的语言模型在自动定理证明中的应用。这项工作的动机是一个主要的限制自动定理证明人相比，人类-原始数学术语的生成-可能是通过从语言模型生成寻址的可能性。我们提出了一个自动化的证明和证明助手，GPT-f，元形式化语言，并分析其性能。GPT-f发现了新的简短证明，这些证明被主Metamath库所接受，据我们所知，这是基于深度学习的系统第一次提供被正式数学社区采用的证明。
2020-09-07 cs.AI cs.CL cs.LG
Proceedings 19th International Workshop on the ACL2 Theorem Prover and Its Applications
Austin, TX（德克萨斯州奥斯汀）
本文介绍第19届 ACL2 研讨会论文集，说明 ACL2 作为工业级自动化推理系统和 Boyer-Moore 系列最新定理证明器的定位，并提及该工作获2005年 ACM 软件系统奖。
2025-07-24 cs.AI cs.LO
A Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools
University of Coimbra（科英布拉大学）；University of Aveiro（阿威罗大学）
在中学采用自动扣分系统面临着几个瓶颈。除了与课程和教师有关的问题之外，几何自动定理证明器的结果与学校中的演示和证明的正常实践之间的不协调是在教育环境中更广泛地使用这种工具的主要障碍。由于早期的几何自动定理证明器的实现，人工智能方法的应用，基于推理规则和使用前向链推理的综合证明器被认为更适合于教育建议。选择一组合适的规则和一种可以使用这些规则的自动化方法是一个主要的挑战。我们讨论了这样一个规则集和它的实现使用几何演绎数据库方法（GDDM）。该方法使用一些选择的几何图形进行测试，这些几何图形可能是第7年班级的目标（约100米）。12岁学生）。本文提出了一个教案，其目标是引入几何定理证明的形式化演示，试图激发学生的这一目标
2023-03-10 cs.AI cs.CY cs.LO
Learning to Prove Theorems by Learning to Generate Theorems
Princeton University（普林斯顿大学）
我们认为自动定理证明的任务，一个关键的人工智能任务。深度学习在训练定理证明器方面已经显示出了希望，但是用于监督学习的人类编写的定理和证明有限。为了解决这个问题，我们建议学习一个神经生成器，它可以自动合成定理和证明，以训练定理证明器。在真实任务上的实验表明，从我们的方法中合成数据改进了定理证明器，并推进了Metamath中自动定理证明的最新技术。代码可在https://github.com/princeton-vl/MetaGen上获得。
2020-10-30 cs.AI cs.LG cs.LO
Reinforcement Learning of Theorem Proving
University of Innsbruck（因斯布鲁克大学）；Czech Technical University in Prague（布拉格捷克理工大学）；University of Warsaw（华沙大学）；Charles University（查理大学）
我们介绍了一个定理证明算法，实际上没有使用域推理指导其连接式证明搜索。相反，它运行了许多蒙特卡洛模拟，这些模拟由以前的证明尝试中的强化学习指导。我们生产几个版本的证明，参数化不同的学习和指导算法。该系统的最强版本是在大量数学问题上训练的，并在以前看不见的问题上进行评估。经过训练的系统在相同数量的推理中解决的问题比基线证明器多40%以上，这在这个人工智能领域是一个非常高的改进。据我们所知，这是强化学习第一次被令人信服地应用于大规模解决一般数学问题。
2018-05-19 cs.AI cs.LG cs.LO
MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize
University of Maryland（马里兰大学）；Georgia Institute of Technology（佐治亚理工学院）；Cornell University（康奈尔大学）；All Purpose AI
本研究推出涵盖13个数学领域的诊断基准MathAdv，结合Lean 4评估当代定理证明器，发现形式化是瓶颈、性能跨领域差异大等问题，为分组件评估模型能力提供依据。
2026-10-20 cs.AI cs.CL cs.LO
Learning Equational Theorem Proving
Radboud University Nijmegen（拉德堡德大学（奈梅亨））；Czech Technical University Prague（布拉格捷克理工大学）
我们开发了分层最短解模仿学习（3SIL）来学习深度强化学习（RL）设置中的方程定理证明。自我训练的模型在证明准群理论中的顶级开放式算法之一阿贝尔内映射（AIM）猜想所产生的问题方面达到了最先进的性能。为了开发这些方法，我们首先使用两个更简单的算术重写任务，它们与AIM问题共享树结构的证明状态和稀疏奖励。在这些任务中，3SIL被证明显着优于几个既定的RL和模仿学习方法。最后的系统，然后评估在一个独立的和合作的模式对AIM的问题。独立的3SIL训练系统在60秒内证明的定理（70.2%）比复杂的手工设计的Waldmeister系统（65.5%）多。在合作模式下，最终系统与Prover9系统相结合，在2秒内证明了独立Prover9在60秒内证明的内容。
2021-02-10 cs.AI cs.LG cs.LO
Reasoning, Metareasoning, and Mathematical Truth: Studies of Theorem Proving under Limited Resources
Microsoft Research（微软研究院）；Center for the Study of Language and Information（语言与信息研究中心）；Stanford University（斯坦福大学）
在早期的工作中，我们引入了灵活推理和决策理论元推理来解决规范推理的棘手问题。在这里，而不是追求的任务，计算信念和行动的决策模型组成的区别不确定的事件，我们研究的方法推断信念的数学真理之前，自动定理证明完成证明。我们采用贝叶斯分析来更新对真理的信念，给出了定理证明的进展，并展示了如何使用决策理论方法来确定在时间紧迫的情况下继续审议与立即采取行动的价值。
2013-02-20 cs.AI
NanoProof: Open and Efficient Automated Theorem Proving in Lean 4
Institute of Formal and Applied Linguistics, Faculty of Mathematics and Physics, Charles University（查理大学数学与物理学院形式与应用语言学研究所）
NanoProof是Lean 4中首个因子化执行引导型开放自动定理证明器，以低计算量实现优于同类系统的性能，证明该类证明器可利用适度资源从头构建。
2026-10-09 cs.AI cs.LG
Lyra: Orchestrating Dual Correction in Automated Theorem Proving
The Chinese University of Hong Kong（香港中文大学）；Sun Yat-sen University（中山大学）；Huawei Noah’s Ark Lab（华为诺亚方舟实验室）
本文提出Lyra框架，通过工具纠正和猜想纠正双重机制有效缓解LLM在自动定理证明中的幻觉并利用错误信息改进证明，在miniF2F上取得SOTA性能。
2024-08-24 cs.AI cs.CL
Mathesis: Towards Formal Theorem Proving from Natural Languages
Huawei Celia Team（华为Celia团队）；Huawei Noah’s Ark Lab（华为诺亚方舟实验室）；The Chinese University of Hong Kong（香港中文大学）
本文提出端到端自然语言定理证明流水线Mathesis，结合强化学习自动形式化器、LeanScorer与证明器，并构建Gaokao-Formal基准，在MiniF2F和高考形式化任务上取得先进结果。
2025-06-08 cs.AI
Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving
Tencent AI Lab（腾讯AI Lab）
针对LLM在形式证明上弱于非形式推理的难题，提出解耦推理与证明的框架，用专用推理器生成子目标引理并由证明器验证，在2000年后IMO难题上成功解决5题。
2025-07-07 cs.AI cs.LO
Rare Speed-up in Automatic Theorem Proving Reveals Tradeoff Between Computational Time and Information Value
UNAM（墨西哥国立自治大学）；University of Oxford（牛津大学）；LABORES；Carnegie Mellon University（卡内基梅隆大学）
我们发现，在自动定理证明中实现的策略涉及到执行速度，证明加速/计算时间和有用的信息之间的一个有趣的权衡。我们提前正式定义这些概念的正常相关的预期（最佳）理论加速时，添加有用的信息（其他定理作为公理）的概念，与实际的策略，可以有效地和高效地实施。我们提出了一个不可避免的权衡存在这种正常性和计算的时间复杂度。这个论点量化了信息在（积极的）加速方面的有用性。结果揭示了一种没有免费午餐的情况下，权衡的基本性质。本文中的主要定理与数值实验一起-使用两个不同的自动定理证明器APros和Prover 9进行命题逻辑的随机定理-为这样一个事实提供了强有力的理论和经验论据，即找到新的有用信息来解决一个特定的问题（定理），一般来说，和问题（定理）本身一样困难。
2015-06-14 cs.AI cs.LO
PhysProver: Advancing Automatic Theorem Proving for Physics
University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；Rutgers University（罗格斯大学）
PhysProver通过结合可验证语言和强化学习，提升物理领域形式化定理证明的效率和效果。
2026-01-22 cs.AI cs.CL
Learning to Reason
自动定理证明一直是人工智能的一项重要任务。证明构成了严格科学探究的基石。在过去的半个世纪里，已经开发了许多工具来部分和完全自动化它们的推导。一些最先进的证明器的例子是E（Schulz，2013），VAMPIRE（Kovács & Voronkov，2013）和Prover 9（McCune，2005-2010）。较新的定理证明器，如E，使用叠加演算代替更传统的解决方案和基于表格的方法。过去也有许多尝试将机器学习方法应用于指导证明搜索。早在1990年，Suttner和Ertel就提出了一种基于多层感知器的方法，使用手工设计的特征; Urban等人（2011）将机器学习应用于Tableau演算; Loos等人（2017）最近提出了一种使用深度神经网络指导E定理证明器的方法。然而，所有这些先前的工作都有一个共同的局限性：它们都依赖于经典一阶逻辑的公理。非经典逻辑的自动定理证明很少受到关注。最近的例子之一是McLaughlin & Pfenning（2008），他们将极化逆方法应用于直觉主义命题逻辑。除此之外，文学大多是沉默的。这确实是不幸的，因为有很多理由希望非经典证明超过经典证明。由于著名的Curry-Howard对应（Howard，1980），构造性/直觉主义证明应该对计算机科学家特别感兴趣，该对应告诉我们，所有终止程序都对应于直觉主义逻辑中的证明，反之亦然。这项工作探讨了使用Q学习…
2018-10-12 cs.AI
What are the Right Symmetries for Formal Theorem Proving?
University of Oxford（牛津大学）；KAIST（韩国科学技术院）；TU Wien（维也纳技术大学）；AITHYRA
本文探讨了正式定理推理中应尊重的对称性，提出了基于范畴论的重写范畴框架，用于形式化证明等价性和成功不变性，并通过测试时方法改进了LLM基定理证明器的鲁棒性和性能。
2026-05-21 cs.AI cs.LG cs.LO
Leanabell-Prover: Posttraining Scaling in Formal Reasoning
Kuaishou Technology（快手科技）
本研究通过持续训练和强化学习对自动定理证明模型进行后训练缩放，成功改进 DeepSeek-Prover-v1.5 和 Goedel-Prover，在 MiniF2F 上达到 59.8% 的通过率，实现全证明生成的最先进性能。
2025-07-14 cs.AI
Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method
National Institute of Science Education and Research（国家教育与科学研究院）；Homi Bhabha National Institute（霍米·巴巴国家研究所）
本文提出DS-Prover动态采样方法，通过根据剩余时间调整策略数量优化证明搜索，并分解多前提策略增强训练数据，在MiniF2F和ProofNet上取得显著性能提升。
2024-02-15 cs.AI cs.LG cs.LO
Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving
State Key Laboratory for Novel Software Technology（新型软件技术国家重点实验室）
本文提出段级监督策略，通过提取局部连贯的证明段落训练策略模型，提升定理证明的成功率，并在推理阶段减少计算成本。
2026-05-12 cs.AI
Cost-Efficient Theorem Proving via Agent Orchestration in Program Verification
Columbia University（哥伦比亚大学）；Barnard College, Columbia University（哥伦比亚大学巴纳德学院）；The Hong Kong University of Science and Technology（香港科技大学）
针对程序验证中定理证明成本高昂的问题，提出CoCo-Prover，通过两层证明图与智能体编排实现成本高效决策，在五个Lean 4基准上取得最优求解率并降低最高30.9%成本。
2026-10-08 cs.AI cs.LO cs.PL
Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
FU Berlin（柏林自由大学）；University Erlangen-Nürnberg（埃尔朗根-纽伦堡大学）；University Bamberg（班贝格大学）
本文引入了HOL的依存类型扩展DHOL，保留了HOL的风格与概念框架，并构建从DHOL到HOL的翻译作为HOL定理证明器的前置预处理器，从而实现DHOL的定理证明。
2023-05-24 cs.AI cs.FL cs.LO
Learning to Reason in Large Theories without Imitation
Google Research（谷歌研究院）；IST Austria（奥地利科学技术研究所）
在本文中，我们演示了如何做自动定理证明在一个大的潜在前提知识库的存在，而不学习人类的证明。我们提出了一种探索机制，在深度强化学习场景中混合基于tf-idf（词频-逆文档频率）查找的额外前提。这有助于探索和学习哪些前提与证明新定理相关。我们的实验表明，用这种探索机制训练的定理证明器的性能优于仅在人类证明上训练的证明器。它接近通过模仿和强化学习相结合训练的证明者的性能。我们执行多个实验，以了解使我们的探索方法工作的基本假设的重要性，从而解释我们的设计选择。
2020-06-11 cs.AI cs.LG cs.LO
Proceedings 6th International Workshop on Theorem proving components for Educational software
第六届教育软件定理证明组件国际研讨会（ThEdu'17）于2017年8月6日在瑞典哥德堡举行。它与CADE 26会议有关。感兴趣的主题包括：应用于检查学生输入的自动演绎方法;应用于证明特定问题解决方案的后条件的自动演绎方法;演绎和计算的组合使系统能够提出下一步;动态几何系统专用的自动证明器;数学教育中的证明和证明。Thedu'17是一个充满活力的研讨会，有一个邀请演讲和八个贡献。它触发了手头的后续程序。
2018-03-02 cs.AI cs.CY
Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities
Princeton Language and Intelligence（普林斯顿语言与智能）；Princeton University（普林斯顿大学）；Peking University（北京大学）；Tsinghua University（清华大学）；Amazon（亚马逊）
本文提出 Ineq-Comp 不等式组合推理基准，通过变量复制、代数重写和多步组合测试 LLM 证明器，发现主流模型即使获得子证明仍存在显著组合推理缺陷。
2025-10-20 cs.AI cs.CL cs.LG
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Caltech（加州理工学院）；NVIDIA（英伟达）；MIT（麻省理工学院）；UC Santa Barbara（加州大学圣塔芭芭拉分校）；UT Austin（德克萨斯大学奥斯汀分校）
本文提出开源平台 LeanDojo 和检索增强证明器 ReProver，通过前提检索与困难负样本提升定理证明能力，并在大规模基准上验证其优于基线方法和 GPT-4。
2023-10-27 cs.AI cs.LG cs.LO
Towards a Geometry Automated Provers Competition
CISUC, University of Coimbra（科英布拉大学CISUC）；CISUC/Department of Mathematics, University of Coimbra（科英布拉大学CISUC/数学系）；The Private University College of Education of the Diocese of Linz（林茨教区私立教育大学学院）；University of Coimbra（科英布拉大学）
几何自动定理证明领域通过大量的具体方法和实现、不同的方法（合成、代数、半合成）以及不同的目标和应用（从人工智能领域的研究到教育中的应用）来区分自己。除了通常的效率测量（例如CPU时间），视觉和/或可读证明的可能性也是几何自动定理证明器（GATP）应该衡量的预期输出。在GATP之间开展竞争将为GATP开发人员创建一个测试平台，以改进现有平台并提出新的平台。它还将允许为GATP建立一个排名，“客户”（例如教育电子学习系统的开发者）可以使用该排名来选择针对特定预期用途的最佳实施方式。
2020-02-28 cs.AI cs.PF
miniCodeProps: a Minimal Benchmark for Proving Code Properties
Carnegie Mellon University（卡内基梅隆大学）
研究当前神经定理证明器自动验证简单程序的能力，提出包含201个Lean程序规范的miniCodeProps基准，发现现有最先进LLM证明器在中等和困难属性上几乎完全失败。
2024-10-10 cs.AI cs.LG cs.SE
OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving
School of Mathematical Sciences, Peking University（北京大学数学科学学院）；Huawei Technologies（华为技术有限公司）；Center for Machine Learning Research, Peking University（北京大学机器学习研究中心）；Beijing International Center for Mathematical Research, Peking University（北京国际数学研究中心）
OptProver通过持续训练实现从竞赛数学到本科优化的高效迁移，结合大规模优化数据筛选与偏好学习目标，提升证明效率与鲁棒性，同时在Lean 4上建立新基准并取得优异成绩。
2026-04-28 cs.AI cs.LG
Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers
Carnegie Mellon University（卡内基梅隆大学）；Peking University（北京大学）
本文提出BFS-Prover-V2系统，通过多轮离线强化学习框架和规划器增强的多智能体树搜索，分别解决训练时和推理时的扩展问题，在MiniF2F和ProofNet基准上取得最先进结果。
2025-10-09 cs.AI
