Probabilistically Checkable Proofs Madhu Sudan Microsoft Research June 11, 2015 TIFR: Probabilistically Checkable Proofs 1 of 28 Can Proofs be Checked Efficiently? The Riemann Hypothesis is true (12th Revision) By Ayror Sappen

# Pages to follow: 15783 June 11, 2015 TIFR: Probabilistically Checkable Proofs 2 of 28 Proofs and Theorems Conventional belief: Must read whole proof to verify it. Modern Constraint: Dont have time to (do anything, leave alone to) read proofs. This talk: New format for writing proofs. Extremely efficiently verifiable probabilistically, with

small error probability. Not much longer than conventional proofs. June 11, 2015 TIFR: Probabilistically Checkable Proofs 3 of 28 Outline of talk Quick primer on the Computational perspective on theorems and proofs (proofs can look very different than youd think). Definition of Probabilistically Checkable Proofs (PCPs). Why (computer scientists) study proofs/PCPs. (Time permitting) Some overview of ancient (~25 year old) and modern (~10 year old) PCPs. June 11, 2015

TIFR: Probabilistically Checkable Proofs 4 of 28 Part I: Primer June 11, 2015 TIFR: Probabilistically Checkable Proofs 5 of 28 What is a proof? June 11, 2015

TIFR: Probabilistically Checkable Proofs 6 of 28 Philosophy & Computing - 101 Theorems vs. Proofs? Theorem: True Statement Proof: Convinces you of truth of Theorem Why is Proof more convincing than Theorem? Easier to verify? Computationally simple (mechanical, no creativity needed, deterministic?) Computational complexity provides formalism! Advantage of formalism: Can study alternate formats for writing proofs that satisfy basic expectations, but provide other features. June 11, 2015

TIFR: Probabilistically Checkable Proofs 7 of 28 The Formalism Theorems/Proofs: Sequence of symbols. System of Logic Verification Procedure . (presumably simple/efficient etc.) Proof proves Theorem accepts. TheoremThere exists s.t. accepts. if both have same set of theorems. But possible different proofs! Different formats! June 11, 2015

TIFR: Probabilistically Checkable Proofs 8 of 28 Theorems: Deep and Shallow A Deep Theorem: talk Proof: (too long to fit this margin). A Shallow Theorem: The number has a divisor between and . Proof: . June 11, 2015 TIFR: Probabilistically Checkable Proofs

9 of 28 Deep Shallow Theory of NP-completeness [Cook,Levin,Karp70s]: Every deep theorem reduces to shallow one! Given Theorem and bound on the length (#symbols) of a proof, there exist integers such that has a divisor between and if and only if has a proof of length [Kilian90s] Shallow theorem easy to compute from deep one. Proof not much longer () [Polynomial vs. Exponential growth important!] June 11, 2015 TIFR: Probabilistically Checkable Proofs

10 of 28 Aside: P & NP P = Easy Computational Problems Solvable in polynomial time (E.g., Verifying correctness of proofs) NP = Problems whose solution is easy to verify (E.g., Finding proofs of mathematical theorems) NP-Complete = Hardest problems in NP Is P = NP? Is finding a solution as easy as specifying its properties? Can we replace every mathematician by a computer? Wishing = Working! June 11, 2015

TIFR: Probabilistically Checkable Proofs 11 of 28 New Formats for Proofs? New format for Proof: Theorem T has Proof Divisor D New Verifier: Compute from ; Verify D divides A; and . Theory of Computing: Many alternate formats for proofs. Can one of these help June 11, 2015

TIFR: Probabilistically Checkable Proofs 12 of 28 Part II: Prob. Checkable Proof June 11, 2015 TIFR: Probabilistically Checkable Proofs 13 of 28 PCP Format PCP Verifier 0101001010111010101110

V 0 1. Reads Theorem 2. Tosses random coins 3. Determines proof query locations 4. Reads locations. Accepts/Rejects HTHHTH Theorem s.t. V accepts (always) False V rejects w. prob. 50% 1

1 Does such a PCP Verifier, making few queries, exist? June 11, 2015 TIFR: Probabilistically Checkable Proofs 14 of 28 Features of interest #queries: Small! Constant? 3 bits? Length (compared to old proof): Linear? Quadratic? Exponential? Transformer: Old proofs => New Proofs? (Not essential, but desirable)

[Arora,Lund,Motwani,S.,Szegedy92]: PCPs with constant queries exist. [Dinur06]: New construction [Large body of work]: Many improvements (to queries, length) June 11, 2015 TIFR: Probabilistically Checkable Proofs 15 of 28 Part III: Why Proofs/PCPs? June 11, 2015 TIFR: Probabilistically Checkable Proofs

16 of 28 Complexity of Optimization Well-studied optimization problems: Map Coloring: Color a map with minimum # colors so adjacent regions have different colors. Travelling Salesman Problem: Visit n given cities in minmum time. Chip Design: Given two chips, are they functionally equivalent? Quadratic system: Does a system of quadratic equations in variables have a solution? [Pre 1970s] All seem hard? And pose similar barriers [Cook,Levin,Karp70s]: All are equivalent, and equivalent to automated theorem proving. Given , and length , find proof of length proving June 11, 2015

TIFR: Probabilistically Checkable Proofs 17 of 28 Approximation Algorithms When problem is intractable to solve optimally, maybe one can find approximate solutions? Find a travelling salesman trip taking more time than minimum? Find map coloring that requires few more colors than minimum? Find solution that satisfies 90% of the quadratic equations? Often such approximations are good enough. But does this make problem tractable?

June 11, 2015 TIFR: Probabilistically Checkable Proofs 18 of 28 Theory of Approximability 70s-90s: Many non-trivial efficient approximation algorithms discovered. But did not converge to optimum? Why? 90s-2015: PCP Theory + Reductions Proved limits to approximability: For many problems gave a limit beyond which finding even approximate solutions is hard. PCP Inapproximability?

Proof doesnearly not fitcorrect this margin PCP Finding proofs as hard as finding correct ones. Analgous to finding approximate solutions as hard as finding optimal ones. June 11, 2015 TIFR: Probabilistically Checkable Proofs 19 of 28

Part IV: PCP Construction Ideas June 11, 2015 TIFR: Probabilistically Checkable Proofs 20 of 28 Aside: Randomness in Proofs Well explored in Computer Science community in 80s. Randomness+Interaction Many effects Simple Proofs of complex statements Pepsi vs. Coke the blind taste test. Proofs Revealing very little about its truth Prove Waldo exists without ruining game.

Proof that some statement has no short proof! June 11, 2015 TIFR: Probabilistically Checkable Proofs 21 of 28 Essential Ingredient of PCPs Locality of error Verifier should be able to point to error (if theorem is incorrect) after looking at few bits of proof. Abundance of error Errors should be found with high probability.

How do get these two properties? June 11, 2015 TIFR: Probabilistically Checkable Proofs 22 of 28 Locality NP-completeness 3Coloring is NP-complete: T a P b

d c f June 11, 2015 abc def g e g Error is 2-local Abundance? TIFR: Probabilistically Checkable Proofs 23 of 28

Abundance I: via Algebra Express (graph-coloring) via Algebra: Leads to problems of the form: Given polynomial find and such that . Example Actual example doesnt fit this margin Advantage of polynomials: Abundance of non-zeroes. Non-zero polynomial usually evaluates to non-zero. Can test for Polynomials June 11, 2015 TIFR: Probabilistically Checkable Proofs 24 of 28

Abundance II: via Graph Theory [Dinur06] Amplification: a d c f aa b e g bb

ad b ee cc d d e c g ff g g f Constant Factor more edges Double fraction of violated edges (in any coloring) Repeat many times to get fraction upto constant.

June 11, 2015 TIFR: Probabilistically Checkable Proofs 25 of 28 Wrapping up PCPs Highly optimistic/wishful definition Still achievable! Very useful Understanding approximations (Hugely transformative) Checking outsourced computations Unexpected consequences: Theory of locality in errorcorrection June 11, 2015

TIFR: Probabilistically Checkable Proofs 26 of 28 Back to Proofs: Philosophy 201 So will math proofs be in PCP format? NO! Proofs *never* self-contained. Assume common language. Proofs also rely on common context Repeating things we all know is too tedious. Proofs rarely intend to convey truth. More vehicles of understanding/knowledge. Still PCP theory might be useful in some contexts:

Verification of computer assisted proofs? June 11, 2015 TIFR: Probabilistically Checkable Proofs 27 of 28 Thank You! June 11, 2015 TIFR: Probabilistically Checkable Proofs 28 of 28