ITR: Probabilistic Checking of Proofs

ITR：证据的概率检查

• 批准号: 0312575
• 负责人: Madhu Sudan
• 金额: --
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing grant
• 财政年份: 2003
• 资助国家: 美国
• 起止时间: 2003-09-01 至 2006-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0312575&HistoricalAwards=false
• 关键词: ITR; Probabilistic; Checking; 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.

理解定理和证明的本质一直是计算机科学基础的核心任务。 现代计算机的设计源于这一追求，而这一追求在计算理论的发展中继续发挥着关键作用。 该研究项目在验证证据的背景下调查新问题。它研究以概率方式验证证明的能力，以较小的错误验证可能性换取验证证明所需时间的巨大优势。 最近（过去十年左右）的研究表明，证明的概率验证是一个可行的目标，并且可以带来令人惊讶的高效可验证性。但迄今为止，该成果尚未投入实际应用。实际应用的主要障碍是概率可验证的证明比经典证明长得多。该项目研究了可概率检查证明的大小和验证它的复杂性之间的权衡。 它还将研究此类证明系统的新应用，特别是自动验证计算机程序正确执行的任务。 为了产生更广泛的影响，该项目还将通过教育和外展活动促进广大受众对信息和计算基础的理解和兴趣。