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.