MaSh: Machine Learning for Sledgehammer
MaSh: Machine Learning for Sledgehammer
复制标题
MaSh：Sledgehammer 的机器学习
DOI：
10.1007/978-3-642-39634-2_6
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Josef Urban
中科院分区：
文献类型：
--
作者：
Daniel Kühlwein;Jasmin Christian Blanchette;Cezary Kaliszyk;Josef Urban
Sledgehammer在证明助手Isabelle/HOL中集成了自动定理证明器。一个关键组件，相关性过滤器，启发式地对数千个可用事实进行排序，并根据与当前目标的语法相似性选择一个子集。我们介绍MaSh，这是一种从成功的证明中学习的替代方法。我们的“零点击”愿景带来了新的挑战：MaSh应该与用户的工作流程无缝集成，这样他们就可以从机器学习中受益，而无需安装软件、设置服务器或指导学习。潜在的机器借鉴了最近在Mizar和HOL Light的背景下进行的研究，并进行了一些增强。MaSh在大型形式化方面优于旧的相关过滤器，并且通过组合两个过滤器可以获得特别强的过滤器。
Sledgehammer integrates automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the relevance filter, heuristically ranks the thousands of facts available and selects a subset, based on syntactic similarity to the current goal. We introduce MaSh, an alternative that learns from successful proofs. New challenges arose from our “zero-click” vision: MaSh should integrate seamlessly with the users’ workflow, so that they benefit from machine learning without having to install software, set up servers, or guide the learning. The underlying machinery draws on recent research in the context of Mizar and HOL Light, with a number of enhancements. MaSh outperforms the old relevance filter on large formalizations, and a particularly strong filter is obtained by combining the two filters.
登录
查看更多内容
BliStr：盲目的战略制定者
DOI：
10.29007/8n7m
发表时间：
2013
期刊：
ArXiv
影响因子：
--
作者：
J. Urban
通讯作者：
J. Urban
DOI：
10.1007/978-3-642-36675-8
发表时间：
2013
期刊：
--
影响因子：
--
作者：
M. P. Bonacina;M. Stickel
通讯作者：
M. P. Bonacina;M. Stickel
从多重证明中学习：第一次实验
DOI：
10.29007/nb2g
发表时间：
2012
期刊：
The Science of the total environment
影响因子：
--
作者：
D. Kühlwein;J. Urban
通讯作者：
J. Urban
三年 Sledgehammer 经验，自动和交互式定理证明者之间的实用联系
DOI：
--
发表时间：
2012
期刊：
IWIL@LPAR
影响因子：
--
作者：
Lawrence Charles Paulson;J. Blanchette
通讯作者：
J. Blanchette
DOI：
10.1007/s10817-014-9303-3
发表时间：
2014-08-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Kaliszyk, Cezary;Urban, Josef
通讯作者：
Urban, Josef