Hammering towards Qed - Institute for Computing and Information

Hammering towards Qed - Institute for Computing and Information

Hammering towards Qed Cezary Kaliszyk University of Innsbruck Josef Urban Radboud University July 18, 2014 1 / 21 Outline Automation for Interac...

383KB Sizes 0 Downloads 4 Views

Recommend Documents

QED - Beckman Institute | Caltech
Mark Taper Forum, Los Angeles, March 10-May 13, 2001 and. "Oxygen", a play by Carl Djerassi and Roald Hoffman, produced

Intelligence and Machines - Simons Institute for the Theory of Computing
May 30, 2013 - ... history of machine intelligence. - Define machine intelligence. - Neocortical principles. - State of

Mechanisms - Department of Information and Computing Sciences
May 16, 2011 - Vickrey-Clark-Groves Mechanism. 3 ... i: ui = vi(a) + m. Auctions are a common area for mechanism design.

Information Flows and the Implications of Cloud Computing for Trade
Sep 26, 2008 - 61 DreamHost is an example of a webhosting service while Salesforce is an example of a software-as-a-serv

Towards a Privacy Research Roadmap for the Computing - arXiv
science of privacy that cuts across application domains. There is ... more applied, domain-specific research that transl

Towards Free Market Cloud Computing - Colin Perkins
Abstract—Although cloud computing has made great inroads in terms of consumer adoption, we argue that the paradigm sti

Towards Securing APIs in Cloud Computing - arXiv
Keywords: Cloud security, access control, Cloud API, RBAC, TRBAC ... through proper access control mechanisms ... Discre

aidanhogan.com - Institute for Information Business
Apr 11, 2011 - ...thanks to people with whom I have worked closely, including Alex, Antoine, Jeff, Luigi and Piero; ...t

Hammering Away - Isabelle - TUM
A User's Guide to Sledgehammer for Isabelle/HOL. Jasmin Christian Blanchette. Institut für Informatik, Technische Unive

An Efficient Method for Computing Synaptic - Salk Institute
Kluwer. Academic Publishers, Norwell, MA. Perkel, D. H., Mulloney, B., and Budelli, R. W. 1981. Quantitative methods for

Hammering towards Qed Cezary Kaliszyk University of Innsbruck

Josef Urban Radboud University

July 18, 2014

1 / 21

Outline

Automation for Interactive Proof Translations Evaluation Machine Learning Reconstruction Towards Qed Strength Logics Knowledge

2 / 21

Interactive proofs I Formal proof skeleton + filling in the gaps I Searching for needed theorems I Tedious properties

I Proof structure is lost

I Uninteresting parts overshadow interesting ones

3 / 21

Interactive proofs I Formal proof skeleton + filling in the gaps I Searching for needed theorems I Tedious properties

I Proof structure is lost

I Uninteresting parts overshadow interesting ones I Automation for Interactive Proof I Tableaux: Itaut, Tauto, Blast I Rewriting: Simp, Subst, HORewrite I Decision Procedures: Congruence Closure, Ring, Omega, Cooper

I Large-theory ATP and translation techniques I Mizar: MaLARea I Isabelle/HOL: Sledgehammer I HOL(y)Hammer

3 / 21

MizAR demo http://www.youtube.com/watch?v=4es4iJKtM3I

4 / 21

AI-ATP systems (?-Hammers) Current Goal

Proof Assistant ITP Proof

First Order Problem

?Hammer

ATP Proof

ATP .

5 / 21

AI-ATP systems (?-Hammers) Current Goal

Proof Assistant ITP Proof

First Order Problem

?Hammer

ATP Proof

ATP .

How much can it do?

5 / 21

AI-ATP systems (?-Hammers) Current Goal

Proof Assistant ITP Proof

First Order Problem

?Hammer

ATP Proof

ATP .

How much can it do?

I Flyspeck (including core HOL Light and Multivariate) I Mizar / MML I Isabelle (Auth, Jinja)

5 / 21

AI-ATP systems (?-Hammers) Current Goal

Proof Assistant ITP Proof

First Order Problem

?Hammer

ATP Proof

ATP .

How much can it do?

I Flyspeck (including core HOL Light and Multivariate) I Mizar / MML I Isabelle (Auth, Jinja)

 45%

5 / 21

Translation Overview I Various exports to FOF

I MESON-style monomorphisation I TFF-style type tagging I Isabelle-style type guards

I Export to TFF1

I Additional provers (Alt-ergo) I Tools that do Monomorphisation of TPTP (Why3, tptp2X) I Export to THF0 I Satallax, Leo-II, ... I Monomorphisation makes the problems big and slow

I SMT solvers

I Reconstruction I Export to other ITPs I Rarely better 6 / 21

Translation overview (HOL) 1

Heuristic type instantiation I Similar for induction

2

Eliminate  Remove -abstractions I lifting, combinators, ... Optimizations I if..then..else, !

3

4

9

5

Separate predicates and terms I Consider cases, introduce bool variables

6

NNF, Skolemize

7 8

Use apply functor to make all applications first-order Encode remaining types I monomorphisation, tags, guards

9

Various optimizations (incomplete) 7 / 21

8 / 21

Re-proving (Flyspeck, 30sec) Prover E-par Z3-4 E Leo II Vampire CVC3 Satallax Yices1 IProver Prover9 Spass LeanCop AltErgo Paradox 4 any

Theorem% 38.4 36.1 32.6 31.0 30.5 28.9 26.9 25.3 24.5 24.3 22.9 21.4 19.8 0.0 50.2

CounterSat% 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.6 0.0 0.0 0.0 0.0 18.2 -

Sotac– 69.12 61.51 45.44 45.77 45.75 43.36 48.75 33.32 29.50 29.98 26.22 26.98 26.82 0.06 9 / 21

Machine learning techniques Algorithms I Syntactic methods I Neighbours using various metrics, Recursive (MePo) I Sparse Naive Bayes I Variable prior, Confidence

I k-Nearest Neighbours

I TF-IDF, Dependency weighting I Neural Networks I Winnow, Perceptron

I Linear Regression

I Needs feature and theorem space reduction

Combining original and ATP dependencies

I Added value depends on the precision of human deps 10 / 21

Features for Machine Learning I A function that given a goal or premise returns a sparse vector I Optionally weights for kinds of features I Internal TF-IDF

I Types and type variables I Constants I Subterms / Patterns I I I I

No variable normalization De-Bruijn indices Types of variables Normalization of type variables

I Meta information: Theory name, kind of rule, contains 9, ...

11 / 21

Naive Bayes I Each predictor

I Given a vector of features of a goal g and a set of facts I Returns the predicted relevance for each fact f

I Assume independence between the features P (f is relevant for proving g )

= =

P (f is relevant j g’s features)

_ _ #f

P (f is relevant j f1 ; : : : ; fn )

P (f is relevant)ni=1 P (fi j f is relevant)

is a proof dependency  ni=1 #fi

appears when f is a proof dependency f is a proof dependency

#

I Efficient

I Fast predictions I Fast updates I Small models 12 / 21

Success rate (%)

Success Rates

40

Syntactic (MePo) 30

20 16

32

64

128

256

512

1024

Number of facts

13 / 21

Success rate (%)

Success Rates

40 Naive Bayes Syntactic (MePo)

30

20 16

32

64

128

256

512

1024

Number of facts

13 / 21

Proof Reconstruction I Existing reconstruction mechanisms

I Metis, SMT I Mizar by I MESON, Prover9 I Parse TSTP/SMT proofs I Create subgoals that match ATP intermediate steps I Automatically solve all simple ones

I High reconstruction rates give confidence in our techniques I Naive reconstruction: 90% (of Flyspeck solved) I MESON, SIMP, ?_ARITH_TAC I With TSTP parsing: 96%

14 / 21

Outline

Automation for Interactive Proof Translations Evaluation Machine Learning Reconstruction Towards Qed Strength Logics Knowledge

15 / 21

Improve Percentage I Is 100% possible?

I Granularity of steps also increases I Premise selection

I Encodings I ATP-systems I Reconstruction

16 / 21

Improve Percentage I Is 100% possible?

I Granularity of steps also increases I Premise selection I Good machine learning algorithms are still slow

I Encodings

I Efficient but more complete I ATP-systems I Strategies and combinations

I Reconstruction

I Formalized decision procedures

16 / 21

ITP logics I MizAR

I Set theory, dependent types, (almost) first order I Sledgehammer, HOL(y)Hammer, ... I HOL, shallow polymorphism

I ACL2

I Structure Irrelevance, Logic as lists I Isabelle/ZF, ... I All features of meta-logic necessary

I Coq

I Good machine-learning, but encodings hard

17 / 21

Sharing parts among systems I Machine Learning Predictors

I Already many shared I Feature extraction I Given common data format

I Certain Transformations

I -lifting, combinators, apply functor I Monomorphisation, Heuristic instantiation I Type encodings (tags, guards, soft-types, ...)

I Knowledge management

I Namespaces, Browsing, Search, Refactoring, Change management

I Readable proof reconstruction

18 / 21

Common Functionality I TPTP hierarchy: FOF, TFF1, THF0, ? I THF1 already used

$

I Sledgehammer HOL(y)Hammer I HOL4 I Type-classes I Property of a universally quantified type I Already in some Isabelle/HOL version of THF1 com_ring :

I Dependent types and intersection types

$tType > $o

I Already in MPTP

I Universes

![X : int, K : matrix(X)]: ... ![X : t1 & t2]: ...

![X : int]:

I General - and Sigma-types I ...

$type(X) : $tType

![W : ![X]: X = X]: ... 19 / 21

Matching concepts across libraries I Same concepts in different proof assistants

I Problem for proof translation I Manually found 7-70 pairs I Same properties I Patterns, like associativity, distributivity ... I Same algebraic structures do differ.

I Automatically finds 400 pairs of same concepts I In HOL Light, HOL4, Isabelle/HOL I Coq: so far only lists analyzed

I Proof advice can be universal?

20 / 21

Conclusion and Future work

I Hammer-systems

I Until recently unappreciated by developers I A large number of top-level proofs found automatically I Try it!

I Interoperation between HOL Light, HOL4 and Isabelle/HOL I Cross-Prover Advice Service

I More logics, ITPs, ATPs, and more effective

21 / 21

HOL(y) Hammer Machine learning based premise selection for HOL Light

http://cl-informatik.uibk.ac.at/software/hh/ 21 / 21

References C. Kaliszyk and J. Urban. MizAR 40 for Mizar 40. CoRR, abs/1310.2805, 2013. C. Kaliszyk and J. Urban. PRocH: Proof reconstruction for HOL Light. In M. P. Bonacina, editor, CADE, volume 7898 of Lecture Notes in Computer Science, pages 267–274. Springer, 2013. C. Kaliszyk and J. Urban. HOL(y)Hammer: Online ATP service for HOL Light. Mathematics in Computer Science, 2014. http://dx.doi.org/10.1007/s11786-014-0182-0. C. Kaliszyk and J. Urban. Learning-assisted automated reasoning with Flyspeck. Journal of Automated Reasoning, 2014. http://dx.doi.org/10.1007/s10817-014-9303-3. D. Kühlwein, J. C. Blanchette, C. Kaliszyk, and J. Urban. MaSh: Machine learning for Sledgehammer. In S. Blazy, C. Paulin-Mohring, and D. Pichardie, editors, Proc. of the 4th International Conference on Interactive Theorem Proving (ITP’13), volume 7998 of LNCS, pages 35–50. Springer, 2013. C. Tankink, C. Kaliszyk, J. Urban, and H. Geuvers. Formal mathematics on display: A wiki for Flyspeck. In J. Carette, D. Aspinall, C. Lange, P. Sojka, and W. Windsteiger, editors, MKM/Calculemus/DML, volume 7961 of Lecture Notes in Computer Science, pages 152–167. Springer, 2013.

21 / 21