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
Analysis of Clause set Schema Aided by Automated Theorem Proving: A Case Study [Extended Paper]
CERES方法[8]是最近发展起来的一种用于证明模式的割消方法，证明模式是具有递归构造的证明序列。证明模式可以被认为是一种规避向LK演算添加归纳规则的方法。在这项工作中，我们在LKS演算[8]中形式化了无限鸽子洞原理的示意版本，我们称之为非内射断言模式（NiA-模式），并使用示意CERES方法提供的一些结构来分析从NiA-模式中提取的子句集模式。据我们所知，这是第一次appli-阳离子的构造建立证明分析的证明图式的数学论点，因为它的出版。我们讨论了自动定理证明（ATP）的作用，在示意性的证明分析，以及有关的形式化的NiA模式，即，示意性的分辨率演算的表达能力的示意CERES方法的缺点。最后，我们讨论了ATP在原理图证明分析中的使用。
2015-03-30 cs.LO
Automated Proofs of Unique Normal Forms w.r.t. Conversion for Term Rewriting Systems
范式的概念在各种等价变换中是普遍存在的。合流性是项重写系统的核心性质之一，它涉及到范式的唯一性。另一个比汇合弱的性质是唯一范式w.r.t.转换（conversion）。著名的例子有CRs但没有CR包括TRS组成的S，K，I-规则的组合逻辑补充了各种配对规则（de Vrijer，1999）。最近，自动汇流证明的TRS引起了人们的关注，导致调查的自动化方法（disprove）CR的TRS，一些强大的汇流工具已经开发。相比之下，还没有多少关于自动证明（disproving）不确定性的努力。事实上，有几个工具，能够（反）证明的，此外，只有少数的可识别性标准已详细说明在这些工具。在本文中，我们解决了自动化的方法来证明或证伪给定的TRS。我们报告的自动化的一些标准，到目前为止，也提出了一些新的标准和方法证明或证伪。所提出的方法在汇流校准器ACP上实现（Aoto等人，2009年），并报告了实验评估。
2018-07-03 cs.LO
Top-down Automated Theorem Proving (Notes for Sir Timothy)
本文提出一种自顶向下的自动定理证明方法，主张编码领域概念并模拟人类数学家可能出错的证明方式，以替代传统自底向上的形式化推理路径。
2023-08-08 cs.LO
Axioms vs. rewrite rules: from completeness to cut elimination
本文研究自动定理证明中证明搜索与重写结合时的完备性问题，指出其关键在于为演绎与计算结合的扩展证明概念建立切割消去，从而揭示自动定理证明与证明论之间的新联系。
2023-06-01 cs.LO
Generating theorem proving procedures from axioms of Truncated Predicate Calculus
提出了一种新的自动定理证明方法。多项式成本程序，承认属于一个理论的句子生成的基础上的一组公理的所谓的截断谓词演算是一个子集的标准谓词演算。几个示例性的问题，包括显示所提出的方法的性能。
2019-07-29 cs.LO
Pecan: An Automated Theorem Prover for Automatic Sequences using Büchi Automata
Pecan是一个自动定理证明器，用于推理Sturmian词的属性，Sturmian词是词组合学领域的重要对象。它能够有效地证明关于所有Sturmian词的非平凡数学定理。
2021-02-02 cs.LO
SCTL: Towards Combining Model Checking and Proof Checking
模型检验和自动定理证明是形式化方法的两大支柱。本文从自动定理证明的角度研究模型检验，旨在将自动定理证明的表达性和模型检验的完全自动性结合起来。本文的重点是Kripke模型的时序逻辑性质的验证。本文的主要贡献是：首先定义了一个允许多元谓词符号的扩展计算树逻辑，然后以Kripke模型为参数，为该逻辑设计了一个证明系统，然后设计了一个用于该演算的证明搜索算法和一个新的自动定理证明器来实现它。验证过程是完全自动的，并且在属性不成立时产生一个反例，或者证书实验结果比较以及现有的国家的最先进的工具，在一些基准，包括应用到空中交通管制和设计选择，导致这种效率进行了讨论。
2017-09-30 cs.LO
Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving
University of Potsdam（波茨坦大学）
用一个组合子项表示证明树，这个组合子项可以简化为树，从而使树中细微的重复形式具体化为组合子项的重复子项。在组合子项的DAG表示中，这些直接分解为共享子图。为了搜索证明，可以枚举组合子项，如子句表，与枚举结构的节点相关联的公式的统一交织在一起。为了限制搜索空间，枚举可以基于被定义为参数化组合子项的证明模式。我们在这里介绍这种“组合子项作为证明结构”的方法来自动化的一阶证明，目前的实施和第一个实验结果。该方法建立在一个长期的观点，证明结构植根于凝聚分离和连接方法。它实现了从连接结构演算中已知的功能，迄今为止还没有实现。
2022-09-26 cs.AI cs.LO
An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations
IBM Research（IBM研究院）
本文提出NIAGRA，一种基于名称不变图神经表示的集成方法，用于自动定理证明，通过改进图神经网络和高效集成，在多个数据集上达到最先进性能，迁移学习提升高达28%。
2023-05-15 cs.AI cs.LO
Proceedings 7th International Workshop on Theorem proving components for Educational software
第七届教育软件定理证明组件国际研讨会（ThEdu'18）于2018年7月18日在英国牛津举行。它与2018年联邦逻辑会议（FLoC 2018）有关。ThEdu研讨会系列的主要目的是将有兴趣将计算机定理证明（TP）适应教育需求的开发人员联系起来，并向数学家和数学教育工作者介绍TP作为教育软件的潜力。感兴趣的主题包括：应用于检查学生输入的自动演绎方法;应用于证明特定问题解决方案的后条件的自动演绎方法;演绎和计算的组合使系统能够提出下一步;动态几何系统专用的自动证明器;数学教育中的证明和证明。ThEdu'18是一个充满活力的研讨会，有一场受邀演讲和六篇贡献。它触发了手头的后续程序。
2019-03-29 cs.AI cs.LO
An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic
IBM Research（IBM研究院）；MIT-IBM Watson AI Lab（麻省理工学院-IBM沃森人工智能实验室）；Northwestern University（西北大学）
一阶逻辑中的自动定理证明是一个活跃的研究领域，机器学习成功地支持了这一领域。虽然有各种各样的建议将逻辑公式编码为数字向量-从简单的字符串到更复杂的基于图形的嵌入-但对这些不同编码的比较知之甚少。在本文中，我们研究和实验比较基于模式的嵌入，在当前系统中应用与流行的基于图形的编码，其中大部分没有被认为是在定理证明上下文之前。我们的实验表明，更复杂的基于图的嵌入，产生更有效的搜索策略和更简单的证明，在运行时间方面的优势，更简单的编码方案。为了支持这一点，我们提出了一个详细的分析，在几个方面的定理证明器的性能，不仅仅是证明完成率，从而提供经验证据，以帮助指导未来的研究神经引导的定理证明走向最有前途的方向。
2020-03-15 cs.AI cs.LG cs.LO
TreeWidzard: An Engine for Width-Based Dynamic Programming and Automated Theorem Proving
Stockholm University（斯德哥尔摩大学）；University of Bergen（卑尔根大学）
TreeWidzard通过统一框架实现基于树宽和路径宽的动态规划算法，支持复杂图性质的算法组合及基于树宽的自动定理证明。
2026-05-10 cs.DS cs.LO math.CO
Proceedings Fourth Workshop on Proof eXchange for Theorem Proving
本卷EPTCS包含第四届定理证明的证据交换研讨会（PxTP 2015）的会议记录，该研讨会是2015年8月2日至3日在柏林举行的自动演绎国际会议（CADE 2015）的一部分。PxTP研讨会系列汇集了研究人员，他们致力于推理系统和形式主义之间的通信，集成和合作的各个方面。这些会议记录包含七篇常规论文，以及Georges Gonthier（微软研究院）和Bart Jacobs（鲁汶大学）受邀演讲的摘要。
2015-07-30 cs.LO
Interpolation with Automated First-Order Reasoning
University of Potsdam（波茨坦大学）
从一阶逻辑全自动定理证明角度研究插值法，介绍克雷格插值的两阶段方法及获取基础插值的方式，提及等式编码等贡献，还引入二阶量词消除作为统一插值方法并描述相关算法。
2026-07-08 cs.LO
Evidence Algorithm and System for Automated Deduction: A Retrospective View
Kiev National Taras Shevchenko University（基辅国立塔拉斯·舍甫琴科大学）；Paris 12 University（巴黎第十二大学）
1960年代初，乌克兰基辅开始了一个旨在开发自动定理证明系统的研究项目。该项目的策划者，院士V.Glushkov，洗礼它“证据算法”，EA。这项工程断断续续地持续了40多年。在该项目的框架内，建立了自动演绎系统的俄文版和英文版。它们可能已经被视为有力的定理证明助手。
2010-05-24 cs.AI cs.LO
Automated Analysis of Logically Constrained Rewrite Systems using crest
本文提出工具 crest，用于自动证明逻辑约束重写系统的汇合性与终止性，并通过大量实验验证其有效性。
2025-05-07 cs.LO
A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving
Northwestern University（西北大学）；IBM Research（IBM研究院）；IBM T.J. Watson Research Center（IBM托马斯·J·沃森研究中心）；University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）；MIT-IBM Watson AI Lab（麻省理工学院-IBM沃森人工智能实验室）；IBM Zurich Lab（IBM苏黎世实验室）；The University of Auckland（奥克兰大学）
自动定理证明器传统上依赖于手动调整的算法来指导它们如何执行证明搜索。深度强化学习已经被提出作为一种方法来满足这种推理的需要，然而，它在自动定理证明中的部署仍然是一个挑战。在本文中，我们介绍了TRAIL，这是一个将深度强化学习应用于基于饱和的定理证明的系统。TRAIL利用（a）定理证明器状态的新神经表示和（b）推理选择过程在基于注意力的行动策略方面的新特征。我们通过系统的分析表明，这些机制使TRAIL显着优于以前的基于学习的定理证明器在两个基准数据集的一阶逻辑自动定理证明（证明约15%以上的定理）。
2020-09-16 cs.AI cs.LG cs.LO
Some observations on the logical foundations of inductive theorem proving
本文研究自动归纳定理证明的逻辑基础，提出理论模型分析归纳公理难度，并澄清归纳性概念关系。
2018-04-12 cs.LO math.LO
On the Complexity of Proving Polyhedral Reductions
IMDEA Software Institute（IMDEA软件研究所）；LAAS-CNRS Université de Toulouse INSA CNRS（图卢兹大学国家科学研究中心实验室）
本文提出自动证明Petri网多面体抽象的方法，通过将等价性问题编码为SMT公式，解决无限状态系统下的等价性验证，并探讨多面体简化在可达性问题中的应用。
2024-09-11 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
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
Automated Theorem Proving for Prolog Verification
université de La Réunion（留尼汪大学）
本文提出通过将LPTP的公理转换为一阶公式并利用自动定理证明器验证Prolog程序属性。
2026-01-07 cs.LO cs.PL
Symbolic Computation and Automated Reasoning for Program Analysis
本讲座介绍了如何结合符号计算技术与一阶定理证明可以用于解决自动化程序分析的一些挑战，特别是用于生成和证明软件的逻辑复杂部分的属性。讲座将首先介绍如何计算机代数方法，如Groebner基础计算，量词消去和代数递归求解，帮助我们推断程序循环的性质与非平凡的算术。通过我们的工作推断出的典型属性是循环不变式和约束循环迭代次数的表达式。谈话将描述我们的工作，以产生一阶属性的程序与无界数据结构，如数组。为此，我们使用基于饱和度的一阶定理证明和扩展一阶证明支持程序分析。由于程序分析需要结合数据结构的一阶理论进行推理，因此讲座还讨论了一阶定理证明的新功能，如归纳推理和内置的布尔排序。这些扩展使我们能够直接在一阶逻辑中表达程序属性，从而使用进一步的一阶定理证明器来推理程序属性。
2017-04-11 cs.LO cs.PL
Local Look-Ahead Guidance via Verifier-in-the-Loop for Automated Theorem Proving
Language Technology Lab, University of Amsterdam（阿姆斯特丹大学语言技术实验室）；Qualcomm AI Research（高通人工智能研究）
针对自动定理证明中奖励稀疏与计算成本高的问题，提出验证器在环的局部前瞻引导方法，利用Lean在每一步提供中间反馈，实验表明能全局提升推理准确性与效率。
2025-06-24 cs.AI cs.CL cs.LG
State Canonization and Early Pruning in Width-Based Automated Theorem Proving
Stockholm University（斯德哥尔摩大学）；University of Bergen（卑尔根大学）
本文提出基于宽度的自动定理证明框架，通过状态规范化和早期剪枝技术，有效减少搜索状态并验证图论猜想的可行性，展示了该方法在三角形自由图着色猜想中的应用。
2026-05-10 cs.CC cs.DS cs.LO
Machine Learner for Automated Reasoning 0.4 and 0.5
University of Innsbruck（因斯布鲁克大学）；Radboud University Nijmegen（拉德堡德大学奈梅亨分校）
机器学习自动推理（MaLARea）是一个学习和推理系统，用于在大型正式库中进行证明，在攻击新猜想时，可以使用数千个定理，并且可以使用大量相关问题和证明来学习特定的定理证明知识。该系统的最新版本以较大优势赢得了2013年CASC LTB竞赛。本文描述了MaLARea中使用的方法背后的动机，讨论了评估此类系统的一般方法和问题，并描述了Mizar@Turing100和CASC'24版本的MaLARea。
2014-05-28 cs.AI cs.LG cs.LO
MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification
MSC-180是一个用于评估自动形式定理证明的基准，揭示了当前基于LLM的定理证明者在数学领域覆盖和泛化能力上的不足。
2025-12-20 cs.AI cs.LO
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)
本文针对依赖类型高阶逻辑DHOL提出原生表推演自动推理规则，并在Lash中实现，借助DHOL到HOL的可靠完备翻译保证完备性，实验表明其性能优于在翻译结果上运行的主流HOL证明器。
2024-10-18 cs.LO
Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
D-CHAB, ETH Zurich, Zurich, Switzerland.；D-INFK, ETH Zurich, Zurich, Switzerland.；ETH AI Center, Zurich, Switzerland.；University of Pennsylvania, PA, USA.；Independent Researcher.
本文提出利用理论计算机科学作为可扩展的严谨证明问题来源，通过算法定义自动生成大量挑战性定理-证明对，展示了在Busy Beaver问题和混合布尔算术问题上的应用，并揭示了自动定理证明在复杂问题上的局限性。
2026-05-18 cs.AI cs.CL cs.LG
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
Progress in Computer-Assisted Inductive Theorem Proving by Human-Orientedness and Descente Infinie?
Saarland Univ.（萨尔兰大学）
本文简要回顾了自动归纳定理证明和计算机辅助数学归纳法的发展历史。我们认为，目前对这一领域进展的低期望是错误的狭隘历史预测造成的。我们的主要动机是解释-在一个抽象的，但希望充分描述的水平-为什么我们相信，在该领域的未来进展是从以人为本的结果和下降无限。
2010-09-01 cs.AI cs.LO
PIE -- Proving, Interpolating and Eliminating on the Basis of First-Order Logic
PIE是基于一阶逻辑的自动推理的嵌入Prolog的环境。它包括一个通用的公式宏系统，并支持创建散布宏定义、推理机调用和LaTeX格式的自然语言文本的文档。支持调用各种推理机：外部证明器以及PIE的子系统，其中包括预处理器，基于Prolog的一阶证明器，Craig插值方法和二阶量词消去方法。
2019-08-29 cs.AI cs.LO
Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
University of York（约克大学）
本文提出概率统一关系（ProbURel）框架，基于统一编程理论形式化概率编程的语法与语义，扩展子分布与超分布处理构造性语义，并在Isabelle/HOL中机械化以支持定理证明自动推理。
2024-09-26 cs.LG cs.LO cs.PL
Checking the Quality of Clinical Guidelines using Automated Reasoning Tools
Institute for Computing and Information Sciences（计算与信息科学研究所）；Radboud University Nijmegen（拉德堡德大学奈梅亨分校）
临床指南的质量要求可以通过借用溯因诊断理论的图式来表示，使用时序逻辑来建模指南中表达的面向时间的方面。以前，我们已经表明，这些要求可以使用交互式定理证明技术进行验证。在本文中，我们探讨了如何将这种方法可以映射到设施的分辨率为基础的定理证明，水獭，和一个互补的程序，搜索有限模型的一阶语句，梅斯。它表明，检查质量的准则所需的推理可以映射到这样的全自动定理证明设施。以这种方式研究关于2型糖尿病的实际指南的医疗质量。
2008-06-02 cs.AI cs.LO cs.SC
BliStrTune: Hierarchical Invention of Theorem Proving Strategies
Czech Technical University（捷克技术大学）
为特定的问题集发明有针对性的证明搜索策略是一项艰巨的任务。国家的最先进的自动定理证明器（ATP），如E允许大量的用户指定的证明搜索策略描述在一个丰富的领域特定的语言。先前提出了几种自动发明ATP策略的机器学习方法。其中之一是Blind Strategymaker（BliStr），这是一个自动发明ATP策略的系统。在本文中，我们介绍BliStrTune -BliStr的层次扩展。BliStrTune允许探索更大的E策略空间，通过交错搜索高级别的参数与他们的微调。我们使用BliStrTune发明新的策略的基础上，也针对大型ITP库的问题，新的条款权重函数。我们发现，新的策略显着提高E的性能在解决问题的Mizar数学图书馆。
2016-11-26 cs.AI cs.LG cs.LO
On Herbrand Skeletons
Herbrand定理在证明论和计算机科学中都有着重要的地位。给定一个Herbrand骨架，它基本上是一个指定矩阵的析取计数的数字，我们希望得到一个可计算的界限，使析取成为拟自治的项的大小。这是逻辑学中的一个重要问题，特别是在证明的复杂性中。在计算机科学中，特别是在自动定理证明中，人们希望有一种算法，可以避免在证明定理时对存在替换公理的猜测。Herbrand的定理形成了自动定理证明的基础，对于给定的数$n$，我们希望有一个算法，它可以找到矩阵的$n$析取中的项，而仅仅是矩阵的形状。本文的主要结果是这两个问题都有负解。
2019-09-30 cs.LO math.LO
Proceedings 11th International Workshop on Theorem Proving Components for Educational Software
Jerusalem College of Technology（耶路撒冷理工学院）；Bar Ilan University（巴伊兰大学）
ThEdu系列追求从中学数学的直观方式到STEM教育中更正式的主题方法的平稳过渡，同时通过利用定理证明技术的力量来支持这种过渡。以下是对本卷如何有助于这一事业的简要说明。第11届教育软件定理证明组件国际研讨会（ThEdu'22），是第八届联邦逻辑会议的卫星活动（FLoC 2022），2022年7月31日至8月12日，以色列海法ThEdu'22是一个充满活力的研讨会，Thierry Dana-Picard邀请了两个演讲（耶路撒冷技术学院，耶路撒冷，以色列）和Yoni Zohar（巴伊兰大学，特拉维夫，以色列）和四个贡献。随后发出了公开征集文件的呼吁，吸引了七份意见书。这些意见书已被我们的审查员接受，他们共同编写了至少三份关于每一份意见书的详细报告。本卷收集了由此产生的订正文件。本卷中的贡献忠实地代表了Thedu的广泛范围，从那些更专注于自动化演绎研究的人，不要忘记在教育环境中可能的应用程序，到那些专注于应用程序的人，在教育环境中，自动化演绎工具和方法。我们，卷的编辑，希望这本论文集将进一步促进基于定理证明的软件的发展，并将允许提高计算机科学家，数学家和教育利益相关者之间的相互理解。在本卷付印的同时，ThEdu研讨会的下一个版本正在准备中：ThEdu'23将是第29届自动演绎国际会议（CADE 2023）的卫星活动，2023年7月1日至4日，意大利罗马。
2023-03-09 cs.AI cs.CY cs.LO
From Width-Based Model Checking to Width-Based Automated Theorem Proving
Stockholm University（斯德哥尔摩大学）；University of Bergen（卑尔根大学）
本文提出一个通用框架，将大量基于宽度的模型检验算法转换为用于测试图论猜想在有限宽度图类上有效性的算法，改进了理论上的上界。
2024-09-15 cs.AI cs.DM cs.DS
Proceedings The 13th International Workshop on Theorem proving components for Educational software
Carnegie Mellon University（卡内基梅隆大学）
本卷收录第13届ThEdu研讨会8篇论文，展示定理证明技术在STEM教育中的自动演绎研究与应用，以促进定理证明软件发展及跨领域理解。
2025-05-07 cs.AI cs.LG cs.LO
Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic
PIE是基于一阶逻辑的自动推理的嵌入Prolog的环境。它的主要重点是公式，作为通过公式宏结构化的复杂形式化的组成部分，以及作为推理任务的输出，如二阶量词消去和克雷格插值。它支持基于文档的工作流，这些文档散布着宏定义、推理机调用和LaTeX格式的自然语言文本。从各种例子出发，本文讨论了PIE的特点和应用的可能性，以及目前的局限性和未来的研究问题。
2020-02-24 cs.AI cs.LO
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
The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs
微积分是一种证明一阶逻辑中陈述有效性的形式主义。它通常用于计算机科学数学逻辑模块。形式证明在微积分中是有限的树，通过连续地将证明规则应用于公式，从而逐步简化它们。学生们经常在诸如形式逻辑和形式证明等主题所涉及的数学形式和抽象层次上挣扎。这些困难可以归类为句法或语义。在句法层面上，学生需要理解什么是正确形式的证明，如何在不脱离微积分的数学框架的情况下应用规则（例如在纸上），等等;除此之外，在语义层面上，学生需要掌握找到正确证明的策略。序贯微积分训练器是一个工具，旨在帮助学生学习正式证明给定语句的技术。在本文中，我们描述的教学动机背后的工具和技术，用于解决问题的句法以及语义层面上。
2018-03-05 cs.CY 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
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
Automated Termination Analysis for Logic Programs with Cut
可终止性是逻辑程序的一个重要性质，也是研究得很好的性质。然而，几乎所有的自动终止分析方法都集中在确定的逻辑程序上，而实际的Prolog程序通常使用cut运算符。本文介绍了一种新的预处理方法，它能自动地将Prolog程序转换成无割的逻辑程序，其中无割程序的终止意味着原程序的终止。因此，在该预处理之后，可以应用用于证明确定逻辑程序的终止的任何技术。我们在我们的终止证明程序AProVE中实现了这种预处理，并成功地进行了广泛的实验。
2010-07-28 cs.LO cs.PL
Property Invariant Embedding for Automated Reasoning
University of Innsbruck（因斯布鲁克大学）；Czech Technical Univ. in Prague（布拉格捷克理工大学）
自动推理和定理证明最近已经成为机器学习的主要挑战。在其他领域，能够抽象不重要的转换的表示，例如视觉中的平移和旋转抽象，变得越来越普遍。然而，嵌入用于学习定理证明的数学公式的标准方法还不能处理许多重要的变换。特别是，嵌入以前看不见的标签，经常出现在定义编码和Skolemization，到目前为止已经非常弱。在已知符号之间传递知识时也会出现类似的问题。我们提出了一种新的编码公式，扩展现有的图神经网络模型。这种编码仅通过图中的节点来表示符号，而不向网络提供原始标签的任何知识。我们在这些节点之间提供了额外的链接，使网络能够恢复意义，从而正确地嵌入这些节点，而不管给定的标签。我们测试所提出的编码在一个自动定理证明的基础上的tableaux连接演算，并表明，它提高了迄今为止使用的最佳表征。编码进一步评估的前提选择任务和新引入的符号猜测任务，并正确预测65%的符号名称。
2019-11-27 cs.AI cs.LG cs.LO
Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
State Key Laboratory for Multimedia Information Processing, School of Computer Science, PKU-Anker LLM Lab, Peking University（信息处理国家重点实验室，计算机科学学院，PKU-Anker LLM实验室，北京大学）；Huawei Technologies Co., Ltd.（华为技术有限公司）；School of Software & Microelectronics, Peking University（软件与微电子学院，北京大学）；School of Electronics Engineering and Computer Science, Peking University（电子工程与计算机科学学院，北京大学）
本文提出DAP框架，通过LLM自然语言推理与自我反思发现答案，并将硬模式问题转换为易模式问题以提升自动定理证明性能，实现了CombiBench和PutnamBench上的显著提升。
2026-04-17 cs.AI cs.CL cs.LO
Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology
Otto-Friedrich-Universität Bamberg（奥托-弗里德里希-班贝格大学）；Freie Universität Berlin（柏林自由大学）；University of Luxembourg（卢森堡大学）
本文介绍基于LogiKEy方法，利用经典高阶逻辑和证明助手Isabelle/HOL教授多元逻辑，通过系列谜题展示从命题到道义逻辑的教学路径，并反驳单一主义质疑，强调其可移植性。
2026-10-07 cs.AI cs.LO
APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning
Huawei Hong Kong Research Center（华为香港研究中心）；Department of Computer Science & Engineering, The Chinese University of Hong Kong（香港中文大学计算机科学与工程系）
提出APOLLO框架，结合Lean编译器与LLM实现自动证明修复，在miniF2F等基准上以低采样预算大幅提升准确率并刷新最优纪录。
2025-11-04 cs.AI cs.LO
Proceedings 8th International Workshop on Theorem Proving Components for Educational Software
本EPTCS卷包含ThEdu'19研讨会的会议记录，该研讨会于2019年8月25日在巴西纳塔尔举行，作为CADE-27的卫星活动。Thedu'19代表了Thedu系列的第八部分，是一个充满活力的研讨会，由Sarah Winkler邀请演讲，四个贡献，以及第一版的几何自动证明器竞赛。讲习班结束后，公开征集论文，共收到七份论文，其中六份已被审查人员接受，并收录在本报告的后续卷中。ThEdu系列追求从中学数学的直观方式到STEM教育中更正式的主题方法的平稳过渡，同时通过利用定理证明技术的力量来支持这种过渡。卷的编辑希望，这一系列的论文将进一步促进基于定理证明的软件的发展，并将合作提高计算机数学家和教育利益相关者之间的相互理解。
2020-02-27 cs.AI cs.LO
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
University of Toronto（多伦多大学）；Vector Institute（向量研究所）
在学习辅助的定理证明中，最关键的挑战之一是推广到与训练时不同的定理。在本文中，我们介绍了INT，一个不等式定理证明基准，专门设计来测试代理的泛化能力。INT基于一个生成定理和证明的过程;这个过程的旋钮允许我们测量6种不同类型的泛化，每种类型都反映了自动定理证明的独特挑战特征。此外，与以前的学习辅助定理证明基准不同，INT提供了一个轻量级和用户友好的定理证明环境，具有快速模拟，有利于执行基于学习和基于搜索的研究。我们引入了基于学习的基线，并使用基准在泛化的6个维度上对其进行评估。然后，我们评估相同的代理增强蒙特卡罗树搜索（MCTS）在测试时，并表明MCTS可以帮助证明新的定理。
2021-04-03 cs.AI cs.LG cs.LO
On Quantified Modal Theorem Proving for Modeling Ethics
Rensselaer Polytechnic Institute（伦斯勒理工学院）
在过去的十年中，形式逻辑已被用来模拟广泛的伦理理论和原则，目标是在自治系统中使用这些模型。用于建模伦理理论的逻辑及其自动推理机的要求与用于其他目的的模态逻辑不同，例如用于时间推理。为了满足这些要求，需要研究新的自动化检验方法。特别是，一个量化的模态逻辑，道义认知事件演算（DCEC），已被用来模拟各种版本的学说的双重效果，akrasia和美德伦理。使用一个片段的DCEC，我们概述了这些不同的特点，并提出了一个草图的算法，可以帮助某些方面证明自动化DCEC。
2019-12-30 cs.AI cs.LO
Lightweight Interactive Proving inside an Automatic Program Verifier
在形式化方法中，演绎验证方法允许在关键软件上建立最强可能的形式化保证。缺点是设计适当的正式规范和成功履行所需的证明义务所需的人力成本。为了在工业软件开发环境中推广演绎验证，必须提供从简单和自动化方法逐步过渡到演绎验证的方法。SPARK环境，用于开发用Ada编写的关键软件，通过提供自动化工具来正式证明某些代码满足Ada合同中表达的要求，从而实现了这一目标。在利用自动证明器来履行证明义务的程序验证器中，需要一些额外的用户与证明任务的交互：或者帮助分析证明失败的原因，或者最终履行最先进的自动证明器无法达到的验证条件。在SPARK中添加交互式证明功能似乎很复杂，因为证明工具链使用了独立的中间验证工具Why 3，它足够通用，可以接受不同输入语言的多个前端。本文报告了我们的方法来扩展Why 3与交互式证明功能，并与一个通用的客户端-服务器基础设施，允许集成到一个外部的，前端的图形用户界面，如SPARK的证明交互。
2018-11-27 cs.LO cs.PL cs.SE
