Tata Institute of Fundamental Research
Probabilistically Checkable Proofs
Special Colloquium
Speaker:
Madhu Sudan (Microsoft Research
New England Cambridge
United States of America)
Date:
Thursday, 11 Jun 2015, 16:00 to 17:00
Venue:
AG-66 (Lecture Theatre)
(Scan to add to calendar)
Abstract:
Abstract: As advances in mathematics continue at the current rate, editors of mathematical journals increasingly face the challenge of reviewing increasingly long, and often wrong, ''proofs'' of classical conjectures. Often, even when it is a good guess that a given submission is erroneous, it takes excessive amounts of effort on the editor/reviewer's part to find a specific error one can point to. Most reviewers assume this is an inevitable consequence of the notion of verifying submissions; and expect the complexity of the verification procedure to grow with the length of the submission.
In this talk I will describe how research, mostly in the 20th century, has allowed us think about theorems and proofs formally; and how this formal thinking has paved the way for radically easy ways of verifying proofs. In particular I will introduce the "PCP" (for Probabilistically Checkable Proof) format of writing proofs. This is a format that allows for perfectly valid proofs of correct theorems, while any purported proof of an incorrect assertion will be ``evidently wrong'', so that a reviewer checking consistency of a very parts of the proof (probabilistically) will detect an error. The existence of PCPs may seem purely fictional but research since the 1990s has shown how such PCPs do exist. In this talk I will explain the concept of a PCP. After giving some some background on why theoretical computer scientists are interested in PCPs and theorems and proofs in general, I will attempt to give an idea of how such PCP formats, and associated verification methods are designed.
Brief Bio: Prof. Madhu Sudan has been a Principal Researcher at Microsoft Research New England since 2009. He received his B.Tech. in Computer Science and Engineering from IIT-Delhi in 1987 and his Ph.D. from the University of California, Berkeley, in 1992. From 1992 to 1997, he was at the IBM Thomas J. Watson Research Center, after which he moved to MIT as a faculty member in the Electrical Engineering and Computer Science (EECS) department and a member of their Computer Science and Artificial Intelligence Laboratory (CSAIL). Sudan's current research interests lie in the interface of Computation and Communication, and in particular, in the role of errors in this interface. He has made important contributions to theoretical computer science in areas such as probabilistically checkable proofs, non-approximability of optimization problems, list decoding, and error‑correcting codes. During his distinguished career, he has won many awards, including the ACM Distinguished Doctoral Dissertation (1993), the Godel Prize (2001), and the Rolf Nevanlinna Prize (2002). He is a fellow of ACM and the American Mathematical Society. Prof. Madhusudan was awarded the Infosys Prize in Mathematical Sciences in 2014.
-----------------------------------------
Infosys Science Foundation lecture by Prof. Madhu Sudan Principal Researcher, Microsoft Research New England, and Adjunct Professor, Electrical Engineering and Computer Science department, and Computer Science and Artificial Intelligence Laboratory, MIT, Cambridge.
| Speaker: | Madhu Sudan (Microsoft Research New England Cambridge United States of America) |
| Date: | Thursday, 11 Jun 2015, 16:00 to 17:00 |
| Venue: | AG-66 (Lecture Theatre) |
(Scan to add to calendar)
Abstract:
Abstract: As advances in mathematics continue at the current rate, editors of mathematical journals increasingly face the challenge of reviewing increasingly long, and often wrong, ''proofs'' of classical conjectures. Often, even when it is a good guess that a given submission is erroneous, it takes excessive amounts of effort on the editor/reviewer's part to find a specific error one can point to. Most reviewers assume this is an inevitable consequence of the notion of verifying submissions; and expect the complexity of the verification procedure to grow with the length of the submission.
In this talk I will describe how research, mostly in the 20th century, has allowed us think about theorems and proofs formally; and how this formal thinking has paved the way for radically easy ways of verifying proofs. In particular I will introduce the "PCP" (for Probabilistically Checkable Proof) format of writing proofs. This is a format that allows for perfectly valid proofs of correct theorems, while any purported proof of an incorrect assertion will be ``evidently wrong'', so that a reviewer checking consistency of a very parts of the proof (probabilistically) will detect an error. The existence of PCPs may seem purely fictional but research since the 1990s has shown how such PCPs do exist. In this talk I will explain the concept of a PCP. After giving some some background on why theoretical computer scientists are interested in PCPs and theorems and proofs in general, I will attempt to give an idea of how such PCP formats, and associated verification methods are designed.
Brief Bio: Prof. Madhu Sudan has been a Principal Researcher at Microsoft Research New England since 2009. He received his B.Tech. in Computer Science and Engineering from IIT-Delhi in 1987 and his Ph.D. from the University of California, Berkeley, in 1992. From 1992 to 1997, he was at the IBM Thomas J. Watson Research Center, after which he moved to MIT as a faculty member in the Electrical Engineering and Computer Science (EECS) department and a member of their Computer Science and Artificial Intelligence Laboratory (CSAIL). Sudan's current research interests lie in the interface of Computation and Communication, and in particular, in the role of errors in this interface. He has made important contributions to theoretical computer science in areas such as probabilistically checkable proofs, non-approximability of optimization problems, list decoding, and error‑correcting codes. During his distinguished career, he has won many awards, including the ACM Distinguished Doctoral Dissertation (1993), the Godel Prize (2001), and the Rolf Nevanlinna Prize (2002). He is a fellow of ACM and the American Mathematical Society. Prof. Madhusudan was awarded the Infosys Prize in Mathematical Sciences in 2014.
-----------------------------------------
Infosys Science Foundation lecture by Prof. Madhu Sudan Principal Researcher, Microsoft Research New England, and Adjunct Professor, Electrical Engineering and Computer Science department, and Computer Science and Artificial Intelligence Laboratory, MIT, Cambridge.
In this talk I will describe how research, mostly in the 20th century, has allowed us think about theorems and proofs formally; and how this formal thinking has paved the way for radically easy ways of verifying proofs. In particular I will introduce the "PCP" (for Probabilistically Checkable Proof) format of writing proofs. This is a format that allows for perfectly valid proofs of correct theorems, while any purported proof of an incorrect assertion will be ``evidently wrong'', so that a reviewer checking consistency of a very parts of the proof (probabilistically) will detect an error. The existence of PCPs may seem purely fictional but research since the 1990s has shown how such PCPs do exist. In this talk I will explain the concept of a PCP. After giving some some background on why theoretical computer scientists are interested in PCPs and theorems and proofs in general, I will attempt to give an idea of how such PCP formats, and associated verification methods are designed.
Brief Bio: Prof. Madhu Sudan has been a Principal Researcher at Microsoft Research New England since 2009. He received his B.Tech. in Computer Science and Engineering from IIT-Delhi in 1987 and his Ph.D. from the University of California, Berkeley, in 1992. From 1992 to 1997, he was at the IBM Thomas J. Watson Research Center, after which he moved to MIT as a faculty member in the Electrical Engineering and Computer Science (EECS) department and a member of their Computer Science and Artificial Intelligence Laboratory (CSAIL). Sudan's current research interests lie in the interface of Computation and Communication, and in particular, in the role of errors in this interface. He has made important contributions to theoretical computer science in areas such as probabilistically checkable proofs, non-approximability of optimization problems, list decoding, and error‑correcting codes. During his distinguished career, he has won many awards, including the ACM Distinguished Doctoral Dissertation (1993), the Godel Prize (2001), and the Rolf Nevanlinna Prize (2002). He is a fellow of ACM and the American Mathematical Society. Prof. Madhusudan was awarded the Infosys Prize in Mathematical Sciences in 2014.
-----------------------------------------
Infosys Science Foundation lecture by Prof. Madhu Sudan Principal Researcher, Microsoft Research New England, and Adjunct Professor, Electrical Engineering and Computer Science department, and Computer Science and Artificial Intelligence Laboratory, MIT, Cambridge.