BliStr: The Blind Strategymaker
Josef Urban
Radboud University Nijmegen

June 18, 2014

1 / 23

Introduction: Large-theory Automated Reasoning

I Reason automatically in large formal theories
I Since 2003: ATP translation of the Mizar Mathematical

Library (ca 50k theorems/proofs in 2014)
I Since 2005: Isabelle-HOL - ca 20k theorems/proofs, ca

40k in AFP in 2014
I Since 2012: HOL Light/Flyspeck - ca 23k theorems/proofs

in 2014I More corpora in 2014: HOL4, ACL2, Coq?

2 / 23

Introduction: Large-theory Automated Reasoning
I Useful for ITP - Sledgehammer, MizAR, HOL(y)Hammer
I Interesting AI research:
I We can try to learn how to prove theorems from many

related proofs and proof developments
I Hopefully closer to how we learn math and science thansolving small isolated problems
I Data-driven AI algos vs. theory-driven AI algos:
I Do not design very complex algos completely manually, butlearn their parts from large amount of data
I Used to build self-driving cars, recent machine-translation

systems, etc. - scary AI?

3 / 23

Large-theory Benchmarks/Competition

I Suitable benchmarks and competitions to foster thelarge-theory research:
I 2006: the MPTP Challenges
I Since 2008: Large-Theory Batch category of the CADE

Automated System Competition (CASC)
I 2010: Judgement Day, 2011: MPTP2078, 2013: HH 7150
I Performance on the benchmarks/competitions

corresponds to performance in the ITP deployment

4 / 23

The Mizar@Turing 2012 large-theory competition
I Sponsored by 3000 GBP by Google at the Turing100

conference
I The MPTP2078 benchmark: 2078 related Mizar problems

in general topology
I 1000 allowed for pre-competition training with their Mizar

and Vampire proofs
I 400 unknown would be used for the competitionI Just a concrete example on which the Blind Strategymaker(BliStr) was developed
I Later used also to develop ATP strategies for Flyspeckproblems

5 / 23

Initial ATP performance in May 2012

I Measured on the 1000 training problems
I Vampire solves 691 of them with 60s time limit (a bit myfault)
I E 1.6pre in auto-mode solves 519 of them with 60s timelimit
I E clearly needed to improve on the problems - but how?

6 / 23

ATP Search Strategies

I Automated Theorem Provers (ATPs) are programmedusing complex search strategies
I E prover has a nice language for strategy specification

7 / 23

The E strategy with longest specification in Jan 2012

G-E--_029_K18_F1_PI_AE_SU_R4_CS_SP_S0Y:--definitional-cnf=24 --simplify-with-unprocessed-units --tstp-in--split-aggressive --split-clauses=4 --split-reuse-defs--simul-paramod --forward-context-sr --destructive-er-aggressive--destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq-F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred-H’(
4 * ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),
3 * ConjectureGeneralSymbolWeight(
PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),
1 * Clauseweight(PreferProcessed,1,1,1),
1 * FIFOWeight(PreferProcessed))’-s --print-statistics --print-pid --resources-info --memory-limit=192

8 / 23

Its clause evaluation heuristic

G-E--_029_K18_F1_PI_AE_SU_R4_CS_SP_S0Y:
4 * ConjectureGeneralSymbolWeight(
SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),
3 * ConjectureGeneralSymbolWeight(
PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),
1 * Clauseweight(PreferProcessed,1,1,1),
1 * FIFOWeight(PreferProcessed)

9 / 23

ATP Search Strategies - continued

I Different strategies fit different mathematical problems
I But most of the lemmas proved by (formal) mathematicians

are not so new
I Problems often share some structure, particularly in large

formal libraries
I So let us group the “similar” problems together and findgood strategies for such groups
I But how again? - Certainly not manually for all of math!

10 / 23

Dawkins - cumulative selection (Blind Watchmaker)
I The strategy space is very large
I Guessing a good strategy at random is hopelessI (a bat sonar “cannot be developed by a random mutation,right??”)I It needs an “intelligent designer” (Watchmaker)!?
I But if there is a selection function that chooses the mostfitting mutations
I Then the iterative process can converge very fast
I “Methinks it is like a weasel” found in 40 iterations by

Dawkins’ program
I Compare it to the chance of hitting one of 2728 sentences

at random

11 / 23

The Blind Watchmaker, a.k.a. Cumulative Evolutionwww.personal.psu.edu/drs18/blogs/screaming_red_ass_sock_monkey/2009/06/post-8.html
12 / 23

The Blind Watchmaker, a.k.a. Cumulative Evolution

I The strategies are like giraffes, the problems are their food
I The better the giraffe specializes for eating problems

unsolvable by others, the more it gets fed and further
evolved13 / 23

The Main Idea

I Evolve faster strategies on groups of similar solvable andeasy problems.
I If they get much faster some more (related but harder)

problems might become solvable.
I What are similar problems? Problems that behave similarly

wrt. existing strategies (this is evolving!)
I What are easy problems? Problems that are quickly

solvable by some strategy (this concept is evolving too!)
I So we need a loop that co-evolves the strategies and theconcepts of similar and easy problems

14 / 23

The Main Strategymaking Loop

I Interleave fast strategy improvement (by Iterated LocalSearch) on its “similar easy” problems with the evaluationof the strategy on all problems
I That way, the notions of “similar” and “easy” evolve, andthe strategies are invented on harder and harder problems
I The giraffes are getting taller and taller, covering more andmore resources

15 / 23

ParamILS - Iterated Local Search

I Start with an initial configuration θ0I Loop between two steps:
I (i) perturbing the configuration to escape from a local

optimum,I (ii) iterative first improvement of the perturbedconfiguration.
I The result of step (ii) is accepted if it improves the previous

best configuration.

16 / 23

17 / 23Governing the Iterated Local Search
1. Start with an initial set of E strategies
2. Evaluate them with high time limit (5s) on all problems
3. For each strategy collect its best-solvable problems
4. This partitions the set of all solvable problems
5. Remove from such sets the problems that still take toomuch time
6. Run ParamILS on each strategy with low time limit (1s) onits set of cheap best-solvable problems
7. After ParamILS invents a new strategy S, evaluate S withthe high time limit on all problem
8. Recompute the problem partitioning (goto 2), someproblems might have become cheaper (eligible for thetraining phase)
9. End when there is no more improvement
10. Variations: make even smaller clusters of problems
randomly - risk of overfitting
18 / 23

Two BliStr runs and a union of 6 runs done within 30
hours (on the 1000 Mizar@Turing training problems)

description

iterations

best strat.

solved

37
23
113

569
576
576

648
643
659

BliStr1400
BliStr32500
Union of 6 runs
description

tlow

TParamILS

real timeuser time

BliStr1400
BliStr32500
Union of 6 runs

1s
3s

400s
2500s

593m
1558m
1800m

3230m
3123m

19 / 23More Results

I The best BliStr strategy on the 1000 training problems: 598

problems solved
I 6 best E1.6pre strategies could solve only 597 together (in60s)
I 6 best BliStr strategies could solve 653 together (in 60s)
I The Turing100 competition (400 problems for evaluation):
I 257 MaLARea/E/BliStr vs 248 Vampire/SInE
I MaLARea/E without the new strategies: only 214
I 14195 Flyspeck/HH problems (2012):
I E1.6pre: 32.6%, using BliStr strategies: 38.4% (in 30s)

20 / 23

The E strategy with longest specification in May 2014atpstr_my_c7bb78cc4c665670e6b866a847165cb4bf997f8a:
6 * ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1)
8 * ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1)
8 * ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1)
4 * ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5)
10 * ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1)2 * ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1)
10 * ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5)
1 * Clauseweight(ByCreationDate,2,1,0.8)
1 * Clauseweight(ConstPrio,3,1,1)
6 * Clauseweight(ConstPrio,1,1,1)
2 * Clauseweight(PreferProcessed,1,1,1)
6 * FIFOWeight(ByNegLitDist)
1 * FIFOWeight(ConstPrio)
2 * FIFOWeight(SimulateSOS)
8 * OrientLMaxWeight(ConstPrio,2,1,2,1,1)
2 * PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5)
10 * RelevanceLevelWeight(ConstPrio,2,2,0,2,100,100,100,100,1.5,1.5,1)
8 * RelevanceLevelWeight2(PreferNonGoals,0,2,1,2,100,100,100,400,1.5,1.5,1)
2 * RelevanceLevelWeight2(PreferGoals,1,2,1,2,100,100,100,400,1.5,1.5,1)
6 * RelevanceLevelWeight2(SimulateSOS,0,2,1,2,100,100,100,400,1.5,1.5,1)
8 * RelevanceLevelWeight2(SimulateSOS,1,2,0,2,100,100,100,400,1.5,1.5,1)
5 * rweight21_g
3 * Refinedweight(PreferNonGoals,1,1,2,1.5,1.5)
1 * Refinedweight(PreferNonGoals,2,1,2,2,2)
2 * Refinedweight(PreferNonGoals,2,1,2,3,0.8)
8 * Refinedweight(PreferGoals,1,2,2,1,0.8)
10 * Refinedweight(PreferGroundGoals,2,1,2,1.0,1)
20 * Refinedweight(SimulateSOS,1,1,2,1.5,2)
1 * Refinedweight(SimulateSOS,3,2,2,1.5,2)

21 / 23Current Limitations and Future WorkI Term orderings and weighting schemes are anotherimportant problem-specific parameters to explore - notdone yet
I Even then the E strategy language is likely not expressive

enoughI Particular subproblems might benefit from very differenttargeted search strategies
I More difficult problems might benefit from splitting intosmaller ones where a good strategy is known
I Similar to splitting ITP proofs into smaller lemmas

discharged by different tactics
I Such process will likely again be highly parameterized andsubject to such data-driven programming

22 / 23

Thanks for your attention!

Questions?

23 / 23