Oct, 2016

高效的认证分辨率证明检查

PDF
TL;DR该论文介绍了一种新的命题证明追踪格式，可以消除复杂的处理，从而实现有效（正式）证明检查。通过使用 C 实现证明检查器来证明该格式的好处。然后在 Coq 中形式化命题证明检查的理论，并从形式化中提取出该格式的一个正确性自证明的证明检查器。使用 280 个不可满足的实例对其性能进行了评估，并使用该格式正式验证了布尔勾股三元组猜想的最近 200 TB 的证明。
发现论文，激发创造
  • 高效的认证 RAT 验证

    这篇论文介绍了一种名为 LRAT 的新型证明格式，它在 DRAT 基础上新增了 hints 以便于快速的验证算法，并可以使用定理证明器等已验证的系统来实现。作者还在 Coq 和 ACL2 中实现了两个经过认证的 LRAT 验证程序。

    Dec, 2016

  • 证明结构研究

    提出并阐述了一种新的证明操纵和分析形式主义，为证明检索方式提高了效率，实现了较短证明的自动化，特别是在首阶问题上的历史证明中进行了一项全面的形式重建分析。

    Feb, 2023

  • 受限伪命题逻辑的解析

    本研究展示了如何将命题演绎推广到受限伪命题逻辑（CPPL）中，这是将自然数与少量约束符号插入命题逻辑字母表并相应地调整底层语言所导致的扩展。虽然该限制被认为是不必要的，但本研究提供了一种建设性证明，证明了 CPPL 的广义演绎推理是正确而完整的。

    Jun, 2023

  • 迈向自动可读的直尺和圆规构造证明

    本论文展示了我们的三角形构造求解器 ArgoTriCS 如何与一阶逻辑和连续逻辑的自动定理证明器合作，从而生成既可读性强的合成正确性证明，又具有形式化特性的构造解决方案。这些证明依赖于许多高级引理，我们的目标是从几何的基本公理中形式化证明它们全部。

    Jan, 2024

  • 可信的正式自然语言规范

    该论文表明，通过使用现有的证明助理，可以以与建立证明助理自身的信任和可审计性原则相一致的方式，构建对自然语言表达的规范的支持。我们在 Lean 证明助理内实现了一种方式，以可扩展的正式英语子集提供规范，并自动将其翻译成正式的命题。我们的方法是可扩展的（对语法结构没有永久限制），模块化的（允许在库中分发有关新词的信息），并且生成解释了每个词的解释方式以及如何使用句子结构来计算含义的证明证书。我们将原型应用于从一本流行教材中翻译各种正式规范的英文描述；在仅需进行小幅修改的情况下，借助一个适度的词汇表，所有规范都能被正确翻译。

    Oct, 2023

  • 使用形式化数学开发无缺陷的机器学习系统

    通过可交互的证明助手，开发者能够证明机器学习系统的正确性，这种方法暴露了所有的实现错误，并通过 Certigrad 实现了优化的随机计算图，并生成了一个机器可验证的证明，证明了系统采样的梯度是数学梯度的无偏估计方法。

    Jun, 2017

  • 基于自动正式化的数学和代码正确性研究：基础证明实验

    本研究介绍了一种基于 Universal Transformer 体系结构的语义解析方法，可以将基本数学证明转化为 Coq 互动定理证明器中的等效形式，以及将装饰有 Hoare 三元组的简单命令式代码翻译成 Coq 中的形式验证证明。通过人工和人工写作证明的有限领域的实验表明，这些模型对于训练期间未看到的中间长度和自然语言变化具有很好的泛化能力。

    Jan, 2023

  • 电路评估的时间最优交互证明

    本文描述了一种交互证明协议的改进方法，可以实现具有正确性保证的计算，效率比现有的实现提高了 200 倍，在矩阵乘法和数据并行计算方面也有应用。

    Apr, 2013

  • 证明的最大可满足性预处理

    基于 Bool 型可满足性的进展，极大可满足性已成为解决 NP 困难优化问题的可行方法，但确保 MaxSAT 求解器的正确性仍然是一个重要问题。本文介绍如何使用伪布尔型证明记录来验证广泛的现代 MaxSAT 预处理技术的正确性，通过结合 VeriPB 和 CakePB 工具，实现对输入和预处理输出 MaxSAT 问题实例具有相同最优值的正式验证，经对应用 MaxSAT 基准测试的广泛评估表明，我们的方法在实践中是可行的。

    Apr, 2024

  • 通过 Cube-and-Conquer 解决和验证布尔型勾股三元组问题

    通过使用组合了前瞻和 CDCL 求解器的混合 SAT 方法以及特定前瞻启发式方法，我们采用 Cube-and-Conquer 范例解决了布尔勾股三元数问题，并产生并验证了大于 68 GB 的压缩证书。

    May, 2016