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.

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