- Email: [email protected]

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

Copyright © 2018 PROPERTIBAZAR.COM. All rights reserved.