HOL(y)Hammer: HOL Light 的在线 ATP 服务
该论文介绍了自动推理的Mizar(MizAR)服务,该服务将多种自动推理,人工智能和表现工具与Mizar及其编写环境集成在一起。服务基于Mizar语言到一阶ATP系统语言的良好转换,并依赖于在包含数万个可用事实的大型理论应用ATP系统的最新进展。
Sep, 2011
该论文结合Flyspeck项目中的数学知识与机器学习方法,提出一种能够自动回答数学问题的人工智能系统,并在评估中表现出较高的效率。该系统的实现涉及到HOL Light逻辑的转换以及机器学习的选择和集成。
Nov, 2012
在Mizar的40周年庆典上,我们成功地开发了一个AI/ATP系统,可以在30秒内自动验证最新版本的Mizar数学库(MML)中约40%的定理,成功地实现了对MML的大规模AI/ATP方法的改进,并将最有用的方法高效地实现使其适用于MML中的150,000个公式,从而将训练时间从大规模语料库中缩短至1-3秒,将该方法简单地部署到Mizar用户的在线自动推理服务(MizAR)中。
Oct, 2013
本文提出HOL4证明助手的机器学习辅助自动推理和前提选择方法,从定理陈述中提取特征选取前提,通过HOLyHammer将其转换为不同格式,再经由ATPs处理。实验显示该系统在HOL4标准库上具有较高的性能。
Sep, 2015
本文介绍了一种用于 HOL4 TacticToe 的策略级自动化方法,将机器学习和翻译技术与自动定理证明辅助工具相结合,以探索不同的策略级证明路径,并且通过组合策略预测和前提选择,在5秒内重新证明了7902个HOL4定理中的39%,效果显著。
Apr, 2018
我们提供了一个基于HOL Light定理证明器的开源框架,可以用作强化学习环境;并提出了一个基于深度强化学习的自动定理证明器DeepHOL,它在基准测试中取得了强大的初步结果。
Apr, 2019
该论文介绍了Thor,一个集成语言模型和自动定理证明器的框架,它采用一种称为“hammers”的方法来选择前提,从而增加了语言模型在PISA数据集上的成功率并解决了相当一部分问题,同时比现有最佳方法在MiniF2F数据集上具有更小的计算量。
May, 2022