ITR: Probabilistic Checking of Proofs

点击翻译按钮获取中文摘要

Understanding the nature of theorems and proofs has been a central quest in the foundations of computer science. The design of the modern computer owes its origins to this quest,and this quest has continued to play a pivotal role in developing a theory of computing. This research project investigates new questions in the context of verifying proofs. It investigates the capacity of proofs to be verified probabilistically, trading off a small possibility of incorrect verification for a huge advantage in the time taken to verify proofs. Research in the recent past (last ten years or so) has shown that probabilistic verification of proofs is a feasible goal and can lead to surprisingly efficient verifiability. However the results have not been of practical use so far. The main obstacle to practical utility is that the probabilistically verifiable proofs are much longer than classical proofs. This project investigates the tradeoff between the size of a probabilistically checkable proof and the complexity of verifying it. It will also investigate new applications of such proof systems, and in particular, to the task of automatic verification of correct execution of computer programs. For broader impact, the project will also foster understanding and interest into the foundations of information and computation to a wide audience via educational and outreach activities.