A Learning-Based Fact Selector for Isabelle/HOL
A Learning-Based Fact Selector for Isabelle/HOL
复制标题
DOI：
10.1007/s10817-016-9362-8
复制
发表时间：
2016-10-01
期刊：
影响因子：
--
通讯作者：
Urban, Josef
中科院分区：
文献类型：
--
作者：
Blanchette, Jasmin Christian;Greenaway, David;Urban, Josef
大锤将自动定理掠夺者集成在证明助手isabelle/hol中。一个关键组件（事实选择器）启发性地对可用的数千个事实（引理，定义或公理）进行排名，并基于与当前证明目标的句法相似性选择子集。我们介绍MASH，这是一种从成功的证明中学习的替代方法。我们的“零点击”愿景引起了新的挑战：MASH与用户的工作流程无缝集成，因此它们从机器学习中受益，而无需安装软件，设置服务器或指导学习。 Mash在大型形式上优于旧事实选择器。
Sledgehammer integrates automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the fact selector, heuristically ranks the thousands of facts (lemmas, definitions, or axioms) available and selects a subset, based on syntactic similarity to the current proof goal. We introduce MaSh, an alternative that learns from successful proofs. New challenges arose from our "zero click" vision: MaSh integrates seamlessly with the users' workflow, so that they benefit from machine learning without having to install software, set up servers, or guide the learning. MaSh outperforms the old fact selector on large formalizations.