May, 2022

Budge：一种编程语言和定理证明器

PDF
TL;DR基于哥德尔编号和质因数分解的简单编程语言，配合具有显式作用域的循环和定理证明器，可以表示和工作于形式系统。编程语言和定理证明器之间可以相互表示，并提供实例程序和它们的求值。
发现论文，激发创造
  • 为什么你会相信 B？

    使用 Coq 深度嵌入 B 逻辑以检查其正确性和实现 B 工具，实现了 B 逻辑的证明器。

    Feb, 2009

  • LangPro: 自然语言定理证明器

    LangPro 是一种自然语言自动证明器，使用基于专门设计的自然逻辑的分析表格方法，能够推导出前提和假设之间的语义关系，并在 FraCaS 和 SICK 文本蕴含数据集上达到了可与最先进技术相媲美的高结果。

    Aug, 2017

  • EvoGPT-f: 用于基准测试形式数学语言的进化 GPT 框架

    这篇论文通过 EvoGPT-f 回答了关于五种形式数学语言（Lean 3、Lean 4、Coq、HOL 4、HOL Light）和四种标记化方法（字符、词级、字节对编码和 StarCoder 标记器）之间的差异化机器学习能力的定量分析，为进一步开展社区间系统定量和定性比较研究奠定了基础。

    Feb, 2024

  • 基于规则的定理证明器：中学证明入门

    介绍了在中学引入自动推理系统面临的几个瓶颈，讨论了一个基于推理规则和自动方法的实现并使用其进行几何猜想的证明，旨在介绍几何定理的形式证明，以激发学生的兴趣。

    Mar, 2023

  • 自然证明器：基于语言模型的数学证明生成

    通过人工提供或查找背景参考条件，NaturalProver 能够生成数学证明，融合符号和自然语言，提高了下一步建议和生成证明的质量，在某些需要短证明的定理上具有证明能力，并且提供的下一步建议有超过 40% 的正确和有用率。

    May, 2022

  • 用于自动定理证明的生成语言建模

    本文探讨了基于 Transformer 的语言模型在自动定理证明中的应用，提出了基于语言模型的生成能够解决自动定理证明器与人类相比的主要限制之一 —— 原始数学术语的生成问题。我们提出了一个自动证明器和证明辅助工具 GPT-f，使用 Metamath 形式语言，并分析了其性能。 GPT-f 发现了新的简短证明，并被采纳为正式数学社区所接受，这是我们所知道的第一次基于深度学习的系统为正式数学社区做出的贡献。

    Sep, 2020

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

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

    Jan, 2023

  • 开放几何证明社区项目

    本文描述了 Open Geometry Prover Community Project 的目标和实施步骤，旨在将不同自动几何定理证明工具的开发整合到一个共同的 “伞下”，以丰富人们的数学体验。

    Jan, 2022

  • 正式数学陈述课程学习

    本文研究在形式数学中使用专家迭代进行语言建模，使用证明搜索交错学习的方法，以与仅使用证明搜索相比，达到显著优异的性能，成功地解决了高中奥林匹克竞赛等多个具有挑战性的问题，实现了基于 miniF2F 基准的最新技术水平。

    Feb, 2022

  • Draft, Sketch, and Prove: 用非正式证明指导形式化定理证明器

    本文介绍了一种名为 DSP 的方法，可以将非正式证明映射到正式证明草图并指导自动证明器，使其搜索更容易的子问题。实验证明语言模型能够产生结构良好的正式草图，并将其指导自动证明器，从而提高性能达到 39.3%。

    Oct, 2022