Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction
我们通过构造性类型论的眼镜来看待具有交互式I/O的语言的操作语义。从我们早期的工作，基于共归纳跟踪的语义虽然，我们定义了几个大步骤的语义，而与交互式I/O，基于删除和终止敏感的弱双相似性。这需要在共归纳定义中嵌套归纳定义，这在数学上和在证明助手中实现的观点上都是有趣的。在第一次定义了一个基本的语义的声明中明确的内部动作（延迟）的delictions，我们引入了一个语义的无延迟delictions，基本上消除了有限的延迟序列的飞行从这些delictions是响应。最后，我们还研究了一个语义方面的无延迟的附加选项，一个沉默的分歧选项。这种语义取决于收敛和发散之间的决定，并且只等价于经典的基本语义。我们已经完全正式化了我们在Coq的发展。
2010-08-12 cs.LO cs.PL
Theorem Provers: One Size Fits All?
本文通过证明插入排序的正确性，对Coq和Idris2两个定理证明器进行了定性评估和社区支持比较，旨在帮助用户做出明智的系统选择并为开发者提供参考。
2025-09-18 cs.LO cs.PL
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
Interactive Proof Presentations with Cobra
我们提出了眼镜蛇，一个现代的证明演示框架，利用尖端的演示技术与最先进的交互式定理证明器一起，将形式化的数学作为活动文档呈现。眼镜蛇提供了一种简单的方式来提出证明和一种新颖的方法，礼堂互动。演示文稿由定理证明者现场检查，并且允许演示者和观众进行现场更改。
2017-01-25 cs.LO
Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers
Heriot-Watt University（赫瑞-瓦特大学）；University of Strathclyde（思克莱德大学）；University of Edinburgh（爱丁堡大学）
神经网络的验证是当前自动定理证明中的一个热点问题。进展非常迅速，现在有各种各样的工具可以验证具有数十万个节点的网络的属性。从理论上讲，这为验证使用神经网络组件的大型控制系统打开了大门。然而，虽然工作已经成功地将这些验证的结果，以证明个别系统的更大的属性，目前还没有通用的方法来弥合验证和交互式定理证明（ITP）之间的差距。在本文中，我们提出了车辆，我们的解决方案，这个问题。车辆配备了一个表达领域特定的语言，用于说明神经网络规范，可以编译为验证器和ITP。它通过使用标准ONNX文件作为网络的单一规范表示，克服了以前类似ITP形式化中的可维护性和可扩展性问题。我们证明了它的实用性，使用它连接神经网络验证器Marabou到Agda，然后正式验证由神经网络驾驶的汽车永远不会离开道路，即使面对不可预测的侧风和不完美的传感器。该网络具有超过20，000个节点，因此该证明比关于ITP中的神经网络增强系统的先前证明提高了3个数量级。
2022-02-10 cs.LG cs.LO cs.PL
Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB
Faculty of Mathematics；Natural Science, Institute of Computer Science, Heinrich Heine University Düsseldorf, Universit\" a tsstr. 1, D-40225 D\" u sseldorf
研究将600多条Event-B证明规则编码到Prolog，集成到ProB工具形成交互式证明系统，有证明树可视化等优势，可导入导出，相比Java编码更优，未来目标是获得快速自动证明器。
2026-07-24 cs.AI cs.LO cs.SE
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
Czech Technical University（捷克理工大学）；Radboud University（拉德堡德大学）
我们提出战术家，一个战术学习者和证明的Coq证明助手。Tactician帮助用户做出战术证明决策，同时保留对一般证明策略的控制。为此，Tactician从以前编写的战术脚本中学习，并为用户提供关于下一个要执行的战术的建议，或者完全接管证明合成的责任。Tactician的目标是为用户提供无缝、交互和直观的体验，以及强大和自适应的证明自动化。在本文中，我们从用户的角度对Tactician进行了概述，包括日常使用和在大范围学习时的包依赖管理问题。最后，我们将介绍Tactician作为Coq插件和机器学习平台的实现。
2020-07-31 cs.AI cs.LO
Making $\textsf{IP}=\textsf{PSPACE}$ Practical: Efficient Interactive Protocols for BDD Algorithms
本文提出基于BDD的交互式协议，使证明者高效验证QBF计数问题，实现工具blic，在标准基准上与先进求解器竞争，验证开销小且错误概率极低。
2023-09-06 cs.CC cs.LO
A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
本文全面综述了交互式定理证明器及函数式编程语言 Lean 4，分析了其架构、类型系统与元编程能力，并通过对比和案例研究展示了其在证明自动化等方面的优势及对形式方法的广泛影响。
2025-01-28 cs.LO cs.PL
A heuristic prover for real inequalities
我们描述了一个通用的方法来验证实值表达式之间的不等式，特别是在交互式定理证明中出现的直接推理。与针对特定语言或一类公式的完整方法相反，我们的方法建立了需要异构形式推理的主张，依赖于Nelson Oppen风格的架构，其中专用模块协作并共享信息。因此，该框架是模块化和可扩展的。一个原型实现表明，该方法的工作原理以及各种例子，并补充技术，所使用的当代交互式证明。
2016-01-04 cs.LO cs.MS
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
Beginners' Quest to Formalize Mathematics: A Feasibility Study in Isabelle
使用交互式定理证明器有多难？我们的回应，审查形式化的希尔伯特的第十个问题在伊莎贝尔/HOL进行的本科生研究小组在雅各布斯大学不来梅。我们认为，我们的例子表明，证明助手是可行的初学者形式化数学。为了使该领域更容易访问，我们还调查了学习交互式定理证明器时出现的障碍。从广义上讲，我们主张在数学研究和课程中更多地采用交互式定理证明器。
2021-06-23 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
Lassie: HOL4 Tactics by Example
使用交互式定理证明的证明工程工作已经在软件系统和数学领域产生了几个令人印象深刻的项目。这种努力的一个关键障碍是要求领域专家也是在构造定理证明器中的证明的低层次细节方面的专家。特别地，用户需要选择导致成功证明的一系列策略，这是一项通常需要知道确切名称并使用大量策略的任务。我们提出了Lassie，HOL4定理证明器的战术框架，允许个人用户通过示例定义自己的战术语言，并给出常用的战术或战术组合，以便于记住名称。Lassie的核心是一个可扩展的语义解析器，它允许用户通过定义泛化的过程交互地扩展策略语言。因此，在Lassie中定义策略不需要任何实现自定义策略的知识，而在Lassie中编写的证明保留了HOL4系统提供的正确性保证。我们通过案例研究展示了Lassie如何被新手和更有经验的交互式定理证明器用户用于小型和大型证明，以及我们如何设想它在HOL4教程中缓解学习曲线。
2021-01-04 cs.LO cs.PL
Interactive Visualization of Saturation Attempts in Vampire
形式化方法的许多应用需要对系统属性进行自动推理，例如系统安全性和保密性。为了提高自动推理引擎（如SAT/SMT求解器和一阶定理证明器）的性能，有必要了解这些引擎在生成正式证书（如逻辑证明和/或模型）方面的成功尝试和失败尝试。这种分析是具有挑战性的，因为在证明/模型搜索期间生成了大量的逻辑公式。在本文中，我们专注于饱和为基础的一阶定理证明，并介绍了SATVIS工具的交互式可视化饱和为基础的证明尝试在一阶定理证明。我们建立在世界领先的定理证明器VAMPIRE之上的SATVIS，通过交互式可视化SATVIS中VAMPIRE的饱和尝试。我们的工作结合了自动布局和可视化的衍生图引起的饱和尝试与交互式转换和搜索功能。因此，我们能够分析和调试（失败）证明尝试的吸血鬼。由于其交互式可视化，我们相信SATVIS可以帮助专家和非专家在定理证明理解一阶证明和分析/完善失败的证明尝试的一阶证明。
2020-01-13 cs.LO
Designing a Theorem Prover
一步一步介绍了一个小定理证明程序的代码，介绍了定理证明技术。使用的程序设计语言是标准ML。证明操作上的一阶逻辑，这是简要解释的微积分制定。给出了统一化和逻辑推理的实现方法。该证明器在几个小例子中得到了演示，其中一个例子显示了它的局限性。文章的最后一部分对交互式定理证明的研究现状进行了综述。
2001-03-29 cs.LO
Voting Theory in the Lean Theorem Prover
逻辑学和社会选择理论之间有着长期的富有成果的相互作用的传统。近年来，这种互动主要集中在计算机辅助方法上，如SAT求解和交互式定理证明。在本文中，我们报告了一个框架的发展，正式投票理论的精益定理证明，我们已经应用到验证最近研究的投票方法的属性。虽然以前的应用交互式定理证明社会选择（使用Isabelle/HOL和Mizar）集中在验证不可能定理，我们的目标是涵盖各种结果，从不可能定理到验证特定投票方法的属性（例如，Condorcet一致性、克隆的独立性等）。为了形式化关于添加或删除候选人和选民的投票理论公理，我们在一个变量选举设置中工作，其形式化使用了精益中的依赖类型。
2021-10-16 cs.LO
REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning
Peking University（北京大学）；Renmin University of China（中国人民大学）；Ubiquant（Ubiquant公司）；Beijing International Center for Mathematical Research（北京国际数学研究中心）
REAL-Prover基于检索增强的Lean证明器，通过微调大型语言模型和检索系统，在数学推理任务中取得显著性能提升。
2025-11-24 cs.AI cs.CL cs.LG
A verified algebraic representation of Cairo program execution
加密交互式证明系统提供了一种有效且可扩展的方法来验证区块链上的计算结果。一个证明器构造一个链外证明，证明程序在给定输入上的执行以某个结果终止。然后，证明者发布一个证书，该证书可以被有效地和可靠地验证，以普遍接受的密码学假设为模。该方法依赖于程序执行轨迹的代数编码。在这里，我们报告这样的编码的正确性的验证开罗模型的计算相对于STARK交互式证明系统，使用精益3证明助手。
2021-12-14 cs.CR cs.LO cs.PL
Isabelle: The Next 700 Theorem Provers
Isabelle是一个通用的定理证明器，设计用于各种形式理论的交互式推理。目前，它为构造类型论、各种一阶逻辑、Zermelo-Fraenkel集合论和高阶逻辑提供了有用的证明过程。这一调查伊莎贝尔作为一个介绍文学。它解释了为什么一般的定理证明是有益的。它提供了一个彻底的历史伊莎贝尔，从它的起源在LCF系统。它提出了一个帐户的逻辑是如何表示，说明使用经典逻辑。该方法与爱丁堡逻辑框架进行了比较。几个伊莎贝尔对象逻辑。
2000-10-31 cs.LO
Automatic verification and interactive theorem proving
自动验证是通过计算机验证正确性证书。相关的工具，通常称为证明助手或交互式证明器，提供了一个交互式环境，用于创建正式证书，其正确性可以完全自动地进行评估。这种系统在数学和计算机科学中都有应用，在数学中证书是定理的证明，在计算机科学中证书证明给定软件在其规范方面的正确性。
2017-01-13 cs.LO
The Foundation of a Generic Theorem Prover
Isabelle是一个交互式定理证明器，支持各种逻辑。它将规则表示为命题（而不是函数），并通过组合规则来构建证明。这些操作构成了一个元逻辑（或“逻辑框架”），其中对象逻辑被形式化。伊莎贝尔现在是基于高阶逻辑-一个精确和良好理解的基础。示例说明了使用此元逻辑来形式化逻辑和证明。一阶逻辑的公理被证明是可靠和完备的。后向证明通过关于对象级蕴涵的元推理形式化。高阶逻辑比其他元逻辑有几个实际的优势。许多证明技术是已知的，如休特的高阶统一程序。
2000-10-31 cs.LO
Proceedings Eleventh Workshop on User Interfaces for Theorem Provers
该系列研讨会汇集了对设计，开发和评估自动推理工具的用户界面感兴趣的研究人员，例如交互式证明助手，自动定理证明器，模型查找器，形式化方法工具以及可视化和操作逻辑公式和证明的工具。第11届逻辑学大会在奥地利维也纳举行，是逻辑学领域有史以来规模最大的联合会议维也纳夏季会议的一部分。本会议录包含了八篇被接受在研讨会上发表的论文以及两篇受邀论文。
2014-10-29 cs.HC cs.LO
Nonuniform Coercions via Unification Hints
我们引入了非统一强制的概念，这是通过非统一过程将一种类型的值提升为另一种类型的丰富值。非均匀子是文献中已知的（均匀）子的推广，它们在高阶交互式定理证明器中使用方便的设备（如规范结构，类型类或统一提示）将数学形式化时自然出现。我们还展示了如何在用户级的交互式定理证明器，允许统一提示，自然可以实现非均匀的dronons。
2011-03-17 cs.LO
Iltis: Learning Logic in the Web
Iltis项目提供了一个交互式的、基于网络的系统，用于教授形式方法的基础。其目的是允许简单地纳入新的教育任务;将这些任务纳入更复杂的练习;并允许简单地纳入和级联反馈机制。目前，许多典型的自动推理工作流程的命题逻辑，模态逻辑和一阶逻辑的某些部分的练习都包括在内。最近，Iltis已经达到了一个成熟的水平，大部分的入门逻辑课程可以补充互动练习。在过去几年中，设计了互动式教材样本，并在课程中使用，其中许多课程的学生超过300人。我们邀请所有读者试用Iltis：https://iltis.cs.tu-dortmund.de
2022-05-27 cs.LO
Smart matching
数学形式化中最令人讨厌的方面之一是需要转换概念以匹配给定的现有结果。这类变换通常基于给定科学领域的显著背景知识（主要以等式或同构的形式表示），通常隐含在数学论述中，并且非常希望在交互式证明器中获得类似的行为。本文介绍了基于叠加的实现这一功能内的Matita交互式定理证明器，特别关注所谓的智能应用策略，支持智能匹配的目标和给定的结果。
2010-05-03 cs.LO
Abstraction boundaries and spec driven development in pure mathematics
本文探讨纯数学研究中如何借助交互式定理证明器强化抽象边界与规格驱动开发，从而管理复杂性，并论证其相较传统隐式实践的额外质性优势。
2023-09-26 cs.CY cs.LO math.AG
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
ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers
Brown University（布朗大学）；California Institute of Technology（加州理工学院）
研究形式定理证明生态系统分散问题，提出ITPEval基准测试，涵盖四个主要交互式定理证明器及两种逻辑基础，评估语句和证明翻译，揭示库不匹配是瓶颈，发布相关基础设施和管道，展示多方面评估结果。
2026-07-23 cs.AI cs.LO
Mining State-Based Models from Proof Corpora
交互式定理证明器已被广泛用于推理各种软件/硬件系统和数学定理。使用交互式证明器时的关键挑战是找到一个合适的证明步骤序列，这将导致成功的证明需要大量的人为干预。本文提出了一种自动化的技术，作为输入的成功证明的例子，并推断出一个扩展的有限状态机作为输出。这反过来又可以用来生成新算法的证明。我们的初步实验表明，推断的模型通常是准确的（包含很少的假阳性序列），以这种方式表示现有的证明在指导新的证明时非常有用。
2014-05-14 cs.LO
Isabelle technology for the Archive of Formal Proofs with application to MMT
本文概述了形式证明档案（AFP）背后的Isabelle技术。交互式开发和准交互式构建工作对逻辑（通常是Isabelle/HOL）、数学工具实现的Isabelle/ML和物理系统集成的Isabelle/Scala提出了显著的可扩展性要求--所有这些都集成在Isabelle/PIDE（Prover IDE）中。AFP的持续增长要求Isabelle的性能不断改进。这是一份关于Isabelle 2019（2019年6月）情况的报告，其中包括显着的附加组件，如证明器会话导出和无头PIDE，用于基于语义信息的自动更新。一个示例应用程序是Isabelle/MMT，它能够将所有Isabelle + AFP转换为OMDoc和RDF三元组，但将Isabelle技术重用于其他应用程序是直接的。
2019-06-11 cs.LO
Formalizing Chemical Physics using the Lean Theorem Prover
本研究利用Lean定理证明器形式化Langmuir与BET吸附理论，补充原始缺失的数学约束，构建热力学与运动学证明互操作框架，为科学工程领域理论形式化提供可行路径。
2023-12-08 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
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
Generic Automatic Proof Tools
本书的章节建立了交互式证明工具Isabelle和经典tableau和解析技术之间的联系。伊莎贝尔的经典推理描述和证明了一个扩展的案例研究：教会罗瑟定理的组合。与其他交互式定理证明器相比，Isabelle的经典推理器实现了高度的自动化。
2001-03-29 cs.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
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
Well-Scoped Locally Nameless Representation of Syntax
University of Cambridge（剑桥大学）
本文提出在Agda中使用基于绑定签名的通用代码实现作用域明确的局部无名表示法，证明其在模α转换下与直观名称化语法的等价性，并展示应用示例。
2026-05-09 cs.LO
Proceedings 10th International Workshop On User Interfaces for Theorem Provers
本EPTCS卷收集了2012年7月11日在不来梅举行的智能计算机数学会议（CICM 2012）的一部分，第10届国际研讨会关于定理证明器的用户界面（CIPP 2012）的后续程序。CNOP研讨会系列旨在汇集对设计，开发和评估交互式证明系统接口感兴趣的研究人员，如定理证明器，形式方法工具和其他操纵和呈现数学公式的工具。从1995年开始，到现在可以回顾十七年的历史。本卷中的论文很好地说明了目前在CROP社区中解决的问题的范围;这包括从界面设计（Windsteiger; Dunchev等人）到使用机器学习等技术来帮助用户（Komendantskaya等人）。网络的特点突出（Tankink），新技术需要改变最基本的交互模式（Wenzel）-旧的REPL（读取，评估，打印，循环）交互模式不能利用现代技术，如网络和多核机器。
2013-07-05 cs.HC cs.LO cs.MS
Formally Verified Approximate Policy Iteration
Technische Universität München（慕尼黑工业大学）；King’s College London（伦敦国王学院）
本文用 Isabelle/HOL 形式化验证因子 MDP 上的近似策略迭代算法，并将其精化为可执行实现，同时开发线性规划解认证软件以验证其实用性。
2024-06-11 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
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
STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Stanford University（斯坦福大学）
针对大语言模型形式化定理证明中训练数据不足、奖励稀疏的问题，提出兼具猜想生成与证明双角色的自博弈定理证明器STP，通过迭代互训提升性能，在多个基准数据集上取得整证明生成方法的最优结果。
2025-03-21 cs.AI cs.LG cs.LO
Verified Real Number Calculations: A Library for Interval Arithmetic
在机械证明中，初等函数的实数计算是非常困难的。在本文中，我们将展示如何在一个定理证明器或证明助手中以一种方便、高度自动化和交互式的方式进行这些计算。首先，我们正式建立了初等函数的上界和下界。然后，基于这些界限，我们开发了一个合理的区间算术实数计算发生在代数设置。为了减少区间算术的依赖效应，我们结合了两种技术：区间分裂和泰勒级数展开。这种务实的方法已经开发，并正式验证，在定理证明。正式的开发还包括一组可定制的策略，以自动化涉及实数显式计算的证明。我们的最终目标是提供有保证的数值性质的证明与最小的人类定理证明者的相互作用。
2007-08-28 cs.LO cs.MS
Reconstructing veriT Proofs in Isabelle/HOL
自动定理证明器现在通常用于交互式定理证明器中，以履行越来越多的证明义务。为了保持证明的可信度，必须在证明助手中验证自动找到的证明。我们在这里提出了一个重建过程中的证明助手Isabelle/HOL证明生成的可满足性模理论求解器veriT这是smt策略的一部分。我们详细描述了我们改进的重建方法的架构和我们在设计它时所面临的挑战。我们的实验表明，VeriT驱动的SMT策略经常被Sledgehammer建议为自动解决证明目标的最快方法。
2019-08-26 cs.LO
Isabelle as Systems Platform: Managing Automated and Quasi-interactive Builds
本文提出并实现了一个基于Isabelle/Scala的新构建管理器，取代了旧的Jenkins持续集成系统，以解决可靠性和性能问题，并展示了其利用环境模块支持自动化和准交互式构建。
2024-12-17 cs.LO
Towards Intuitive Reasoning in Axiomatic Geometry
在合成几何中证明引理通常是一项耗时的工作，因为在得到有趣的结果之前需要证明许多中间引理。近年来，自动定理证明器（ATP）的改进意味着它们可以证明许多中间引理。交互式定理证明器Elfe接受用英语写的数学文本，并在ATP的帮助下验证它们。因此，几何文本可以很容易地在Elfe中形式化，只留下由用户导出的证明的基石。这使得教学公理几何的学生没有以前的经验，在形式化的数学。
2019-04-01 cs.HC cs.LO
Translating Scala Programs to Isabelle/HOL
我们提出了一个值得信赖的莱昂验证系统和伊莎贝尔证明助手之间的连接。Leon是一个用于验证Scala程序功能的系统。它使用各种自动定理证明器（ATP）来检查源于输入程序的验证条件（VC）。另一方面，Isabelle是一个交互式定理证明器，用于使用自己的输入语言Isabelle/Isar验证数学规范。用户指定（归纳）定义并手动编写关于它们的证明，尽管有半自动化策略的帮助。这两个系统的集成，使我们能够利用伊莎贝尔丰富的标准库，并给予更大的信心，保证分析程序的正确性。
2016-07-06 cs.LO
Proof in Context -- Web Editing with Rich, Modeless Contextual Feedback
Agora系统是形式数学的一个原型Wiki：一个基于网络的形式数学协作系统，旨在支持正式发展的非正式文档。这个系统需要一个可重用的校对编辑器组件，既用于文档的协作编辑，又用于嵌入到生成的文档中。本文介绍了Agora的异步编辑器的设计，这是通用的，足以支持不同的工具工作的编辑器的内容和提供上下文信息，与交互式定理proverss是一个特殊的，但重要的情况下，详细介绍了Coq定理证明。
2013-07-08 cs.HC cs.LO cs.SE
Recycling Proof Patterns in Coq: Case Studies
University of Dundee（邓迪大学）
交互式定理证明器的发展导致了大型图书馆和各种形式证明基础设施的创建。然而，尽管（或者可能是由于）它们的复杂性，非专家或跨领域的库的重用是一个挑战。在本文中，我们提供了详细的案例研究和评估机器学习工具ML4PG建立交互式数据挖掘的电子图书馆的证明，并提供用户指导的基础上，证明模式在现有的图书馆。
2014-03-07 cs.AI cs.LG cs.LO
ALICE: An Advanced Logic for Interactive Component Engineering
本文介绍了一个概述的验证框架ALICE在其当前版本0.7。它基于通用定理证明器Isabelle [Pau 03 a]。在ALICE中，软件或硬件组件被指定为具有定向通信信道的全状态黑盒。组件通过这些通道发送和接收异步消息。组件的行为通常被描述为一种与观察结果的关系，这种关系以流经其输入和输出通道的消息流的形式出现。支持非定时和定时以及基于状态的、递归的、关系的、等式的、假设/保证的和函数式的规格说明。因此，ALICE是非常适合的形式化和验证的分布式系统建模与此流处理范例。
2014-10-16 cs.LO cs.SE
SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus
为解决一阶自动定理证明器到交互式定理证明器的证明迁移问题，提出 TPTP 推导格式扩展 SC-TPTP，支持序列形式体系，并实现工具库以解析、检查证明并导出至 Coq。
2025-07-15 cs.LO
Physics as Code: From Scans to Theorems with ITP APIs in $SU(5)$ Model Building
DAMTP and Cavendish Laboratory, University of Cambridge（剑桥大学 DAMTP 和卡文迪许实验室）；Department of Computer Science, University of Bath（巴斯大学计算机科学系）
本文提出利用交互式定理证明器API在SU(5)模型构建中实现形式化验证的方法，通过形式化分类和定理推导替代传统扫描，提升模型构建的可靠性与可重用性。
2026-03-30 cs.LO hep-ph hep-th
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning
Australian National University（澳大利亚国立大学）；Data61, CSIRO（澳大利亚联邦科学与工业研究组织Data61部门）
我们提出了一种使用深度强化学习的交互式定理证明（ITP）的新方法。所提出的框架能够学习证明搜索策略以及端到端方式的策略和参数预测。我们制定ITP的过程作为一个马尔可夫决策过程（MDP），其中每个状态代表一组潜在的衍生路径。这种结构使我们能够引入一种新的回溯机制，使代理有效地丢弃（预测）死端推导和重新启动有前途的替代品。我们在HOL4定理证明器中实现了该框架。实验结果表明，该框架优于现有的自动定理证明器（即，锤子）在HOL4中可用。我们进一步阐述了使用消融研究的框架的关键组成部分的作用。
2021-06-17 cs.AI cs.LG cs.LO
