Sep, 2013

HOL(y)Hammer: HOL Light 的在线 ATP 服务

HTML
PDF
TL;DRHOL(y)Hammer 是一个基于HOL Light编码的在线人工智能/自动定理证明(ATP)服务，提供自动处理基于HOL Light的任意正式开发项目和攻击上传项目的任意猜想的功能。
发现论文，激发创造
  • Mizar 正式化的 ATP 和演示服务

    该论文介绍了自动推理的Mizar（MizAR）服务，该服务将多种自动推理，人工智能和表现工具与Mizar及其编写环境集成在一起。服务基于Mizar语言到一阶ATP系统语言的良好转换，并依赖于在包含数万个可用事实的大型理论应用ATP系统的最新进展。

    Sep, 2011

  • 使用学习辅助的自动化Flyspeck推理

    该论文结合Flyspeck项目中的数学知识与机器学习方法，提出一种能够自动回答数学问题的人工智能系统，并在评估中表现出较高的效率。该系统的实现涉及到HOL Light逻辑的转换以及机器学习的选择和集成。

    Nov, 2012

  • MizAR 40对Mizar 40

    在Mizar的40周年庆典上，我们成功地开发了一个AI/ATP系统，可以在30秒内自动验证最新版本的Mizar数学库(MML)中约40%的定理，成功地实现了对MML的大规模AI/ATP方法的改进，并将最有用的方法高效地实现使其适用于MML中的150,000个公式，从而将训练时间从大规模语料库中缩短至1-3秒，将该方法简单地部署到Mizar用户的在线自动推理服务(MizAR)中。

    Oct, 2013

  • 利用数百万引理的学习辅助定理证明

    该研究实现并运用了一些适当的标准去分析HOL Light和Flyspeck 等正式数学库中的引理图，从而提高了自动化定理证明的效率和准确性。

    Feb, 2014

  • TPTP风格的自动定理证明器在ACL2问题上的初步实验

    本文初步探讨了在ACL2系统上使用外部ATP进行实验的情况，旨在为解决ACL2问题提供外部推理和人工智能系统的初步效用评估。

    Jun, 2014

  • HOL4的前提选择和外部证明器

    本文提出HOL4证明助手的机器学习辅助自动推理和前提选择方法，从定理陈述中提取特征选取前提，通过HOLyHammer将其转换为不同格式，再经由ATPs处理。实验显示该系统在HOL4标准库上具有较高的性能。

    Sep, 2015

  • 使用HOL4策略进行推理学习

    本文介绍了一种用于 HOL4 TacticToe 的策略级自动化方法，将机器学习和翻译技术与自动定理证明辅助工具相结合，以探索不同的策略级证明路径，并且通过组合策略预测和前提选择，在5秒内重新证明了7902个HOL4定理中的39％，效果显著。

    Apr, 2018

  • HOList: 面向高阶定理证明机器学习的环境

    我们提供了一个基于HOL Light定理证明器的开源框架，可以用作强化学习环境；并提出了一个基于深度强化学习的自动定理证明器DeepHOL，它在基准测试中取得了强大的初步结果。

    Apr, 2019

  • Thor: 锤炼联合语言模型和自动定理证明器

    该论文介绍了Thor，一个集成语言模型和自动定理证明器的框架，它采用一种称为“hammers”的方法来选择前提，从而增加了语言模型在PISA数据集上的成功率并解决了相当一部分问题，同时比现有最佳方法在MiniF2F数据集上具有更小的计算量。

    May, 2022

  • MizAR 60 适用于 Mizar 50

    我们发展出了一种AI/TP系统，通过使用基于学习的前提选择方法和增量训练方法，可以自动验证大量Mizar定理，证明效率高达60％和75％。

    Mar, 2023