CS294: Foundations of Probabilistic Proofs (F2020)

Interactive Proofs 1   [intro video] [intro slides]   [video] [slides]

• introduction to the course
• definition of interactive proofs
• GNI is contained in IP (with private coins)
• IP is contained in PSPACE

Formulation of interactive proofs:

• Babai 1985: Trading group theory for randomness
• Goldwasser Micali Rackoff 1989: The knowledge complexity of interactive proof systems

Video:

• Proofs, Secrets, and Computation (by Silvio Micali)

Interactive Proofs 2   [video] [slides]

• sumcheck protocol
• coNP contained in IP
  • arithmetization for UNSAT
• P^#P contained in IP
  • arithmetization for #SAT

The sumcheck protocol:

• Lund Fortnow Karloff Nisan 1992: Algebraic methods for interactive proof systems

Interactive Proofs 3   [video] [slides]

• definition of QBF
• PSPACE is contained in IP
  • TQBF is the starting point
  • arithmetization of formula and quantifiers
  • Shamir's protocol (with Shen's degree reduction)
• TQBF is PSPACE-complete

Shamir's protocol:

• Shamir 1992: IP=PSPACE
• Shen 1992: IP=PSPACE: simplified proof

Additional:

• Meir 2013: IP=PSPACE using error-correcting codes
• Meir 2014: talk on the work above

Interactive Proofs 4   [video] [slides]

• private coins vs public coins
• definition of AM[k] and MA[k]
• GNI is contained in AM[2]
  • reduction to approximate counting
  • approximate counting via pairwise-independent hashing
• IP[k] is contained in AM[k+2]
  • high-level intuition only

Goldwasser--Sipser transformation:

• Goldwasser Sipser 1986: Private coins versus public coins in interactive proof systems
  • emulating any interactive proof, with public coins

Additional:

• Goldreich Leshkowitz 2016: On emulating interactive proofs with public coins
  • an alternative emulation that is more efficient than GS86
• Furer Goldreich Mansour Sipser Zachos 1989: On completeness and soundness in interactive proof systems
  • achieving perfect completeness for AM
  • IP with perfect soundness is in NP

Interactive Proofs 5   [video] [slides]

• IPs with bounded communication/randomness
  • complexity classes IP[p,v,r] and AM[p,v,r] (prover bits ≤ p, verifier bits ≤ v, random bits ≤ r)
• IP[p,v,r] is contained in DTime(2^O(p+v+r)poly)
  • compute value of game tree
• IP[p,v] is contained in BPTime(2^O(p+v)poly)
  • approximate value of game tree (sub-sample by random tapes)
  • proof via Chernoff bound and union bound
• AM[p] is contained in BPTime(2^{O(p log p)}poly)
  • approximate value of game tree (sub-sample by transcript-consistent next messages)
  • refine previous analysis via hybrids
• IP[p] is contained in BPTime(2^{O(p log p)}poly)^NP
  • (sketch) as above but transcript consistency is harder

The results presented in class:

• Goldreich Håstad 1998: On the complexity of interactive proofs with bounded communication

Additional results:

• Boppana Håstad Zachos 1987: Does co-NP have short interactive proofs?
• Goldreich Vadhan Wigderson 2002: On interactive proofs with a laconic prover

Interactive Proofs 6   [video] [slides]

• inefficiency of Shamir's protocol
  • honest prover in Shamir's protocol is 2^{O(n^2)}
  • honest prover in Shen's protocol is 2^O(n)
  • T-time S-space machines yield 2^{O(S log T)}-time provers
• doubly-efficient interactive proofs
  • motivation of delegation of computation
  • theorem statement for log-space uniform circuits
• low-degree extensions (univariate and multivariate)
• bare bones protocol for layered circuits
  • one sumcheck per layer

The result presented in class:

• Goldwasser Kalai Rothblum 2015: Delegating computation: interactive proofs for muggles

A survey:

• Goldreich 2017: On doubly-efficient interactive proof systems

Additional on implementations of GKR's protocol:

• Cormode Mitzenmacher Thaler 2012: Practical verified computation with streaming interactive proofs
• Thaler Roberts Mitzenmacher Pfister 2012: Verifiable computation with massively parallel interactive proofs
• Thaler 2013: Time-optimal interactive proofs for circuit evaluation
• Wahby Howald Garg Shelat Walfish 2015: Verifiable ASICs

Additional on doubly-efficient interactive proofs:

• Reingold Rothblum Rothblum 2016: Constant-round interactive proofs for delegating computation
• Rothblum 2016: talk on the work above (basic)
• Rothblum 2016: talk on the work above (more technical)

Interactive Proofs 7   [video] [slides]

• IP for GI
• definition of honest-verifier zero knowledge (HVZK)
• the IP for GI is HVZK
• definition of malicious-verifier zero knowledge (ZK)
• the IP for GI is ZK
• PZK ⊆ SZK ⊆ CZK
• towards SZK ⊆ coAM
  • running simulator when x ∉ L
  • IP for GI → IP for GNI (!)

On zero knowledge:

• Goldwasser Micali Rackoff 1989: The knowledge complexity of interactive proofs systems
• Goldreich 2010: Zero knowledge - a tutorial
• Fortnow 1987: The complexity of perfect zero-knowledge

Video:

• Zero knowledge probabilistic proof systems (by Shafi Goldwasser)

Probabilistically Checkable Proofs 1   [video] [slides]

• definition of a PCP verifier
• the complexity class PCP_c,s[r,q]_Σ
• simple class inclusions
• delegation of computation via PCPs
• PSPACE ⊆ PCP

Video:

• Wigderson 2018: Scientific revolutions, ToC and PCP

New York Times article about the PCP Theorem:

• Kolata 1992: New short cut found for long math proofs

Probabilistically Checkable Proofs 2   [video] [slides]

• exponential-size PCPs
  • NP ⊆ PCP_1,0.5[poly(n),O(1)]_{0,1}
  • good query complexity, bad proof length
• linear PCPs
  • the complexity class LPCP_c,s[l,r,q]_Σ
  • NP ⊆ LPCP_1,0.75[O(n²),O(m+n),4]_{0,1}

The exponential-size constant-query PCP is the inner PCP in this paper:

• Arora Lund Motwani Sudan Szegedy 1998: Proof verification and the hardness of approximation problems

Probabilistically Checkable Proofs 3   [video] [slides]

• compiling any LPCP into a PCP
• self-correction
• linearity testing
  • BLR test
  • analysis via majority decoding

Main:

• Blum Luby Rubinfeld 1990: Self-testing/correcting with applications to numerical problems

Additional:

• Bellare Coppersmith Håstad Kiwi Sudan 1996: Linearity testing in characteristic two
  • first connection of Fourier analysis and testing

Video:

• Rubinfeld 2018: A comedy of errors

Probabilistically Checkable Proofs 4   [video] [slides]

• NP ⊆ PCP[log, polylog] (up to low-degree testing)
  • start from satisfiability of quadratic equations
  • amplify gap via an error-correcting code
  • arithmetization via Reed--Muller instead of Hadamard
  • reduce to sumcheck problem

Main:

• Babai Fortnow Lund 1990: Non-deterministic exponential time has two-prover interactive protocols

Probabilistically Checkable Proofs 5   [video] [slides]

• NP ⊆ PCP[log, polylog] with low-degree testing
• definition of low-degree testing
• univariate polynomials
  • d+2 random points (any ε)
    • [S92, Section 3.1.1]
  • d+2 random evenly-spaced points (ε ~ 1/d²)
    • [S92, Section 3.1.2]
• multivariate polynomials
  • total degree via random lines (ε ~ 1/d²)
    • [S92, Section 3.2.1]

Main:

• Babai Fortnow Lund 1990: Non-deterministic exponential time has two-prover interactive protocols

Additional:

• Arora Safra 1998, Section 4
• Sudan 1992: Efficient checking of polynomials and proofs and the hardness of approximation problems

PCPs with Sublinear Verification 1   [video] [slides]

• NEXP ⊆ PCP[poly, poly]
  • why last lecture's approach fails
    • verifier would run in exponential time
  • definition of oracle satisfiability (OSAT)
    • [BFL90, Definition 4.1]
  • OSAT is NEXP-complete
    • [BFL90, Proposition 4.2]
  • OSAT to zero testing
  • zero testing to sumcheck
    • Method 1: via random evaluation [BFLS91, Section 5.2]
    • Method 2: via additional polynomials [BS08, Lemma 4.11]

Main:

• Babai Fortnow Lund 1990: Non-deterministic exponential time has two-prover interactive protocols

PCPs with Sublinear Verification 2   [video] [slides]

• NTIME(T) ⊆ PCP[ptime=poly(T), vtime=poly(n,log(T))]
  • low-degree extension with H of logarithmic size
    • [BFLS91, Section 4.1]
  • low-degree projection polynomials to obtain bits
    • [BFLS91, Section 6]
• PCP-based delegation of computation

Main:

• Babai Fortnow Levin Szegedy 1991: Checking computations in polylogarithmic time
• Kilian 1992: A note on efficient zero-knowledge proofs and arguments
• Micali 1994: Computationally sound proofs

Interactive Oracle Proofs 1   [video] [slides]

• definition of the IOP model
• PCP as a special case of IOP
• IP as a special case of IOP
• IOP=NEXP
• IOP-based delegation of computation

IOP model and its compilation into non-interactive arguments:

• Ben-Sasson Chiesa Spooner 2016: Interactive oracle proofs

Interactive Oracle Proofs 2   [video] [slides]

• linear-size IOPs for arithmetic computations
  • R1CS(𝔽) ∈ IOP[k=O(log n),l=O(n),q=O(log n)]_𝔽
• the Reed--Solomon encoding
• univariate sumcheck

IOPs for R1CS(𝔽):

• Ben-Sasson Chiesa Riabzev Spooner Virza Ward 2019: Aurora: transparent succinct arguments for R1CS

Aditional on IOPs for CSAT(𝔽₂):

• Ben-Sasson Chiesa Gabizon Riabzev Spooner 2016: Interactive oracle proofs with constant rate and query complexity

Interactive Oracle Proofs 3   [video] [slides]

• testing proximity to the Reed--Solomon code
• the main challenges
• the FRI protocol

FRI protocol:

• Ben-Sasson Bentov Horesh Riabzev 2018: Fast Reed--Solomon interactive oracle proofs of proximity

Interactive Oracle Proofs 4   [video] [slides]

• soundness analysis of the FRI protocol

FRI protocol:

• Ben-Sasson Bentov Horesh Riabzev 2018: Fast Reed--Solomon interactive oracle proofs of proximity

Additional reading:

• Ben-Sasson Kopparty Saraf 2018: Worst-case to average case reductions for the distance to a code
• Ben-Sasson Goldberg Kopparty Saraf 2019: DEEP-FRI: sampling outside the box improves soundness
• Ben-Sasson Carmon Ishai Kopparty Saraf 2020: Proximity Gaps for Reed--Solomon Codes

Interactive Oracle Proofs 5   [video] [slides]

• automata computations over fields
• linear-size IOP for automata computations (with succinct verification)
• machines as time trace + memory trace
• permutation check

Main:

• Ben-Sasson Bentov Horesh Riabzev 2018: Scalable, transparent, and post-quantum secure computational integrity
• Ben-Sasson Chiesa Goldberg Gur Riabzev Spooner 2019: Linear-Size Constant-Query IOPs for Delegating Computation

Proof Composition 1   [video] [slides]

• definition of robust PCPs/IOPs
• definition of PCPs/IOPs of proximity
• proof composition theorem (non-interactive and interactive)

Main:

• Ben-Sasson Goldreich Harsha Sudan Vadhan 2006: Robust PCPs of proximity, shorter PCPs, and applications to coding
• Dinur Reingold 2006: Assignment testers: towards a combinatorial proof of the PCP Theorem
• Ben-Sasson Chiesa Gabizon Riabzev Spooner 2016: Interactive oracle proofs with constant rate and query complexity

Proof Composition 2   [video] [slides]

• definition of robust PCP
• robustification
• query bundling
• construction of a robust PCPs

Robustification:

• Dinur Reingold 2006: Assignment testers: towards a combinatorial proof of the PCP Theorem

Additional on O(1)-query tests:

• Section 7.2 of Arora Lund Motwani Sudan Szegedy 1998: Proof verification and the hardness of approximation problems

Proof Composition 3   [video] [slides]

• definition of PCP of proximity (PCPP)
• PCPP from local decoder and special PCP
• exp-size constant-query PCPP for NP
• poly-size polylog-query PCPP for NP
• PCP Theorem via proof composition

Main:

• Ben-Sasson Goldreich Harsha Sudan Vadhan 2006: Robust PCPs of proximity, shorter PCPs, and applications to coding
• Dinur Reingold 2006: Assignment testers: towards a combinatorial proof of the PCP Theorem

Parallel Repetition   [video] [slides]

• reducing queries at expense of alphabet size
• 2-query PCPs vs 2-player 1-round games
• Verbitsky's Theorem

Main on parallel repetition:

• Verbitsky 1996: Towards the parallel repetition conjecture

Counterexamples:

• Feige 1991: On the success probability of the two provers in one-round proof systems
• Feige Verbitsky 1996: Error reduction by parallel repetition: a negative result

Additional on explicit bounds for Furstenberg–Katznelson:

• Polymath 2010: A new proof of the density Hales-Jewett theorem

Limitation of PCPs and IOPs   [video] [slides]

• statement of the Parallel Repetition Theorem (exponential decay)
• statement of the Sliding Scale Conjecture
• limitations of PCPs wrt to soundness error
• limitations of IOPs wrt to soundness error

Main:

• Raz 1998: A parallel repetition theorem
• Moshkovitz 2019: Sliding scale conjectures in PCP
• Chiesa Yogev 2020: Barriers for succinct arguments in the random oracle model

Towards the sliding scale conjecture:

• Bellare Goldwasser Lund Russell 1991: Efficient probabilistically checkable proofs and applications to approximations
• Dinur Fischer Kindler Raz Safra 1999: PCP characterizations of NP: Toward a polynomially-small error-probability
• Moshkovitz 2016: Low degree test with polynomially small error

Holographic Proofs   [video] [slides]

• sublinear verification for any computation
• offline/online model
• from holography to preprocessing
• holographic PCP for NP
• holographic IOP for NP

Main:

• Chiesa Hu Maller Mishra Vesely Ward 2020: Marlin: Preprocessing zkSNARKs with universal and updatable SRS
• Chiesa Ojha Spooner 2020: Fractal: Post-quantum and transparent recursive proofs from holography

No class (Thanksgiving week).

No class (Thanksgiving week).

Class Project Presentations 1

Class Project Presentations 2

No class (RRR week).

No class (RRR week).