Social Network Processes in the Isabelle and Coq Theorem Proving Communities
University of Edinburgh（爱丁堡大学）
我们确定了在伊莎贝尔和科克社区的主要演员，并描述他们如何影响和影响他们的同龄人。这项工作探讨了社会网络分析的基础，我们希望在ProofPeer项目的背景下，这是一个新的模式，互动的定理证明的基础上合作和社会互动是有用的。
2016-09-22 cs.AI cs.LO cs.SI
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
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
Graph Representations for Higher-Order Logic and Theorem Proving
Google Research（谷歌研究院）
本文首次将图神经网络（GNNs）用于高阶证明搜索，并证明GNNs可以改进该领域的最新成果。交互式高阶定理证明器允许大多数数学理论的形式化，并已被证明对深度学习构成了重大挑战。高阶逻辑是高度表达性的，即使它是结构良好的，具有明确定义的语法和语义，仍然没有建立良好的方法将公式转换为基于图的表示。在本文中，我们考虑了高阶逻辑的几个图形表示，并对高阶定理证明的HOList基准评估它们。
2019-09-13 cs.AI cs.LG cs.LO
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
HolPy: Interactive Theorem Proving in Python
HolPy是一个用Python实现的交互式定理证明系统。它使用高阶逻辑作为逻辑基础。它的主要功能包括广泛使用宏来生成，检查和存储证明，基于JSON的理论格式，以及用于在Python中实现证明自动化和其他扩展的API。一个点和点击为基础的用户界面，实现了通用的定理证明。我们描述了HolPy的主要设计决策、当前应用和未来计划。
2020-01-27 cs.LO
Automatic verification and interactive theorem proving
自动验证是通过计算机验证正确性证书。相关的工具，通常称为证明助手或交互式证明器，提供了一个交互式环境，用于创建正式证书，其正确性可以完全自动地进行评估。这种系统在数学和计算机科学中都有应用，在数学中证书是定理的证明，在计算机科学中证书证明给定软件在其规范方面的正确性。
2017-01-13 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
Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
这是Paral-ITP项目的概述，该项目旨在使证明助手Isabelle和Coq适合多核时代。
2013-05-31 cs.LO
LeanAgent: Lifelong Learning for Formal Theorem Proving
California Institute of Technology（加州理工学院）；Stanford University（斯坦福大学）；University of Wisconsin, Madison（威斯康星大学麦迪逊分校）
针对形式化定理证明中静态LLM泛化性差的问题，提出终身学习框架LeanAgent，通过课程学习、动态数据库和渐进训练持续扩展数学知识，成功证明155个高级定理，并在稳定性和后向迁移上表现优越。
2025-03-06 cs.AI cs.LG cs.LO
ProofPeer - A Cloud-based Interactive Theorem Proving System
ProofPeer致力于成为一个基于云的交互式定理证明系统。在说明了为什么需要这样一个系统之后，本文提出了ProofPeer要取得成功需要满足的一些设计挑战。上下文作为一个解决方案的ProofPeer的用户之间共享证明状态的问题。编年史是作为一种组织和版本上下文的方式引入的。
2012-01-02 cs.DL cs.LO cs.MS
HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving
Tencent Hunyuan Teams（腾讯混元团队）
本研究推出基于Hunyuan 7B微调的自动定理证明模型HunyuanProver，搭配可扩展低成本数据合成框架与引导式树搜索算法，在miniF2F-test等基准上取得SOTA性能，并将开源3万条合成证明数据集。
2025-03-21 cs.AI cs.CL
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
Interactive Visualization of Saturation Attempts in Vampire
形式化方法的许多应用需要对系统属性进行自动推理，例如系统安全性和保密性。为了提高自动推理引擎（如SAT/SMT求解器和一阶定理证明器）的性能，有必要了解这些引擎在生成正式证书（如逻辑证明和/或模型）方面的成功尝试和失败尝试。这种分析是具有挑战性的，因为在证明/模型搜索期间生成了大量的逻辑公式。在本文中，我们专注于饱和为基础的一阶定理证明，并介绍了SATVIS工具的交互式可视化饱和为基础的证明尝试在一阶定理证明。我们建立在世界领先的定理证明器VAMPIRE之上的SATVIS，通过交互式可视化SATVIS中VAMPIRE的饱和尝试。我们的工作结合了自动布局和可视化的衍生图引起的饱和尝试与交互式转换和搜索功能。因此，我们能够分析和调试（失败）证明尝试的吸血鬼。由于其交互式可视化，我们相信SATVIS可以帮助专家和非专家在定理证明理解一阶证明和分析/完善失败的证明尝试的一阶证明。
2020-01-13 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
Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers
本卷包含了在交互式定理证明器（PAR 2010）的偏性和递归研讨会的会议记录，该研讨会于7月15日在英国爱丁堡举行。该研讨会是作为交互式定理证明国际会议（ITP 2010）的卫星研讨会举办的，ITP 2010本身是2010年联邦逻辑会议（FLoC 2010）的一部分。这个研讨会是研究人员在定理证明器中处理部分函数和终止一般（共同）递归的新方法的场所。
2010-12-21 cs.LO
Proceedings Sixth Workshop on Proof eXchange for Theorem Proving
本卷EPTCS包含了2019年8月26日在巴西纳塔尔举行的第六届定理证明证据交换研讨会（PxTP 2019）的会议记录，作为CADE-27会议的一部分。PxTP研讨会系列汇集了研究人员，他们致力于推理系统和形式主义之间的通信，集成和合作的各个方面，特别关注证明。在过去几十年中，计算机辅助推理（包括自动化和交互式推理）取得了进展，使人们有可能建立越来越适用于更广泛问题的推理工具，并能够逐步更快地解决更大的问题。近年来，在较大的系统中，这些工具之间的合作已经证明了减少人工干预的潜力。推理系统之间的合作依赖于理论形式主义和实用工具的可用性，以交换问题，证明和模型。PxTP系列研讨会致力于鼓励这种合作，邀请各方就推理工具之间合作的各个方面做出贡献，无论是自动的还是交互式的。
2019-08-23 cs.LO
Proceedings Seventh Workshop on Proof eXchange for Theorem Proving
本卷EPTCS包含第七届定理证明证据交换研讨会（PxTP 2021）的会议记录，该研讨会于2021年7月11日在美国匹兹堡举行，作为CADE-28在线会议的一部分。PxTP研讨会系列汇集了研究人员，他们致力于推理系统和形式主义之间的通信，集成和合作的各个方面，特别关注证明。在过去几十年中，计算机辅助推理（包括自动化和交互式推理）取得了进展，使人们有可能建立越来越适用于更广泛问题的推理工具，并能够逐步更快地解决更大的问题。近年来，在较大的系统中，这些工具之间的合作已经证明了减少人工干预的潜力。推理系统之间的合作依赖于理论形式主义和实用工具的可用性，以交换问题，证明和模型。PxTP系列研讨会致力于鼓励这种合作，邀请各方就推理工具之间合作的各个方面做出贡献，无论是自动的还是交互式的。
2021-07-04 cs.LO
An Exercise in Invariant-based Programming with Interactive and Automatic Theorem Prover Support
基于不变式的编程（IBP）是一种基于结构的正确的编程方法，其中程序是围绕不变式构建的，这些不变式在实际代码之前被另外制定。Socos是一个专门为支持IBP而构建的程序构建和验证环境。Socos的前端是一个图形化的图表编辑器，允许程序员构建基于不变式的程序并检查其正确性。Socos的后端组件，程序检查器，计算程序的验证条件，并试图自动证明它们。它使用定理证明器PVS和SMT求解器Yices来尽可能多地释放验证条件，而无需用户交互。在本文中，我们首先从用户和系统级的角度描述了Socos环境，然后通过在Socos中构建一个经过验证的堆排序实现来验证IBP工作流。案例研究突出了自动和交互式定理证明在IBP工作流程的三个连续阶段的作用：开发的背景理论，制定程序规范和不变量，并证明最终实现的正确性。
2012-02-22 cs.LO cs.PL
Bit-Blasting ACL2 Theorems
交互式定理证明需要大量的人工指导。证明一个性质包括（1）找出它为什么成立，然后（2）诱使定理证明者相信它，这两个步骤都需要很长时间。我们解释如何使用GL，一个框架，证明有限的ACL2定理与BDD或SAT为基础的推理。这种方法使我们不必深入理解为什么一个性质是真的，并且自动化了承认它为定理的过程。我们使用Centaur Technology的GL来验证x86整数、MMX、SSE和浮点运算的执行单元。
2011-10-21 cs.LO
LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Games
Carnegie Mellon University（卡内基梅隆大学）；Karlsruhe Institute of Technology（卡尔斯鲁厄理工学院）；DePaul University（德保罗大学）
本文利用大语言模型扩展混合系统和游戏的自动定理证明与综合，通过混合游戏符号逻辑和微分游戏逻辑实现对复杂CPS的验证与综合。
2026-09-27 cs.LO
Voting Theory in the Lean Theorem Prover
逻辑学和社会选择理论之间有着长期的富有成果的相互作用的传统。近年来，这种互动主要集中在计算机辅助方法上，如SAT求解和交互式定理证明。在本文中，我们报告了一个框架的发展，正式投票理论的精益定理证明，我们已经应用到验证最近研究的投票方法的属性。虽然以前的应用交互式定理证明社会选择（使用Isabelle/HOL和Mizar）集中在验证不可能定理，我们的目标是涵盖各种结果，从不可能定理到验证特定投票方法的属性（例如，Condorcet一致性、克隆的独立性等）。为了形式化关于添加或删除候选人和选民的投票理论公理，我们在一个变量选举设置中工作，其形式化使用了精益中的依赖类型。
2021-10-16 cs.LO
Designing a Theorem Prover
一步一步介绍了一个小定理证明程序的代码，介绍了定理证明技术。使用的程序设计语言是标准ML。证明操作上的一阶逻辑，这是简要解释的微积分制定。给出了统一化和逻辑推理的实现方法。该证明器在几个小例子中得到了演示，其中一个例子显示了它的局限性。文章的最后一部分对交互式定理证明的研究现状进行了综述。
2001-03-29 cs.LO
Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving
Technische Universität München（慕尼黑工业大学）
当聚合多个代理的偏好时，两个重要的要求是结果应该是经济有效的，并且聚合机制不应该是可操纵的。在本文中，我们提供了一个全面的不可能使用这两个条件的随机聚集机制的计算机辅助证明。更确切地说，我们表明，每一个有效的聚合机制，可以操纵所有预期的效用表示的代理人的喜好。这解决了一个开放的问题，并加强了一些现有的定理，包括声明中所示的特殊领域的分配。我们的证明是通过制定索赔作为一个可满足性问题的谓词从实值算术，然后检查使用SMT（可满足性模理论）求解器。为了验证结果的正确性，SMT求解器返回的最小不可满足约束集被翻译回高阶逻辑中的证明，该证明由交互式定理证明器自动验证。据我们所知，这是SMT求解器在计算社会选择中的首次应用。
2017-09-06 cs.AI cs.GT cs.LO
Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
Beneficial AI Foundation（有益人工智能基金会）
本文引入最大形式化验证基准FVAPPS（含4715样本），将APPS的Python单元测试泛化为Lean 4未证明定理，测试显示Sonnet和Gemini证明正确率为30%和18%，挑战相关社区解决编程问题及正确性规范。
2025-02-08 cs.AI cs.LG cs.LO
The Abella Interactive Theorem Prover (System Description)
Abella是一个交互式系统，用于推理对象语言的各个方面，这些方面已经通过基于语法结构的递归规则正式呈现。Abella使用两级逻辑方法来规范和推理。一个级别由规范逻辑定义，该规范逻辑支持结构语义规则的透明编码，并且还支持它们的执行。第二个层次，称为推理逻辑，嵌入规范逻辑，并允许开发有关规范的属性的证明。这两种逻辑的一个重要特征是，它们利用lambda树语法方法来处理对象语言中的绑定。除此之外，Abella还被用来证明λ演算的正规化性质、λ演算的截容许性、类型唯一性和主体归约性质。本文讨论了Abella的逻辑基础，概述了它支持的定理证明的风格，最后描述了它最近的一些应用。
2008-05-23 cs.LO cs.PL
How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers
近年来，交互式定理证明器的有效性已经增加到一定程度，使得交互过程中的瓶颈转移到效率上：虽然原则上大型和复杂的定理是可证明的（有效性），但用户与系统交互需要花费大量精力（缺乏效率）。我们进行了焦点小组，以评估Isabelle/HOL和键系统的可用性有两个目标：（a）检测交互式定理证明者和他们的用户之间的交互的可用性问题，（b）分析如何评价和调查方法常用的人机交互，如焦点小组和合作评估，适用于特定领域的交互式定理证明（ITP）。在本文中，我们报告我们的经验，使用评估方法焦点小组，以及我们如何适应这种方法，ITP。我们主要在“元水平”上描述我们的结果和结论，即，我们专注于ITP的具体特征对焦点小组的设置和结果的影响。在具体层面上，我们简要总结了我们的案例研究中使用的ITP的可用性的见解。
2014-10-30 cs.HC cs.LO
Verifying Quantum Phase Estimation (QPE) using Prove-It
本文使用通用交互式定理证明助手 Prove-It 验证了量子相位估计（QPE）算法的结果概率声明，展示了其生成形式化认证证明的能力，并与其他系统进行了比较。
2023-04-05 cs.LO quant-ph
Formalizing IMO Problems and Solutions in Isabelle/HOL
国际数学奥林匹克（IMO）可能是世界上最著名的智力竞赛，因此也是人工智能（AI）面临的最大挑战之一。最近制定的IMO Grand Challenge要求建立一个可以在比赛中赢得金牌的AI。我们提出了一些初步的步骤，可以帮助解决这一目标，通过创建一个公共的存储库的机械检查的解决方案的IMO问题的交互式定理证明器伊莎贝尔/HOL。这个知识库由塞尔维亚贝尔格莱德大学数学系的学生在“交互式定理证明导论“课程中积极维护。
2020-10-30 cs.LO
Prove-It: A Proof Assistant for Organizing and Verifying General Mathematical Knowledge
我们介绍了证明它，基于Python的通用交互式定理证明助手设计的目标是使正式的定理证明简单和自然的非正式定理证明（适度的培训）。Prove-它使用高度灵活的基于笔记本的用户界面，该界面使用LaTeX记录交互和证明步骤。我们审查证明，它的表达，判断，定理和证明的高度表达性的表示;证明系统通过构建一个传统的证明矛盾，$\sqrt{2}\notin\mathbb{Q}$ ;并讨论如何避免系统的不一致，如罗素和库里的悖论。附录中提供了关于该系统核心要素的大量文档。目前的发展和未来的工作包括有前途的应用量子电路操纵和量子算法验证。
2020-12-26 cs.LO quant-ph
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
From LCF to Isabelle/HOL
交互式定理证明器在过去的四十年里得到了巨大的发展，从原始的开始到今天的强大系统。在这里，我们专注于Isabelle/HOL及其独特的优势。它们包括自动证明搜索，从一阶定理证明世界借用技术，但也自动搜索反例。它们包括一个高度可读的结构化证明语言和一个独特的交互式开发环境，用于编辑现场证明文档。一切都建立在Robin Milner为Edinburgh LCF设想的基础上：一个证明内核，使用抽象类型来确保可靠性并消除存储证明的需要。与20世纪70年代的研究原型相比，Isabelle是一个实用和通用的工具。它被系统设计师，数学家和许多其他人使用。
2019-07-17 cs.LO
jsCoq: Towards Hybrid Theorem Proving Interfaces
MINES ParisTech PSL Research University（巴黎高等矿业学院PSL研究大学）
我们描述了jsCcoq，一个新的平台和用户环境的Coq交互式证明助手。jsCoq系统以HTML5-ECMAScript 2015规范为目标，它通常在符合标准的浏览器中运行，不需要外部服务器或服务。针对教育用途，jsCoq允许用户立即开始与证明脚本进行交互，这要归功于其自包含的性质。事实上，一个完整的Coq环境与证明脚本一起打包，简化了分发和安装。开始使用jsCoq就像点击一个链接一样简单。当前版本提供了10多个流行的Coq库，并支持流行的书籍，如Software Foundations或Certified Programming with Dependent Type。新的目标平台开辟了新的互动和展示可能性。它还促进了一些新的辅酶相关技术的发展。特别是，我们已经实现了一个新的基于序列化的协议，用于与证明助手进行交互，以及一个新的包格式用于库分发。
2017-01-25 cs.HC cs.LG cs.LO
CircuitProver: Agentic Lean 4 Theorem Proving with Reusable Circuit Proof Library for Hardware Verification
Hong Kong University of Science and Technology(Guangzhou)（香港科技大学（广州））
CircuitProver是基于Lean 4的智能体硬件验证框架，可自动转换硬件设计为Lean模型，通过积累可复用证明知识完成63项基准证明，比普通智能体更高效。
2026-07-31 cs.AR 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
