AI over Large Formal Knowledge Bases: The First Decade

Josef Urban, Radboud University Nijmegen

Talk Structure

AI for Formal Math or FM for AI?

The Plan

  1. Make large KBs of formal thought (Mizar/MML, HOL/Flyspeck, Isabelle) accessible to strong AI tools: DONE (or well under way)
  2. Test/Use/Evolve AI tools:
    • deductive AI: first-order/higher-order/inductive ATPs, SMTs, decision procs.
    • inductive AI: statistical learning tools (Bayesian, kernels, neural,...),
    • inductive AI: semantic learning tools (ILP - Progol, Alef, ..; latent semantics - PCA; genetic methods, ... )

The Plan (continued)

  1. Build custom/combined inductive/deductive tools/metasystems:
    • usually combining ATP/symbolic techniques with ML/statistical ideas
    • (statistically governed, "greedy", ...) indexing, subsumption, abstraction, limited inference/induction, concept/lemma creation, strategy generation, etc.
  2. Continuously test performance
  3. Define harder AI tasks as the performance grows (prove theorems from more basic lemmas, develop whole theories, ...)
  4. GOTO 2

The Plan (continued)

Corpora

AI tools: Evolving technology stack

Premise Selection

Example: Mizar Proof Advisor (2003)

Evaluation of methods on MPTP2078

ML evaluation (premise recall) ML evaluation: Recall

Evaluation of methods on MPTP2078

ATP evaluation (problems solved) ATP evaluation: Solved

Combined (ensemble) methods

Combining with SInE improves the best method from 726 to 797 (10%) ATP evaluation: Combined ATP evaluation: Solved

Learning from ATP and ITP proofs

Learning from the shortest ATP proofs helps also by about 10% ATP vs MML ATP and MML, combined with SInE

Evaluation on Flyspeck

Example of a simpler proof

The HOL(y)Hammer AI/ATP service

HH architecture

HH architecture

Examples of AI guidance in E and Prover9

BliStr: Blind Strategymaker, E-MaLeS

BliStr on 1000 Mizar@Turing problems

Examples of self-evolving metasystems

Machine Learner for Automated Reasoning

MaLARea Architecture

MaLARea

MaLARea

Machine Learning Connection Prover

MaLeCoP Architecture

MaLeCoP

MaLeCoP

Some lessons learned

Some lessons learned

Challenges in large formal KBs

transfer ideas from SAT to malecop and E

Challenges in large formal KBs

Acknowledgments

Thanks for your Attention!