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 条

[1] Premise Selection for Mathematics by Corpus Analysis and Kernel Methods [J].

Alama, Jesse ;

Heskes, Tom ;

Kuhlwein, Daniel ;

Tsivtsivadze, Evgeni ;

Urban, Josef .

JOURNAL OF AUTOMATED REASONING, 2014, 52 (02) :191-213

[2]

Alama J, 2012, LECT NOTES COMPUT SC, V7180, P37, DOI 10.1007/978-3-642-28717-6_6

[3]

[Anonymous], 2013, EPiC Series in Computing

[4]

[Anonymous], 2019, LCP ISABELLE 2019

[5]

[Anonymous], 2012, IWIL 2010 EPIC

[6]

Barrett Clark, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P171, DOI 10.1007/978-3-642-22110-1_14

[7]

Berghofer S, 2000, LECT NOTES COMPUT SC, V1869, P38

[8]

Blanchette Jasmin Christian, 2012, Interactive Theorem Proving. Proceedings of the Third International Conference, ITP 2012, P345, DOI 10.1007/978-3-642-32347-8_24

[9] Semi-intelligible Isar Proofs from Machine-Generated Proofs [J].

Blanchette, Jasmin Christian ;

Boehme, Sascha ;

Fleury, Mathias ;

Smolka, Steffen Juilf ;

Steckermeier, Albert .

JOURNAL OF AUTOMATED REASONING, 2016, 56 (02) :155-200

[10] Extending Sledgehammer with SMT Solvers [J].

Blanchette, Jasmin Christian ;

Boehme, Sascha ;

Paulson, Lawrence C. .

JOURNAL OF AUTOMATED REASONING, 2013, 51 (01) :109-128

← 1 2 3 4 5 6 →