Learning to Prove Theorems via Interacting with Proof Assistants
Princeton University（普林斯顿大学）
人类通过大量的高级推理和特定问题的见解来证明定理。证明助手提供了一种类似于人类数学推理的形式主义，将高阶逻辑中的定理和证明表示为高级策略。然而，人类专家必须通过将策略输入到证明助手中来手动构造证明。在本文中，我们研究的问题，使用机器学习自动化的互动与证明助手。我们构建了CoqGym，这是一个大规模的数据集和学习环境，包含来自Coq证明助手开发的123个项目的71K人类书面证明。我们开发了ASTactic，这是一种基于深度学习的模型，可以以抽象语法树（AST）的形式生成策略作为程序。实验表明，在CoqGym上训练的ASTactic可以生成有效的策略，并可用于证明以前无法通过自动方法证明的新定理。代码可在https://github.com/princeton-vl/CoqGym上获得。
2019-05-21 cs.AI cs.LG cs.LO
Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
Independent researcher, Cambridge, UK
证明助手提供通过归纳来应用证明的策略，但是这些策略依赖于人类工程师给出的输入。为了使这个费力的过程自动化，我们开发了SeLFiE，这是一种布尔查询语言，用于表示经验丰富的用户关于如何在Isabelle/HOL中应用导入策略的知识：当我们将用SeLFiE编写的归纳启发式应用于归纳问题和归纳策略的参数时，SeLFiE解释器通过检查问题和相关常数的定义。为了研究句法分析和常量定义分析之间的复杂互动，我们引入了定义量词。为了评估，我们建立了一个自动感应证明使用SeLFiE。我们基于347个归纳问题的评估表明，我们的新证明器在1.0秒的超时时间内比相应的基准证明器提高了1.4 x 10^3%，加速的中值为4.48 x。
2022-05-20 cs.AI cs.LO cs.PL
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
University of Innsbruck（因斯布鲁克大学）；Czech Academy of Sciences（捷克科学院）；University of Melbourne（墨尔本大学）
本研究将交互式定理证明中的策略预测建模为归纳逻辑编程任务，通过丰富特征空间学习可解释规则，并用于过滤现有策略选择方法，实验证明能提升性能。
2024-11-02 cs.AI cs.LG cs.LO
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
Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
University of Michigan（密歇根大学）；Amazon Web Services（亚马逊网络服务）
针对 Lean 4 中并行策略搜索因反复重建证明状态导致开销巨大的问题，提出证明状态快照技术，通过一次捕获并复用证明状态，实现 5.6-50 倍加速。
2026-05-27 cs.AI cs.LO
Vibe Coding an LLM-powered Theorem Prover
Griffith University（格里菲斯大学）
Isabellm是一个基于LLM的定理推理论证系统，通过结合分步推证器和证明计划器，实现自动证明合成，并展示了LLM在复杂证明任务中的潜力与挑战。
2026-01-08 cs.AI cs.LO
Reinforced Large Language Model is a formal theorem prover
Alibaba Group（阿里巴巴集团）
针对定理形式化与证明中LLM的应用问题，提出强化学习框架迭代优化预训练LLM，通过生成并对比策略提升准确率，效果优于直接微调LLM。
2025-02-13 cs.AI
Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning
Nanjing University（南京大学）；University of Toronto（多伦多大学）；Peking University（北京大学）；Microsoft Research（微软研究院）；Meta FAIR
本文提出一种神经符号策略生成器，协同LLM的数学直觉与符号方法，分别处理重写和缩放策略，并在161个竞赛不等式上取得最先进性能。
2025-02-27 cs.AI
GamePad: A Learning Environment for Theorem Proving
University of California, Berkeley（加利福尼亚大学伯克利分校）；OpenAI（开放人工智能研究中心）
在本文中，我们介绍了一个名为GamePad的系统，可以用来探索应用机器学习方法的定理证明在Coq证明助手。交互式定理证明器（如Coq）使用户能够以逐步的方式构建机器可检查的证明。因此，他们提供了一个机会，探索定理证明与人类的监督。我们使用GamePad来合成一个简单的代数重写问题的证明，并训练Feit-Thompson定理的形式化的基线模型。我们处理位置评估（即，预测剩下的证明步骤的数量）和策略预测（即，预测下一个证明步骤）任务，这些任务在基于策略的定理证明中自然出现。
2018-12-21 cs.AI cs.LG 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
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
Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study
MIT（麻省理工学院）
研究发现强化学习训练的轻量定理证明器在推理时存在模式崩溃，通过增加采样预算未能提升解题数量，但固定战术骨架调度可显著提升性能，且多样性控制揭示了提示多样性对证明能力的影响。
2026-06-26 cs.AI
Proof Artifact Co-training for Theorem Proving with Language Models
University of Pittsburgh（匹兹堡大学）；OpenAI；IBM Research（IBM研究院）；Google Research（谷歌研究院）；Stanford University（斯坦福大学）；Carnegie Mellon University（卡内基梅隆大学）；CIBO Technologies（CIBO科技）；University of Toronto（多伦多大学）；University of Cambridge（剑桥大学）
在大型形式化数学库中，用于定理证明的模仿学习的标记数据是稀缺的，因为这样的库需要人类专家多年的集中努力才能建立。当将大型Transformer语言模型应用于战术预测时，这是特别具有挑战性的，因为在数据稀缺、容易过拟合的情况下，性能相对于模型大小的缩放很快就会被破坏。我们提出了PACT（{ \bf P}roof { \bf A}rtifact { \bf C}o-{ \bf T}raining），这是一种从内核级证明项中提取丰富的自监督数据的通用方法，用于与通常的战术预测目标一起进行协同训练。我们将这种方法应用于精益，一个交互式的证明助手，它拥有一些迄今为止最复杂的形式化数学。我们仪器精益与神经定理证明器驱动的Transformer语言模型，并表明PACT提高定理证明成功率从32%到48%的测试定理。
2022-03-16 cs.AI cs.LG cs.LO
Process-Verified Reinforcement Learning for Theorem Proving via Lean
KAIST AI（韩国科学技术院人工智能系）
提出利用Lean证明助手提供过程级验证信号，结合GRPO风格强化学习目标，通过策略级监督提升定理证明性能。
2026-06-19 cs.AI
Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings
Rodrigo Mendoza-Smith（罗德里戈·门多萨-史密斯）
通过Lean 4内核级公理依赖追踪，发现选择公理在证明空间中具有可测量的几何关联，服从单参数混合律，并影响神经定理证明器性能。
2026-06-26 cs.AI cs.LG cs.LO
Graph2Tac: Online Representation Learning of Formal Math Concepts
IHES（高等科学研究所）；University of Cambridge（剑桥大学）；IBM Research（IBM研究院）；Radboud University（拉德堡德大学）；Czech Technical University in Prague（捷克布拉格技术大学）
该研究利用形式化数学概念的局部性特性，提出在线k近邻求解器和图神经网络Graph2Tac，在Coq证明助手的定理证明任务上性能显著优于现有通用证明器，且二者互补性强。
2024-06-23 cs.AI cs.LG
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
Lean-STaR: Learning to Interleave Thinking and Proving
Carnegie Mellon University（卡内基梅隆大学）；Tsinghua University（清华大学）
本文提出 Lean-STaR 框架，让语言模型在每个证明步骤前生成非形式化思考，并结合专家迭代提升性能，在 miniF2F-test 上取得 Pass@64 46.3% 的最优结果。
2025-03-15 cs.AI
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
Harnessing Code Agents for Automatic Software Verification
Singapore Management University, Barkhausen Institut（新加坡管理大学, 巴克豪森研究所）
研究利用大语言模型代码智能体进行自动软件验证，将引理交给智能体自由选择方法并置于验证框架，该方法简单有效，能完全覆盖目标引理，在多维度评估中表现出色，可自动为软件开发编写证明。
2026-07-08 cs.AI cs.FL cs.SE
MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
Tencent AI Lab（腾讯AI实验室）；Tencent LLM Department（腾讯大语言模型部门）
针对现有大语言模型逐步定理证明器搜索引导有偏差的问题，提出含数据剪枝策略与多视角树搜索的MPS-Prover，在多个基准上取得最优性能，证明更短更多样。
2025-05-16 cs.AI
SorryDB: Can AI Provers Complete Real-World Lean Theorems?
University of California, Berkeley（加州大学伯克利分校）
提出动态更新的基准SorryDB，包含78个GitHub上的现实形式化项目，评估AI证明者在复杂依赖下的能力，发现当前方法互补，基于Gemini Flash的智能体方法表现最佳。
2026-06-16 cs.AI cs.LG
TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics
Skolkovo Institute of Science and Technology（斯科尔科沃科学技术研究所）；HSE University（高等经济大学）；Artificial Intelligence Research Institute（人工智能研究所）；Sberbank（俄罗斯联邦储蓄银行）
提出TheoremBench基准，通过结构化定理族和细粒度评估指标，揭示当前证明器在复杂定理上的行为偏差。
2026-06-08 cs.AI
BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving
ByteDance Seed（字节跳动种子）；ByteDance Applied Machine Learning（字节跳动应用机器学习）；Stanford University（斯坦福大学）
本文提出BFS-Prover，一种可扩展的最佳优先树搜索框架，通过数据过滤、DPO优化和长度归一化，在MiniF2F上达到72.95%的最先进性能，证明简单方法可媲美复杂搜索。
2025-10-09 cs.AI
Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification
ETH Zürich（苏黎世联邦理工学院）；Princeton Language and Intelligence（普林斯顿语言与智能实验室）；Department of Computer Science, Princeton University（普林斯顿大学计算机科学系）；MiroMind
本文提出Goedel-Code-Prover框架，通过分层证明搜索提升Lean4中代码验证的自动化水平，实现62%的成功率，优于现有基线方法。
2026-08-11 cs.AI cs.SE
Proving Theorems Recursively
Sun Yat-sen University（中山大学）；University of Edinburgh（爱丁堡大学）；City University of Hong Kong（香港城市大学）；HKU（香港大学）；HKUST (Guangzhou)（香港科技大学（广州））；HKUST（香港科技大学）；MBZUAI（穆罕默德·本·扎耶德人工智能大学）
提出递归证明方法POETRY，在Isabelle中逐层搜索可验证草图并推迟子证明，显著提升证明成功率与长度。
2024-05-23 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
Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs
本研究提出满足五项必要条件的Pistis智能体式证明搜索方法，通过OrderDecompose分治搜索生成欧几里得《几何原本》前三卷的忠实形式化Lean证明，其性能优于基线方法，可作为证明检查工具。
2026-08-18 cs.AI
Rethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving
State Key Laboratory for Novel Software Technology（新型软件技术国家重点实验室）
本文提出段级监督策略，通过提取局部连贯的证明段落训练策略模型，提升定理证明的成功率，并在推理阶段减少计算成本。
2026-05-12 cs.AI
FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory
State Key Laboratory of Novel Software Technology, Nanjing University（南京大学新型软件技术国家重点实验室）；School of Artificial Intelligence, Nanjing University（南京大学人工智能学院）；School of Intelligence Science and Technology, Nanjing University（南京大学智能科学与技术学院）；Department of Computer Science, ETH Zurich, Switzerland（瑞士苏黎世联邦理工学院计算机科学系）；School of Computing and Mathematical Sciences, Birkbeck, University of London, UK（伦敦大学伯克贝克学院计算与数学科学学院）
针对大语言模型在数学证明子目标补全能力探索不足的问题，本文提出基于机器学习基础理论的Lean 4基准FormalML，含4937道不同难度题目，评估发现现有证明器仍存局限，需研发更强的LLM定理证明器。
2025-09-26 cs.AI cs.CL
LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
State Key Laboratory for Novel Software Technology, Nanjing University（南京大学计算机软件新技术全国重点实验室）；School of Computing and Mathematical Sciences, Birkbeck, University of London（伦敦大学伯贝克学院计算与数学科学学院）
本文提出可扩展的证明状态探索数据合成方法与自适应束大小策略，用于微调 LLM 策略模型，并在 MiniF2F 和 ProofNet 上取得 Pass@1 最优结果。
2025-05-17 cs.AI
Neural Theorem Proving: Generating and Structuring Proofs for Formal Verification
针对通用定理证明难题，本研究提出含三组件的神经定理证明框架，经两阶段微调训练LLM，在基准测试与AWS S3策略验证场景有效，还整理了新数据集。
2025-10-01 cs.AI cs.FL cs.LG
Hilbert: Recursively Building Formal Proofs with Informal Reasoning
UC San Diego（加州大学圣地亚哥分校）；Apple（苹果公司）
Hilbert结合非正式推理与形式验证，通过递归分解问题并利用反馈优化证明，显著提升在形式证明任务中的性能。
2026-03-16 cs.AI cs.FL cs.LG
ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
University of Texas, Austin, USA（得克萨斯大学奥斯汀分校）
提出ProofWala框架，通过itp-interface库实现与交互式定理证明器的程序化交互，支持多语言证明数据合成、并行证明搜索，并验证了跨语言与跨领域迁移的有效性。
2026-05-29 cs.AI cs.LG cs.LO
ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
Tsinghua University（清华大学）；Huawei Noah’s Ark Lab（华为诺亚方舟实验室）；Shanghai Qi Zhi Institute（上海期智研究院）
ProofAug 通过对模型生成的证明方案进行细粒度结构分析，在多种粒度上为 LLMs 集成自动化方法，并作为即插即用模块与树搜索算法结合，在 miniF2F 上显著提升了 Isabelle 和 Lean 4 中的神经定理证明效率与准确率。
2025-06-06 cs.AI cs.LG
