Evolution of Proofs in Computer Science

 
Yael Tauman Kalai
Microsoft Research
 
The Evolution of Proofs
in Computer Science
 
What is a Proof?
 
Mathematical proofs:
 
Developed by ancient Greek mathematicians
[Thales,Eudoxus,Theaetetus,Atistotle 600BCE]
 
[Euclid 300 BCE]  
Introduced axiomatic method,
theorems are proved using deductive logic.
 
Proof theory: 
well studied branch of mathematics
[Hilbert 19
th
 century]
Classical Proofs
Zero-Knowledge Proofs
[Goldwasser-Micali-Rackoff85]
 
Zero-Knowledge Proofs
[Goldwasser-Micali-Rackoff85]
Interactive Proofs
[Goldwasser-Micali-Rackoff85]
 
[Goldreich-Micali-Wigderson87]
:
Interactive Proofs are More Efficient!
[Lund-Fortnow-Karloff-Nissan90, Shamir90]
 
Example:  
Chess
 
Interactive Proofs are More Efficient!
[Lund-Fortnow-Karloff-Nissan90, Shamir90]
 
Multi-Prover Interactive Proofs
[BenOr-Goldwasser-Kilian-Wigderson88]
The Power of Multi-Prover Interactive
Proofs (MIPs)
[Babai-Fortnow-Lund90]
Any proof can be made 
exponentially shorter
with a 2-prover interactive proof!
[Fortnow-Rompel-Sipser88]:
 
 
 
[Fortnow-Rompel-Sipser88]:
Probabilistically Checkable Proofs
V
 
PCP Theorem:
Every proof  can be converted to a  probabilistically
checkable one (of almost same size) that can be verified
 by reading only 
constant
 number of its bits.
 
[Feige-Goldwasser-Lovasz-Safra-Szegedy91, Babai-Fortnow-Levin-
 
Szegedy91, Arora-Safra92, Arora-Lund-Mutwani-Sudan-Szegedy92]
 
 
 
 
Classical
proofs
(zero-knowledge)
Interactive
proofs
multi-prover
interactive proofs
Probabilistically
checkable proofs
Fast Forward to Today’s Reality
 
 
proof
 
Verifying
 should be 
easier than computing
!
 
Proving
 should 
not
 be much 
harder than computing
!
Delegating Computation in the Real World
 
Interactive Proofs
not useful for real world delegation
 
Proving is harder than computing
 
Verifying is easier that computing
(time to verify proportional to space of
computation)
Interactive Proofs
useful for real world delegation
 
Only for functions computable by 
low depth circuits
 
[Goldwasser-Kalai-Rothblum08]
Proving is not harder than computing
Computationally-Sound Proofs
[Micali94]
certificate!
A delegation scheme 
for all functions.
Computational  soundness:  
Cheating is
possible, but requires too much work,
assuming hardness assumption
 
no satisfying proof of security
2-Message Delegation Scheme
 
[Aiello-Bhatt-Ostrovsky-Rajagopalan2000, Dwork-
Langberg-Naor-Nissim-Reingold2004, Kalai-Raz2009,
Groth10, Gennaro-Gentry-Parno2010 , Chung-Kalai-
Vadhan2010, Applebaum-Ishai-Kushilevitz2010, Gentry-
Wichs2011,  Parno-Raykova-Vaikuntanathan2011,
Benabbas-Gennaro-Vahlis2011,
 
Goldwasser-Lin-
Rubinstein2011, Damgard-Faust-Hazay2011, Lipma12,
Fiore-Gennaro2012, Bitansky-Canetti-Chiesa-
Tromer2012a, Bitansky-Canetti-Chiesa-Tromer2012b,
Gennaro-Gentry-Parno-Raykova2012, Kalai-Raz-
Rothblum2013, Kalai-Raz-Rothblum2014]
[Kalai-Raz-Rothblum2014]:
2-message
 delegation scheme for 
all functions
under 
standard hardness assumptions
No-signalling
 strategies
[Khaln-Tsirelson85, Rastall85]
 
special relativity theory:   
information does
not travel faster than the speed of light
No-Signalling Strategies
Multi-Prover Interactive Proofs (MIPs)
 
Classical soundness:
[Babai-Fortnow-Lund90]:  
MIP for all functions
 
Quantum soundness:
[Ito-Vidick2012]: 
MIP for all functions
 
No-Signalling soundness:
[Kalai-Raz-Rothblum2014]: 
MIP for all functions
 
 
[Kalai-Raz-Rothblum2014]:
No-signalling
 multi-prover interactive
proofs for 
all functions
2-message delegation 
for
all functions
 
under standard hardness
assumptions
[Kalai-Raz-Rothblum2014]:
MIP
 
sound against
no-signalling
provers
 
secure
for every FHE
with sub-exponential
security
 
[Aiello-Bhatt-Ostrovsky-Sivarama00]
Classical
proofs
zero-knowledge
Interactive
proofs
Muti-prover
interactive proofs
Probabilistically
checkable 
proofs
No-signalling
multi-prover
interactive proofs
2-message
delegation
 
Delegation in Practice
 
[Cormode-Mitzenmacher-Thaler2012]
[
Thaler-Roberts-Mitzenmacher-Pfister2012]
[Thaler2013]
[Vu-Setty-Blumberg-Walfish2013]
[BenSasson-Chiesa-Genkin-Tromer-Virza2013]
[Parno-Gentry-Howell-Raykova2013]
 
Thank You!
Slide Note
Embed
Share

Explore the development of proofs in computer science, from classical mathematical proofs to interactive and zero-knowledge proofs pioneered by researchers like Goldwasser, Micali, Rackoff, and others. Discover how proof theory has evolved over time, making computation verification more efficient and secure.

  • Computer Science
  • Proof Theory
  • Interactive Proofs
  • Zero-Knowledge Proofs
  • Mathematical Evolution

Uploaded on Sep 28, 2024 | 0 Views


Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

E N D

Presentation Transcript


  1. The Evolution of Proofs in Computer Science Yael Tauman Kalai Microsoft Research

  2. What is a Proof? Mathematical proofs: Developed by ancient Greek mathematicians [Thales,Eudoxus,Theaetetus,Atistotle 600BCE] [Euclid 300 BCE] Introduced axiomatic method, theorems are proved using deductive logic. Proof theory: well studied branch of mathematics [Hilbert 19th century]

  3. Classical Proofs http://t1.gstatic.com/images?q=tbn:ANd9GcRgVZaiUJw6jETLHjTP2kLvHubHBHBEgPR_7e5AejdA009zk8XWQw ? ?

  4. Zero-Knowledge Proofs [Goldwasser-Micali-Rackoff85] https://encrypted-tbn2.gstatic.com/images?q=tbn:ANd9GcQUTuUOrhz56SCCWsCh_zSwnfBPAV02PZVA8YqrN4TRxALPs_l_

  5. Zero-Knowledge Proofs [Goldwasser-Micali-Rackoff85] https://encrypted-tbn2.gstatic.com/images?q=tbn:ANd9GcQUTuUOrhz56SCCWsCh_zSwnfBPAV02PZVA8YqrN4TRxALPs_l_ ? ?

  6. Interactive Proofs [Goldwasser-Micali-Rackoff85] ? ? [Goldreich-Micali-Wigderson87]: Every statement that has a classical proofhas zero- knowledge interactive proof, assuming one-way functions

  7. Interactive Proofs are More Efficient! [Lund-Fortnow-Karloff-Nissan90, Shamir90] Example: Chess

  8. Interactive Proofs are More Efficient! [Lund-Fortnow-Karloff-Nissan90, Shamir90] correctness of any computation can be proved: Time to verify Space required to do the computation

  9. Multi-Prover Interactive Proofs [BenOr-Goldwasser-Kilian-Wigderson88] ?1 ?2 ?1 ?2 ?

  10. The Power of Multi-Prover Interactive Proofs (MIPs) [Babai-Fortnow-Lund90] Any proof can be made exponentially shorter with a 2-prover interactive proof!

  11. [Fortnow-Rompel-Sipser88]: ?1 ?2?3?4 ?1 ?2?3?4 ?1 ?2 ?

  12. [Fortnow-Rompel-Sipser88]: ?

  13. Probabilistically Checkable Proofs V [Feige-Goldwasser-Lovasz-Safra-Szegedy91, Babai-Fortnow-Levin- Szegedy91, Arora-Safra92, Arora-Lund-Mutwani-Sudan-Szegedy92] PCP Theorem: Every proof can be converted to a probabilistically checkable one (of almost same size) that can be verified by reading only constant number of its bits.

  14. Classical proofs (zero-knowledge) Interactive proofs multi-prover interactive proofs Probabilistically checkable proofs

  15. Fast Forward to Todays Reality

  16. Delegating Computation in the Real World Help me compute ? on ? ?(?) proof http://t3.gstatic.com/images?q=tbn:ANd9GcScK77uBTorrrLXSv5W0LY_P5gegzcxoCQB81Tr7sMajiUC_DNB Verifying should be easier than computing! Proving should not be much harder than computing!

  17. Interactive Proofs not useful for real world delegation Verifying is easier that computing (time to verify proportional to space of computation) Proving is harder than computing

  18. Interactive Proofs useful for real world delegation [Goldwasser-Kalai-Rothblum08] ? ? Proving is not harder than computing Only for functions computable by low depth circuits

  19. Computationally-Sound Proofs [Micali94] A delegation scheme for all functions. Computational soundness: Cheating is possible, but requires too much work, assuming hardness assumption ? ? hash proof certificate! Secure under standard assumption [Kilian92] no satisfying proof of security

  20. 2-Message Delegation Scheme [Aiello-Bhatt-Ostrovsky-Rajagopalan2000, Dwork- Langberg-Naor-Nissim-Reingold2004, Kalai-Raz2009, Groth10, Gennaro-Gentry-Parno2010 , Chung-Kalai- Vadhan2010, Applebaum-Ishai-Kushilevitz2010, Gentry- Wichs2011, Parno-Raykova-Vaikuntanathan2011, Benabbas-Gennaro-Vahlis2011, Goldwasser-Lin- Rubinstein2011, Damgard-Faust-Hazay2011, Lipma12, Fiore-Gennaro2012, Bitansky-Canetti-Chiesa- Tromer2012a, Bitansky-Canetti-Chiesa-Tromer2012b, Gennaro-Gentry-Parno-Raykova2012, Kalai-Raz- Rothblum2013, Kalai-Raz-Rothblum2014]

  21. [Kalai-Raz-Rothblum2014]: 2-message delegation scheme for all functions under standard hardness assumptions No-signalling strategies [Khaln-Tsirelson85, Rastall85] special relativity theory: information does not travel faster than the speed of light

  22. No-Signalling Strategies ?1 ?2 ?1 ?2 ? Original soundness: ?1 and ?2don t interact Quantum soundness: ?1 and ?2may have entangled quantum states No-signalling soundness: answer of ?1 (conditioned on ?1)does not give information about ?2

  23. Multi-Prover Interactive Proofs (MIPs) Classical soundness: [Babai-Fortnow-Lund90]: MIP for all functions Quantum soundness: [Ito-Vidick2012]: MIP for all functions No-Signalling soundness: [Kalai-Raz-Rothblum2014]: MIP for all functions

  24. [Kalai-Raz-Rothblum2014]: No-signalling multi-prover interactive proofs for all functions 2-message delegation for all functions under standard hardness assumptions

  25. [Kalai-Raz-Rothblum2014]: MIP ?1 ?2 ? sound against no-signalling provers ? ?1?2 ?1 ?2 ? ? [Aiello-Bhatt-Ostrovsky-Sivarama00] 2-msg delegation secure for every FHE with sub-exponential security ? ? ?1, ?2, , ? ?1, ?2, , ?

  26. Classical proofs zero-knowledge Interactive proofs No-signalling multi-prover interactive proofs Muti-prover interactive proofs Probabilistically checkable proofs 2-message delegation

  27. Delegation in Practice [Cormode-Mitzenmacher-Thaler2012] [Thaler-Roberts-Mitzenmacher-Pfister2012] [Thaler2013] [Vu-Setty-Blumberg-Walfish2013] [BenSasson-Chiesa-Genkin-Tromer-Virza2013] [Parno-Gentry-Howell-Raykova2013]

  28. Thank You!

More Related Content

giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#