Transcript Computer

Kazushige Terui
RIMS, Kyoto University
On 11/10/2015, IPSJ announced:
Computer Shogi Project has been completed.
What’s next?
 Go, or …
Computer Shomei (Proof)
 Can
computer compete with human
mathematicians in theorem proving?
 How similar is Shomei to Shogi?
 Being


studied in
Automated Theorem Proving
CASC competition every year
Fundamental difficulty
 Linked
to Interactive Theorem Proving
 Dates back to Foundations of Mathematics
 Formal proofs are also studied in
Theory of Proofs and Programs
in Theoretical Computer Science
 Cf. Todai Robot Project (NII)
Real function 𝑓 𝑥 = 𝑎𝑥 2 + 𝑏𝑥 + 𝑐
has the minimum when a>0
Translated by human
∀𝑎, 𝑏, 𝑐. (𝑎 > 0 → ∃𝑥. ∀𝑦. 𝑓 𝑥 ≤ 𝑓 𝑦 )
Input to a prover
Theorem. Proof …
∃𝑥. 𝑎𝑥 2 + 𝑏𝑥 + 𝑐 = 0
↕
Consider the sentences built from
2 − 4𝑎𝑐 ≥ 0
𝑏
 polynomials with rational coefficients, ＝, ≦



“and” “or” “implies” “not”
“for every real number x …”
“there exists a real number x such that …”
Then, any sentence can be
 tranformed into one without “for all”,
“there exists”（quantifier elimination）
 decided true or not（decidability）
 proved from the axioms of (ordered) realclosed fields if true（completeness）
 Theorem


provers work so-so fine for:
Some specific domains (eg. RCF)
Finitely axiomatizable theories over 1st order
logic
 Difficulty
arises when the theory includes:
“for every set X…”
“for every function f…” Identifying the limit:
“for every natural number
n…”
foundations
of math
“Mathematics of mathematicians” (1870s～）
 computability theory
 proof theory
 model theory
（+ set theory, nonclassical logics）
Outcomes
 Computers（Turing）
⇒ Computer Science（1950’s～）
 Formal systems（Frege, Russell, Hilbert）
⇒ Computer Shomei
A math theory expressed as a package of formal
language, axioms and inference rules.
 Better to think of it as

“Proving capability of
an imaginary mathematician”

Example: Peano Arithmetic (PA) can
calculate basic funcitons on natural numbers
 use mathematical induction
 deal with integers and rationals (indirectly)
 NOT deal with infinite sets and real numbers

 Natural
numbers, addition, multiplication,
 ＝, ≦, “and” “or” “implies” “not”
 “for every natural x…”
 “there exists a natural x such that…”
 Example:
“n is a prime”
𝑛 ≥ 2 ∧ ∀𝑥, 𝑦(𝑛 = 𝑥𝑦 → 𝑥 = 1 ∨ 𝑦 = 1)
𝐴
𝐴∧𝐵
𝐵
𝐵
𝐴∧𝐵
[𝐴]
𝐴 𝐴→𝐵
𝐵
𝐴 0
𝐵
𝐴→𝐵
𝐴 𝑥 → 𝐴(𝑥 + 1)
𝐴(𝑛)
𝐴
𝐴∧𝐵
𝐵
𝐵
𝐴∧𝐵
[𝐴]
𝐴 𝐴→𝐵
𝐵
𝐴 0
𝐵
𝐴→𝐵
𝐴 𝑥 → 𝐴(𝑥 + 1)
𝐴(𝑛)
𝐴∧𝐵
𝐵
𝐴
𝐴∧𝐵
𝐵
𝐵
𝐴∧𝐵
[𝐴]
𝐴 𝐴→𝐵
𝐵
𝐴 0
𝐵
𝐴→𝐵
𝐴 𝑥 → 𝐴(𝑥 + 1)
𝐴(𝑛)
𝐴∧𝐵
𝐵
𝐴
𝐴∧𝐵
𝐵
𝐵
𝐴∧𝐵
[𝐴]
𝐴∧𝐵
𝐵
𝐵∧𝐴
𝐴 𝐴→𝐵
𝐵
𝐴 0
𝐵
𝐴→𝐵
𝐴 𝑥 → 𝐴(𝑥 + 1)
𝐴(𝑛)
𝐴
𝐴∧𝐵
𝐵
𝐵
𝐴∧𝐵
[𝐴]…[𝐴]
[𝐴 ∧ 𝐵] [𝐴 ∧ 𝐵]
𝐵
𝐴
𝐵∧𝐴
𝐴 𝐴→𝐵
𝐵
𝐴 0
𝐵
𝐴→𝐵
𝐴 𝑥 → 𝐴(𝑥 + 1)
𝐴(𝑛)
𝐴∧𝐵 →𝐵∧𝐴
Proof completed!
 Draw
a proof figure by patching axioms and
inference rules.
 If a proof figure (without assumptions)
𝐴
can be drawn, one says:
“PA proves sentence A.”
PA can prove
 elementary theorems in number theory
 also some advanced theorems which require
analysis or algebra
⇐ since PA conservatively extends to ACA0
 perhaps Fermat’s last theorem too???
（open problem）
 NOT all theorems
（Variants of Ramsey’s theorem,
Kruskal’s theorem, etc.）
Theorem：
There is no mechanical procedure to determine
whether a given sentence of PA is true or not.
Theorem（Church, Turing 1936）：
There is no mechanical procedure to determine
whether a given sentence of 1st order logic is
logically true or not.
Negative solution to Hilbert’s Entscheidungsproblem
(1928)
Theorem：There is no “feasible” procedure to
determine if a given sentence has a “short” proof
or not (unless P=NP).
“short”：provided by a parameter n
“feasible”：in polynomial time p(n)
Negative solution to Gödel’s
Entscheidungsproblem（1956）
Theorem（Gödel 1931）：
There is a true sentence which PA cannot prove.
Example：
G := “PA cannot prove G”（1st incompleteness）
CON := “PA is consistent”（2nd incompleteness）
The same holds even when new symbols and
axioms are added to PA recursively and
consistently.
 Incompleteness


theorem does NOT entail:
Computer is inferior to Human
Computer Shomei is impossible
 In
fact, theorem provers work so-so fine for
finitely axiomatizable theories over
1st order logic.

Solution to Robins’ Conjecture (1997)
 On


the other hand, they do not work well for
Integers (induction axioms)
Sets (2nd order logic or comprehension axioms)
 In
 In
1st order logic, one quantifies over objects.
∀x.A(x) : “for every object x, A(x) holds”
2nd order logic, one quantifies over sets of
objects too.
∀P.A(P) : “for every set P, A(P) holds”

2nd order logic encompasses natural numbers and induction.
𝑵=
{ 𝑋 ∶ 0 ∈ 𝑋 ∧ ∀𝑥 𝑥 ∈ 𝑋 → 𝑥 + 1 ∈ 𝑋 }
Completeness Theorem（Gödel1930）：
There is a (recursive) complete formal system for
1st order logic which proves all logically true
sentences.
Incompleteness Theorem（Cor. to Gödel1931）：
There is NO (recursive) complete formal system
for 2nd order logic which proves all logically true
sentences (in the standard semantics).
1st order：can avoid “guessing from infinite”
（subformula prop., Skolemization, unification）
𝐴 𝐴→𝐵
𝐵
𝐴(𝑡)
∃𝑥. 𝐴(𝑥)
1st order unification
is linear time
2nd order：“guessing from infinite”is essential
（lack of subformula prop, decidable unification）
𝐴(𝐵)
∃𝑃. 𝐴(𝑃)
Big Deviation from Shogi !!!
2nd order unification
is undecidable
From 1st order to higher order!
 Needed
for large part of mathematics
 Some provers exist, but …
 New ideas required
 Study
of logic and computation based on the
slogan “proofs are programs.”
Programming
languages
Constructive
math
Proof
theory
 Introduction
each other:
𝐴 𝐵
𝐴∧𝐵
𝐴
 Sentences
and elimination rules cancel
𝐴
and proofs (quotiented) form a
cartesian closed category:
𝑯𝒐𝒎 𝑨, 𝑩 ∧ 𝑪 ≅ 𝑯𝒐𝒎(𝑨, 𝑩) × 𝑯𝒐𝒎(𝑨, 𝑪)
𝑯𝒐𝒎 𝑨 ∧ 𝑩, 𝑪 ≅ 𝑯𝒐𝒎(𝑨, 𝑩 → 𝑪)
Proof simplification is a computational process:
Fundamental of proof theory（Gentzen1934）：
Proof simplification eventually terminates in 1st
order predicate logic.
Theorem（Gentzen1936,38）：
Consistency of PA can be proved by transfinite
induction up to ε0.

Proofs ≅ Programs
（in functional programming languages）
Logic
Computation
Sentence
Type
Proof figure
Program
Proof simplification
Program execution
A implies B
Functions from A to B
Mathematical Induction
Recursive programming
Consistency
Termination
Denotational semantics（Scott 1960’s～）
sentence ⇒ topological space
proof
⇒ continuous map
Example：category Equ
Objects：T0 spaces endowed with equivalence
relations（equilogical spaces）
 Morphisms：equivalence-preserving continuous maps
Equ is cartesian closed, hence by interpreting
sentences A by equilogical spaces 𝐴 :

∈
∈
𝑃𝑟𝑜𝑜𝑓 𝐴, 𝐵 ⟶ 𝐸𝑞𝑢 𝐴 , 𝐵
𝑝
↦
[𝑝]
Invariant
of proofs
 Not
just symbolic, but also algebraic,
dynamic and continuous.
 Subject
 Does
of mathematical study.
it help to Computer Shomei?

Support writing rigorous proofs
“A technical argument by a trusted author, which
is hard to check and looks similar to arguments known to
be correct, is hardly ever checked in detail.”
(Voevodsky 2014)

Developed under strong influence of the theory
of proofs and programs
Proof assistant
Theoretical backgrd
Origin
Isabelle/HOL
Simple type theory
Church 1940
Agda
Dependent type
theory
Martin-Löf 1970’s
Coq
Calculus of
construction
Coquand 1985
 Mainly

for industrial purposes
Verification of software/hardware
 Spreading

Used by 23% of articles submitted to POPL2014
 About



in theoretical computer science
to be used in pure mathematics
Four color theorem（Coq, Gonthier 2005）
Feit-Thompson thm（Coq, Gonthier et.al. 2012）
Kepler conjecture（Isabelle/HOL Light, Hales
et.al. 2014）
 Computer
supports Human writing a rigorous
proof.
 Human
prove.
supports Computer learning how to
1998：T. Hales et. al. proves Kepler’s conjecture.
 2002：Referee report “it’s 99% correct, but…”
 2003：Hales launches the FLYSPECK project.
 2014：Project completed（see the report 2015）






Proof assistants: Isabelle/HOL and HOL Light
International team of more than 30 people
Detected a small error in the original proof
Are proof assistants really correct ?
⇒ The core of HOL Light: just 400 lines in OCaml
Byproduct: a reusable large-scale library:
thousands of definitions and lemmas
(Kaliszyk, Urban 2014)
 Library
includes (at June, 2012) :
Γ = { 𝐴1 , … , 𝐴1897 }
defs and axioms
Δ = { 𝐿1 , … , 𝐿14185 } lemmas
 Scenario: for each 𝑛 ≤ 14185, let prover(s)
automatically prove
Γ ∪ 𝐿1 , … , 𝐿𝑛−1 ⟹ 𝐿𝑛
 Result: 39％ success（14CPU, 2.2GHz, 30sec）
 Crucial: Premise selection
Machine
Learning!

If premises are selected by human, 56％ are
automatically provable.


The rest 44％ should contain difficult lemmas.
Currently learning is restricted to premise
selection （+α）


Can a computer learn proof tactics too?
“Cornerstones” (lemmas) should be provided by
human.

Train the provers so that they work with less
cornerstones.
 「コンピュータは数学者になれるのか？」
 「数学者はコンピュータに慣れるのか？」
証明の一部自動化
自
動
定
理
証
明
証 人
明 間
支 数
援＋学
系 者
証明データの提供
 Proofs
in mathematics get longer and longer
 Supports
from computers will be essential
 New
trend in ATP (Urban et. al.):
Theorem Proving from Large-Scale Libraries
 From
Big Data to Big Proofs (Scott 2014)
(Photo removed. Google the word “big proof”)
Big Proof (1973 – 2006)
 Computer


Not yet competes with human mathematicians
Boundary between 1st and 2nd orders
 How




Shomei?
to overcome?
Development in proof assistants
Win-win relationship between human and
computer
Learning higher facilities (proof tactics)
Theory of proofs and programs (?)
Thank you for your attention!
Comments appreciated:
[email protected]