A Learning-Based Fact Selector for Isabelle/HOL

被引：38

作者：

Blanchette, Jasmin Christian ^{[1
,2
,3
]}

Greenaway, David ^{[4
]}

Kaliszyk, Cezary ^{[5
]}

Kuhlwein, Daniel ^{[6
]}

Urban, Josef ^{[7
]}

机构：

[1] Inria Nancy Grand Est, Villers Les Nancy, France

[2] LORIA, Villers Les Nancy, France

[3] Max Planck Inst Informat, Saarbrucken, Germany

[4] Univ New South Wales, NICTA, Sydney, NSW, Australia

[5] Univ Innsbruck, Innsbruck, Austria

[6] Radboud Univ Nijmegen, Nijmegen, Netherlands

[7] Czech Tech Univ, Prague, Czech Republic

来源：

JOURNAL OF AUTOMATED REASONING | 2016年 / 57卷 / 03期

基金：

奥地利科学基金会; 欧洲研究理事会;

关键词：

Relevance filtering; Machine learning; Proof assistants; Automatic theorem provers; PROVING SYSTEM COMPETITION; EFFICIENT SMT-SOLVER; SLEDGEHAMMER; MATHEMATICS; KERNEL; MIZAR;

D O I：

10.1007/s10817-016-9362-8

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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.

引用

页码：219 / 244

页数：26

共 55 条

[41] STATISTICAL INTERPRETATION OF TERM SPECIFICITY AND ITS APPLICATION IN RETRIEVAL [J].