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; 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.

理解定理和证明的性质一直是计算机科学基础上的核心追求。 现代计算机的设计归功于这一任务，这一任务继续在制定计算理论中发挥关键作用。 该研究项目在验证证明的背景下研究了新问题。它调查了概率验证的证据的能力，在用于验证证明所花费的时间中，易于不正确验证的少量可能性。 最近（过去十年左右）的研究表明，对证明的概率验证是一个可行的目标，可以带来令人惊讶的有效验证能力。但是，到目前为止，结果尚未实用。实际实用程序的主要障碍是概率可验证的证明比经典证据更长。该项目调查了概率可检查的证明的规模与验证它的复杂性之间的权衡。 它还将研究此类证明系统的新应用程序，尤其是自动验证正确执行计算机程序的任务。 为了获得更广泛的影响，该项目还将通过教育和外展活动向广大受众的信息和计算基础增强和兴趣。