DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
DeepSeek-AI（深度求索公司）
本研究推出面向Lean 4的定理证明开源模型DeepSeek-Prover-V1.5，通过增强数据集微调、证明助手反馈强化学习及新型RMaxTS蒙特卡洛树搜索方法，在miniF2F、ProofNet基准上刷新最优成绩。
2024-08-15 cs.AI cs.CL cs.LG
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)
证明助手经常调用自动定理证明器来证明子目标。然而，每个证明器都有自己的证明演算，它产生的证明轨迹往往缺乏许多细节来构建完整的证明。因此，这些痕迹很难检查和重用的证明助手。Dedukti是一个证明检查器，其证明可以翻译为各种证明助手：Coq，HOL，Lean，Matita，PVS。我们实现了一个工具，从TSTP文件中提取TPTP子问题，并使用能够生成Dedukti证明的自动证明器（如ZenonModulo或ArchSAT）在Dedukti中重建完整的证明。此工具是通用的：它不假设证明器产生跟踪的证明演算，并且它可以使用不同的证明器来产生Dedukti证明。我们将我们的工具应用于TPTP库的CNF问题上的自动定理证明器产生的痕迹，并且我们能够为其中的大部分重建证明，显着增加了可以为这些问题获得的Dedukti证明的数量。
2019-08-26 cs.LO
TacticToe: Learning to Prove with Tactics
Czech Technical University, Prague（布拉格捷克理工大学）；University of Innsbruck（因斯布鲁克大学）；Data61
我们实现了一个自动化的战术证明器TacticToe顶部的HOL4交互式定理证明器。TacticToe从人类证明中学习哪种数学技术适用于每种证明情况。这些知识，然后使用一个蒙特卡罗树搜索算法，探索有前途的战术级证明路径。在单个CPU上，时间限制为60秒，TacticToe证明了HOL4标准库中7164个定理的66.4%，而具有自动调度的E prover解决了34.5%。结合TacticToe和E prover的结果，成功率上升到69.0%。
2021-12-02 cs.AI cs.LO
Towards the Integration of an Intuitionistic First-Order Prover into Coq
一个有效的直观的一阶证明集成到Coq是有用的重放证明发现外部自动定理证明。我们提出了一个两阶段的方法：一个直观的证明者生成一个证书的基础上的矩阵表征的直观的一阶逻辑，然后将证书转换成一个序列式的证明。
2016-06-20 cs.LO
AUTO2, a saturation-based heuristic prover for higher-order logic
我们介绍了一个新的定理证明经典高阶逻辑命名为auto 2。证明器的设计是为了在搜索证明时使用人类指定的算法。核心算法是通过从初始假设导出的命题空间进行最佳优先搜索，其中新命题通过称为证明步骤的用户定义函数添加。我们在Isabelle/HOL中实现了证明器，并将其应用于数学和计算机科学的几个形式化项目，展示了它可以在各种可能的证明任务中提供的高水平自动化。
2016-05-24 cs.LO
Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers
Otto-Friedrich-University Bamberg（班贝格奥托·弗里德里希大学）；FU Berlin（柏林自由大学）；University of Greifswald（格赖夫斯瓦尔德大学）；University of Miami（迈阿密大学）
本文报告了使用高阶自动定理证明器（ATP）对Boolos的好奇推断的探索。令人惊讶的是，只有合适的速记符号必须手工提供给ATP才能找到简短的证明。构造简短证明所需的高阶引理由ATP自动发现。考虑到本文的观察和建议，Boolos和相关示例的充分证明自动化现在似乎在高阶ATP的范围内。
2022-12-01 cs.AI cs.LO math.HO
Vibe Coding an LLM-powered Theorem Prover
Griffith University（格里菲斯大学）
Isabellm是一个基于LLM的定理推理论证系统，通过结合分步推证器和证明计划器，实现自动证明合成，并展示了LLM在复杂证明任务中的潜力与挑战。
2026-01-08 cs.AI cs.LO
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
Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant
最近，我们开发了一个自动定理证明射影关联几何。这个证明，基于组合方法使用拟阵，收益饱和使用拟阵规则。它被设计为一个独立的工具，用C语言实现，它以几何配置作为输入，并产生一些Coq证明脚本作为输出：预期定理的陈述，证明定理的证明脚本以及可能的一些辅助引理。在本文档中，我们将展示如何在Coq中嵌入这样一个外部工具作为插件，以便它可以作为一个简单的策略使用。
2021-07-06 cs.LO cs.SE
Importing SMT and Connection proofs as expansion trees
不同的自动定理证明器在不同的演绎系统中推理，从而产生一般不兼容的证明对象。为了理解和分析这些对象，需要研究相应的证明理论，然后在逐个证明者的基础上研究用于表示证明的语言。在这项工作中，我们提出了一个实现，需要SMT和连接证明对象从两个不同的证明和进口他们都作为扩展树。通过在同一个框架中表示证明，所有可用于扩展树的算法和工具（压缩，可视化，微积分证明构造，证明检查等）都可以用于扩展树。可以统一使用。扩展证明也可以用作所产生的证明对象的验证工具。
2015-07-31 cs.LO
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
Open Geometry Prover Community Project
CISUC University of Coimbra（科英布拉大学 CISUC）；CISUC, Department of Mathematics University of Coimbra（科英布拉大学数学系 CISUC）
数学证明无疑是数学的基石。在过去的几年里，计算和推理工具的出现，特别是自动几何定理证明器，极大地丰富了我们的数学经验。为了避免不同的努力，开放几何证明器社区项目的目的是在一个共同的“保护伞”下，为几何自动定理证明器的发展整合不同的努力。在本文中，指定了这种集成的必要步骤，并描述了其中一些步骤的当前实现。
2022-01-03 cs.AI cs.LO
Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers
Key Laboratory of High Confidence Software Technologies (Peking University), Ministry of Education（高可信软件技术教育部重点实验室）；School of Computer Science, Peking University, Beijing, China（北京大学计算机学院）
本文提出Strat2Rocq方法，通过提取LLM的证明策略来增强符号证明器的能力，提升自动化证明效果。
2026-03-04 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
The Foundation of a Generic Theorem Prover
Isabelle是一个交互式定理证明器，支持各种逻辑。它将规则表示为命题（而不是函数），并通过组合规则来构建证明。这些操作构成了一个元逻辑（或“逻辑框架”），其中对象逻辑被形式化。伊莎贝尔现在是基于高阶逻辑-一个精确和良好理解的基础。示例说明了使用此元逻辑来形式化逻辑和证明。一阶逻辑的公理被证明是可靠和完备的。后向证明通过关于对象级蕴涵的元推理形式化。高阶逻辑比其他元逻辑有几个实际的优势。许多证明技术是已知的，如休特的高阶统一程序。
2000-10-31 cs.LO
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
Understanding and Improving Automated Proof Synthesis for Interactive Theorem Provers
School of Software, Northwestern Polytechnical University（西北工业大学软件学院）；School of Computer Science and Ningbo Institute, Northwestern Polytechnical University（西北工业大学计算机科学与宁波研究院）；Research Institute of Trustworthy Autonomous Systems, Southern University of Science and Technology（南方科技大学可信自主系统研究院）；Department of Computer Science and Engineering, Southern University of Science and Technology（南方科技大学计算机科学系）
本文研究了现有证明合成技术无法证明的定理特征，提出基于人类专家证明模式的模式引导战术搜索方法，提升证明成功率和复杂定理的证明能力。
2026-04-27 cs.LO
Certified Connection Tableaux Proofs for HOL Light and TPTP
University of Innsbruck（因斯布鲁克大学）；Radboud University Nijmegen（拉德堡德大学奈梅亨分校）；Czech Technical University in Prague（捷克布拉格技术大学）
近年来，基于有序调节和模型消除的Metis证明器已经取代了HOL 4和Isabelle/HOL中早期内置的通用证明自动化方法。在年度CASC竞赛中，基于连接表的leanCoP系统表现优于Metis。在本文中，我们将展示如何在HOLLight中实现leanCoP的核心算法。leanCoP的旗舰特性，即它的简约核心，导致了一个非常简单的证明系统。这在将MESON证明重构机制扩展到连接表证明方面起着至关重要的作用，提供了证明其证明的leanCoP实现。我们讨论了我们的直接实现使用显式的Prolog堆栈之间的差异，继续传递实现MESON目前在HOLLight和比较他们的性能对所有核心HOLLight目标。由此产生的证明也可以用作通用TPTP证明。我们将其性能与基于分辨率的Metis在TPTP和其他有趣的数据集上进行比较。
2014-10-20 cs.AI cs.LO
A TLA+ Proof System
我们描述了一个扩展的TLA+规约语言与结构的写作证明和证明环境，称为证明经理（PM），检查这些证据。该语言和PM支持增量开发和检查层次结构的证明。PM将证明转换为一组独立的证明义务，并调用一组后端证明者来验证它们。可以使用不同的证明者来核实不同的义务。目前支持的后端是tableau prover Zenon和Isabelle/TLA+，这是Isabelle/Pure中TLA+的公理化。一个完整的TLA+证明的证明义务也可以用来证明Isabelle/TLA+中的定理。
2008-11-12 cs.LO
READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking
Univ. Paris-Sud（巴黎第十一大学）；CNRS（法国国家科学研究中心）
LCF传统的交互式定理证明，这是由米尔纳在20世纪70年代开始，似乎是绑在经典的读取-评估-打印循环的顺序和同步评估的证明命令。我们打破了这个循环，并将读取-评估-打印阶段改造为并行和异步证明处理的模型。因此，我们解释了Isabelle/Scala方法的一些关键概念，以证明交互和集成，以及Isabelle/jEdit Prover IDE作为前端技术。我们希望再次开启关于ITP系统的非平凡交互模型的科学讨论，并帮助其他老派的证明助手走上类似的道路。
2013-07-08 cs.AI cs.HC cs.LO
Proving Theorems using Incremental Learning and Hindsight Experience Replay
DeepMind
传统的一阶逻辑自动定理证明器依赖于速度优化的搜索和许多手工设计的算法，这些算法被设计成在广泛的领域中工作得最好。文献中的机器学习方法要么依赖于这些传统的证明器来引导自己，要么无法达到可比的性能。在本文中，我们提出了一个一般的增量学习算法的训练域特定的证明一阶逻辑没有等式，只基于一个基本的给定子句算法，但使用一个学习子句评分功能。子句被表示为图，并呈现给具有谱特征的Transformer网络。为了解决稀疏性和初始缺乏训练数据以及缺乏自然课程，我们将事后经验重放适应于定理证明，以便即使在没有证据的情况下也能够学习。我们表明，以这种方式训练的证明者可以在证明的数量和质量方面与TPTP数据集上的最先进的传统证明者相匹配，有时甚至超过。
2021-12-20 cs.AI cs.LO
Proceedings of the 12th Workshop on User Interfaces for Theorem Provers
DFKI（德国人工智能研究中心）；U Coimbra（科英布拉大学）；University of Edinburgh（爱丁堡大学）；FU Berlin（柏林自由大学）；Stanford（斯坦福大学）；INRIA Sophia-Antipolis（法国国家信息与自动化研究所索菲亚-安提波利斯分部）
该系列研讨会汇集了对设计，开发和评估自动推理工具的用户界面感兴趣的研究人员，例如交互式证明助手，自动定理证明器，模型查找器，形式化方法工具以及可视化和操作逻辑公式和证明的工具。第12届CNOP在葡萄牙科英布拉举行，是自动推理国际联合会议（IJCAR'16）的一部分。研讨会包括一次特邀演讲、六次提交论文的介绍以及关于推理工具及其用户界面的生动实践会议。这些后续会议记录包含四篇投稿论文，在研讨会后经过第二轮审查后被接受出版，以及邀请论文。
2017-01-24 cs.AI cs.HC cs.LO
ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers
Brown University（布朗大学）；California Institute of Technology（加州理工学院）
研究形式定理证明生态系统分散问题，提出ITPEval基准测试，涵盖四个主要交互式定理证明器及两种逻辑基础，评估语句和证明翻译，揭示库不匹配是瓶颈，发布相关基础设施和管道，展示多方面评估结果。
2026-07-23 cs.AI cs.LO
Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers
CyberAgent；RIKEN AIP（RIKEN先进研究所）
研究通过分析教师证明器生成的数据分布，探讨了分层证明器在重复子证明中通过预测可重用证明图来减少样本需求的机制。
2026-05-07 cs.LG cs.LO stat.ML
STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Stanford University（斯坦福大学）
针对大语言模型形式化定理证明中训练数据不足、奖励稀疏的问题，提出兼具猜想生成与证明双角色的自博弈定理证明器STP，通过迭代互训提升性能，在多个基准数据集上取得整证明生成方法的最优结果。
2025-03-21 cs.AI cs.LG cs.LO
Proceedings Eleventh Workshop on User Interfaces for Theorem Provers
该系列研讨会汇集了对设计，开发和评估自动推理工具的用户界面感兴趣的研究人员，例如交互式证明助手，自动定理证明器，模型查找器，形式化方法工具以及可视化和操作逻辑公式和证明的工具。第11届逻辑学大会在奥地利维也纳举行，是逻辑学领域有史以来规模最大的联合会议维也纳夏季会议的一部分。本会议录包含了八篇被接受在研讨会上发表的论文以及两篇受邀论文。
2014-10-29 cs.HC cs.LO
Formalizing Chemical Physics using the Lean Theorem Prover
本研究利用Lean定理证明器形式化Langmuir与BET吸附理论，补充原始缺失的数学约束，构建热力学与运动学证明互操作框架，为科学工程领域理论形式化提供可行路径。
2023-12-08 cs.LO
Students' Proof Assistant (SPA)
学生证明助手（SPA）旨在教授如何使用像伊莎贝尔这样的证明助手，并教授如何建立可靠的证明助手。从技术上讲，它是一个微型证明助手内的伊莎贝尔证明助手。此外，我们推测，一个好的方法来教结构化证明是一个具体的证明者之间的语义，证明系统和证明者的连接是明确的。Lamport的TLAPS证明助手中的证明与声明式证明器SPA中的证明具有非常相似的结构。为了说明这一点，我们比较证明佩尔蒂埃的问题43 TLAPS，伊莎贝尔/Isar和SPA。我们还考虑佩尔蒂埃的问题34，也被称为安德鲁斯的挑战，鼓励学生发展自己的理由功能，从而获得了很多的洞察力的证明助手。虽然SPA功能齐全，但到目前为止，我们只在少数教育场景中使用过它。
2019-04-01 cs.LO
Hammering Higher Order Set Theory
本文利用自动定理证明器缩短高阶集合论的形式化开发，涵盖算术基本定理等标准定理，并比较不同证明器性能及探讨证明重构。
2025-09-10 cs.LO
Interactive Proof Presentations with Cobra
我们提出了眼镜蛇，一个现代的证明演示框架，利用尖端的演示技术与最先进的交互式定理证明器一起，将形式化的数学作为活动文档呈现。眼镜蛇提供了一种简单的方式来提出证明和一种新颖的方法，礼堂互动。演示文稿由定理证明者现场检查，并且允许演示者和观众进行现场更改。
2017-01-25 cs.LO
Forward Invariant Cuts to Simplify Proofs of Safety
使用演绎技术，如定理证明器，在混合系统的安全验证中有几个优点;然而，最先进的定理证明器需要大量的人工干预。此外，定理证明者在证明任务上取得进展所需的协助类型与系统设计者能够提供的阻力之间通常存在差距。本文提出了一种扩展的KeYmaera，演绎验证工具微分动态逻辑，新技术允许本地推理使用系统设计师的直觉，per-crossing在特定的模式作为证明任务的一部分。我们的方法允许定理证明者利用ward不变量，发现使用数值技术，作为安全性证明的一部分。我们引入了一个新的推理规则的证明演算的KeYmaera，前向不变切割规则，我们提出了一种方法来发现有用的前向不变，然后使用新的切割规则来完成验证任务。我们展示了我们的新方法可以用来完成验证任务，现有的演绎方法，我们的几个例子，包括一个涉及汽车动力系统控制系统的范围之外。
2015-08-10 cs.LO
Metamath Zero: The Cartesian Theorem Prover
随着定理证明器技术使用的扩展，对工具正确性的依赖也在增加。Metamath Zero是一个验证系统，旨在简化逻辑和实现，而不影响验证的效率。它是用自己的语言正式指定的，并支持与其他证明语言之间的大量翻译。本文描述了元路径零的抽象逻辑，本质上是一个多排序的一阶逻辑，以及二进制证明格式和它可以确保基本上线性时间验证的方式，同时仍然是简洁和有效的规模。Metamath Zero目前保持着ZFC中证明的$\mathtt{set .mm}$ Metamath库的最快验证记录（包括Wiedijk的100个形式化目标中的71个），不到200 ms。最终，我们打算用它来验证验证器实现的正确性，直到二进制可执行文件，因此它可以用作更复杂证明系统的信任根。
2020-03-30 cs.LO math.LO
A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
本文全面综述了交互式定理证明器及函数式编程语言 Lean 4，分析了其架构、类型系统与元编程能力，并通过对比和案例研究展示了其在证明自动化等方面的优势及对形式方法的广泛影响。
2025-01-28 cs.LO cs.PL
LogicProof: An Interactive Web-Based Educational Theorem Prover for Natural Deduction and Sequent Calculus across Classical and Constructive Logics
Technical University of Košice（科希策理工大学）
介绍LogicProof这一用于教育的交互式网络定理证明器，支持经典和构造性逻辑的自然演绎与相继式演算，经学生测试能提升对形式证明构建的理解，补充现有教学方法。
2026-07-07 cs.LO
Bootstrapping LCF Declarative Proofs
假设我们一直在接受这样的想法，即LCF系统中的形式化证明应该类似于它们的书面对应物，因此由公式组成，这些公式只为完全验证的证明提供路标。为了切实可行，大多数详细的核查必须通过一般目的的证明程序来进行。现在，如果这些是我们在逻辑规则的内核之外实现的唯一过程，那么定理证明器是什么样子的呢？我们给出了我们的帐户，从头开始在ProofPeer定理证明器中工作，一路上对这个新设置进行观察。
2017-03-15 cs.LO
TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq
ENS de Lyon（里昂高等师范学院）；University of Lorraine, CNRS, Inria, LORIA（洛林大学、法国国家科学研究中心、法国信息与自动化研究所、洛林信息研究与自动化工具实验室）
本文提出TableauxRocq，将自由变量一阶表aux深度嵌入到Rocq证明器中，提供了一个形式化计算系统，证明其正确性，并展示如何利用反射技术将Goeland证明器的Rocq术语和TableauxRocq的证明证书在相似时间内进行验证，且在Skolem化优化下性能更优。
2026-05-16 cs.LO
ENIGMA: Efficient Learning-based Inference Guiding Machine
Czech Technical University in Prague（布拉格捷克理工大学）
ENIGMA是一种基于学习的方法，用于指导基于饱和定理证明器中给定子句的选择。许多证明搜索中的子句根据它们在证明中的参与程度被分为肯定和否定。一个有效的分类模型是在这些数据上训练的，使用快速的基于特征的子句表征。然后，学习的模型与核心证明器紧密相连，并用作新的参数化评估启发式的基础，该启发式提供所有生成的子句的快速排名。该方法在E prover和CASC 2016 AIM基准上进行了评估，显示E的性能大幅提高。
2017-01-23 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
Extensional Higher-Order Paramodulation in Leo-III
University of Luxembourg（卢森堡大学）
Leo-III是一个自动化的定理证明器，用于扩展类型论，具有Henkin语义和选择。通过将基于调节的证明搜索适应于高阶逻辑来启用具有原始等式的推理。证明器可以与多个外部专家推理系统（诸如一阶证明器和SMT求解器）协作。Leo-III与TPTP/TSTP框架兼容，用于输入格式，报告结果和证明，以及推理系统之间的标准化通信，例如，从证明助手（如Isabelle/HOL）内部进行证明重建。Leo-III支持多态一阶和高阶逻辑，所有正常的量化模态逻辑以及不同的道义逻辑中的推理。它的发展开始了TPTP基础设施的不断扩展，以在非经典逻辑中进行推理。
2021-02-28 cs.AI cs.LO cs.SC
Verification of Provers and Solvers
University of Innsbruck（因斯布鲁克大学）
介绍自动推导工具与证明助手的连接方法，通过认证和验证等方式，回顾比较现有方法并提及成功应用。
2026-07-29 cs.LO cs.SC
Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
Department of Computer Science and Technology, Tsinghua University, Beijing, China（清华大学计算机科学与技术系）
利用编译器将大量证明尝试压缩为结构化失败模式，提出一种学习-精炼框架，通过树搜索基于验证器反馈局部修正错误，在可比测试时预算下在PutnamBench上达到最先进性能。
2026-05-29 cs.AI cs.LG cs.LO
Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs
Ohio University（俄亥俄大学）；UNC Charlotte（北卡罗来纳大学夏洛特分校）
数学证明的日益复杂性使得数学家的人工验证在认知上要求很高。自动形式化试图通过将用自然语言编写的证明转换为通过交互式定理证明器可由计算机验证的形式表示来解决这个问题。在本文中，我们介绍了一种语义解析方法，通用Transformer架构的基础上，转换成一个等价的形式化的Coq交互式定理证明语言的基本数学证明。同样的架构也被训练来将用Hoare三元组装饰的简单命令式代码转换成Coq中的形式可验证的正确性证明。在有限的人工和人类书面证明领域上的实验表明，该模型可以很好地推广到训练过程中看不到的中间长度和自然语言的变化。
2023-01-05 cs.AI cs.CL cs.LO
Formal verification of a proof procedure for the description logic ALC
描述逻辑（DL）是一种用于以结构化和形式化的方式表示和推理应用领域知识的语言。为了实现这一目标，已经实施了几个证明器，如RACER和FaCT++，但这些证明器本身尚未获得认证。为了确保这些DL中推导的合理性，有必要正式验证这些推理机应用的推导。形式化方法为证明过程的规范和验证提供了强大的工具，其中包括证明过程的可靠性，完整性和终止性等属性的方法。在本文中，我们提出了一个证明过程的描述逻辑ALC的定义，基于语义tableau方法。我们通过使用Isabelle证明助手证明其可靠性、完备性和终止性来确保证明器的有效性。证明分为两个阶段进行，首先在抽象级别上建立这些属性，然后将它们实例化以用于基于列表的实现。
2013-07-31 cs.LO
Formalization, Mechanization and Automation of Gödel's Proof of God's Existence
Freie Universität Berlin（柏林自由大学）；Vienna University of Technology（维也纳技术大学）
哥德尔的本体论证明已经分析了第一次与前所未有的详细程度和形式的帮助下，高阶定理证明。以下是已经完成的（并按此顺序）：一个详细的自然演绎证明。TPTP THF语法中公理、定义和定理的形式化。使用Nitpick自动验证公理和定义的一致性。自动证明定理与证明LEO-II和Satallax。使用Coq证明助手的逐步形式化。使用Isabelle证明助手的形式化，其中定理（和一些额外的引理）已使用Sledgehammer和Metis自动化。
2017-09-03 cs.AI cs.LO math.LO
Mathematics with large language models as provers and verifiers
CNRS LIX Ecole Polytechnique, Institut Polytechnique de Paris（高等理工学院巴黎理工研究所）
本文提出一种由多个gpt-5实例分别充当证明器与验证器协同工作的协议，使ChatGPT成功证明2025年IMO六题中的五题及约三分之一的数论猜想，并用Lean进行形式化验证以防幻觉。
2025-11-06 cs.AI cs.CL cs.LG
Reconstructing veriT Proofs in Isabelle/HOL
自动定理证明器现在通常用于交互式定理证明器中，以履行越来越多的证明义务。为了保持证明的可信度，必须在证明助手中验证自动找到的证明。我们在这里提出了一个重建过程中的证明助手Isabelle/HOL证明生成的可满足性模理论求解器veriT这是smt策略的一部分。我们详细描述了我们改进的重建方法的架构和我们在设计它时所面临的挑战。我们的实验表明，VeriT驱动的SMT策略经常被Sledgehammer建议为自动解决证明目标的最快方法。
2019-08-26 cs.LO
A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
我们提出了一个综合的两个证明风格的交互式定理证明：程序风格（其中证明是脚本的命令，如在Coq）和声明式风格（其中证明是文本在一个受控的自然语言，如在Isabelle/Isar）。我们的方法结合了声明式风格的优点-编写正式证明的可能性，如正常的数学文本-和程序风格-强大的自动化和帮助形成的证明，包括确定中间步骤的声明。我们的方法是新的，显着不同的方式，程序和声明式的证明风格已经结合在伊莎贝尔，Ssreflect和Matita系统。我们的方法是通用的，可以实现任何程序的交互式定理证明器，无论其架构和逻辑基础。为了展示我们提出的方法的可行性，我们将其完全实现为一个名为miz 3的证明接口，位于HOL Light交互式定理证明器之上。这个接口使用的声明式语言是Mizar系统语言的一个轻微变体，可以用于任何交互式定理证明器，无论其逻辑基础如何。miz 3界面允许轻松访问HOL Light的全套战术和正式库，因此具有“工业实力”。我们的方法提供了一种方法，自动转换任何程序的证明，一个声明的副本，其中转换后的证明是类似的大小，原来的。由于所有的声明式系统本质上都有相同的证明语言，这提供了一种在交互式定理证明器之间移植证明的简单方法。
2012-03-27 cs.LO
Checking Zenon Modulo Proofs in Dedukti
Dedukti被认为是一个通用的证明检查器。它是一个基于lambda Pi演算模的逻辑框架，用作后端来验证来自定理证明器的证明，特别是那些实现某种形式重写的证明。我们提出了一个浅嵌入到Dedukti的证明Zenon模，扩展表为基础的一阶定理证明Zenon演绎模和类型。Zenon Modulo适用于学术和工业项目中的程序验证。我们嵌入的目的是通过分离不可信的证据搜索和可信的证据验证来增加自动生成的证据的可信度。
2015-07-31 cs.LO
A Theorem Prover for Quantum Hoare Logic and Its Applications
量子霍尔逻辑（QHL）在Ying的工作中被引入来描述和推理量子程序。在本文中，我们实现了一个定理证明QHL基于Isabelle/HOL。通过应用定理证明器，验证一个量子程序的规格等价地转化为矩阵之间的顺序关系。由于Isabelle/HOL的局限性，顺序关系的计算通过调用外部Python语言的oracle来解决。据我们所知，这是量子程序的第一个定理证明器。为了证明它的力量，两个著名的量子算法，即，Grover量子搜索和量子相位估计是Shor的多项式时间分解量子算法的关键步骤，利用定理证明器证明了这两个步骤。这是他们两人的第一次机械化证明。
2016-01-15 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
Performing Implicit Induction Reasoning with Certifying Proof Environments
传统的基于显式归纳模式的归纳方法在模式层次上是非约简的、局部的，被证明助手广泛采用。另一方面，自动定理证明器使用的隐式归纳方法允许懒惰和相互归纳推理。本文提出了一种新的策略，使Coq证明助手能够自动进行隐式归纳推理。通过使用一个自动的黑盒方法，拟由集成了Coq的认证证明环境手动证明的命题由Spike隐式归纳定理证明器证明。最终的证明随后被翻译成经过认证的Coq脚本。
2013-07-31 cs.LO
A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
新的拍卖方案不断被设计出来。它们的设计对货物的分配和所产生的收入具有重大影响。但是，如何判断一个新的设计是否具有所需的属性，例如效率，即将货物分配给那些最重视它们的投标人？我们说：通过正式的，机器检查的证明。我们研究了Isabelle，Theorma，Mizar和Hets/CASL/TPTP定理证明器的适用性，以重现拍卖理论的一个关键结果：Vickrey 1961年关于第二价格拍卖性质的定理。基于我们的正式化经验，从拍卖设计师的角度来看，我们给出了什么样的系统用于正式拍卖的建议，并概述了进一步的步骤，一个完整的拍卖理论工具箱。
2013-05-23 cs.GT cs.LO cs.MS
Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
本文提出Lean-auto，一种在Lean 4与自动定理证明器之间的翻译算法，首次在Lean 4中实现基于ATP的通用证明自动化，保证健全性并在Mathlib4上优于现有工具。
2025-05-24 cs.LO
Prover-Adversary games for systems over (non-deterministic) branching programs
University of Birmingham（伯明翰大学）
本文引入 Pudlak-Buss 风格的 Prover-Adversary 博弈来刻画确定性分支程序（BP）和非确定性分支程序（NBP）上的证明系统，并证明了这些证明系统与对应博弈之间的多项式等价性，同时基于此技术得到了 Immerman-Szelepcsenyi 定理的证明复杂性版本。
2026-05-19 cs.CC cs.LO math.LO
