Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings
Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021, Proceedings
复制标题
使用分析 Tableaux 和相关方法进行自动推理 - 第 30 届国际会议，TABLEAUX 2021，英国伯明翰，2021 年 9 月 6-9 日，会议记录
DOI：
10.1007/978-3-030-86059-2_11
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Rawson M
中科院分区：
文献类型：
--
作者：
Rawson M
最先进的自动化定理证明者通过精心设计的例程探索大型搜索空间，但大多数人不像人类数学家那样从过去的经验中学习。不幸的是，机器学习的启发式定理证明通常要么快速要么准确，而不是两者兼而有之。因此，系统必须在启发式指导的质量和使用它所需的推理速度的降低之间进行权衡。我们提出了一个基于延迟参数调节的系统(LazyCoP)，它完全与启发式开销隔离，允许使用甚至是深层神经网络，而推理速度没有明显的下降。给S 10次在数学语料库中寻找证据的能力，当训练自己的证据时，系统从的百分之七十提高到百分之七十。
State-of-the-art automated theorem provers explore large search spaces with carefully-engineered routines, but most do not learn from past experience as human mathematicians can. Unfortunately, machine-learned heuristics for theorem proving are typically either fast or accurate, not both. Therefore, systems must make a tradeoff between the quality of heuristic guidance and the reduction in inference rate required to use it. We present a system (lazyCoP) based on lazy paramodulation that is completely insulated from heuristic overhead, allowing the use of even deep neural networks with no measurable reduction in inference rate. Given 10 s to find proofs in a corpus of mathematics, the system improves from 64% to 70% when trained on its own proofs.