机械化定理证明研究综述-江南 , 李清安 , 汪吕蒙 , 张晓瞳 , 何炎祥.pdf

上善若水

131

31页

0次

2022-05-24

免费下载

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn

Journal of Software,2020,31(1):82112 [doi: 10.13328/j.cnki.jos.005870] http://www.jos.org.cn

机械化定理证明研究综述





江

南

李清安

汪吕蒙

张晓瞳

何炎祥

(湖北工业大学计算机学院,湖北武汉 430068)

(武汉大学计算机学院,湖北武汉 430072)

通信作者: 何炎祥, E-mail: yxhe@whu.edu.cn

摘要: 随着现代社会计算机化程度的提高,与计算机相关的各种系统故障足以造成巨大的经济损失.机械化定

理证明能够建立更为严格的正确性,从而奠定系统的高可信性.针对机械化定理证明的逻辑基础和关键技术,详细剖

析了一阶逻辑和基于消解的证明技术、自然演绎和类型化的



演算、3 种编程逻辑、基于高阶逻辑的硬件验证技

术、程序构造和求精技术之间的联系和发展变迁,其中,3 种编程逻辑包括一阶编程逻辑及变体、Floyd-Hoare 逻辑

和可计算函数逻辑.然后分析、比较了各类主流证明助手的设计特点,阐述了几个具有代表性的证明助手的开发和

实现.接下来对它们在数学、编译器验证、操作系统微内核验证、电路设计验证等领域的应用成果进行了细致的

分析.最后,对机械化定理证明进行了总结,并提出面临的挑战和未来研究方向.

关键词: 定理证明;证明助手;消解;自然演绎;类型化的



演算;编程逻辑;求精

中图法分类号: TP18

中文引用格式: 江南,李清安,汪吕蒙,张晓瞳,何炎祥.机械化定理证明研究综述.软件学报,2020,31(1):82112. http://www.jos.

org.cn/1000-9825/5870.htm

英文引用格式: Jiang N, Li QA, Wang LM, Zhang XT, He YX. Overview on mechanized theorem proving. Ruan Jian Xue Bao/

Journal of Software, 2020,31(1):82112 (in Chinese). http://www.jos.org.cn/1000-9825/5870.htm

Overview on Mechanized Theorem Proving

JIANG Nan

, LI Qing-An

, WANG Lü-Meng

, ZHANG Xiao-Tong

, HE Yan-Xiang

(School of Computer Science, Hubei University of Technology, Wuhan 430068, China)

(School of Computer Science, Wuhan University, Wuhan 430072, China)

Abstra ct : Modern society is now being increasingly computerized. Computer-related failures could result in severe economic loss.

Mechanized theorem proving is an approach to ensuring stricter correctness, and hence high trustworthiness. First, the logical foundations

and key technologies of mechanized theorem proving are discussed. Specifically, first-order logic and resolution-based technology, natural

deduction and Curry-Howard correspondence, three logics of programming including first-order programming logic and its variant, Floyd-

Hoare logic, and logic for computable functions, hardware verification technology based on higher-order logic, and program constructions

and refinement are analyzed, as well as the relationship and evolvement between them. Then key design features of the mainstream proof

assistants are compared, and the development and implementation of several representative provers are discussed. Next their applications

in the fields of mathematics, compiler verification, operating-system microkernel verification, and circuit design verification are analyzed.

Finally, mechanized theorem proving is summarized and challenges and future research directions are put forward.

 基金项目: 国家自然科学基金(90818018, 91018009, 61170022, 91118003, 61373039); 华为技术有限公司合作项目(YB201509

0035); 湖北工业大学校博士科研启动基金(BSQD2017043)

Foundation item: National Natural Science Foundation of China (90818018, 91018009, 61170022, 91118003, 61373039); Huawei

Technologies Co. Ltd Project (YB2015090035); Doctoral Research Startup Foundation of Hubei University of Technology (BSQD2017

043)

收稿时间: 2018-07-20; 修改时间: 2018-10-27, 2019-03-04; 采用时间: 2019-05-22; jos 在线出版时间: 2019-08-09

CNKI 网络优先出版: 2019-08-12 12:08:23, http://kns.cnki.net/kcms/detail/11.2560.TP.20190812.1208.013.html

江南等:机械化定理证明研究综述

Key words: theorem proving; proof assistant; resolution; natural deduction; typed



-calculus; logics of programming; refinement

计算机已经渗透到社会生产和人类生活的方方面面,与计算机相关的各种故障足以造成巨大的经济损失.

2017 年,全球爆发的勒索病毒(WannaCry)源于 Windows 操作系统的漏洞(MS17-010);早在 1994 年,奔腾处理器

的浮点除运算错误使得英特尔公司不得不召回成百上千万芯片,损失约 4.5 亿.更为严格的研发方法,能够避免

许多这样的错误.在这些方法中,机械化定理证明是被学术界广泛认可的形式验证技术

[1]

,并在工业界获得了越

来越多的成功应用.

机械化定理证明是指使用计算机,以定理证明的方式对数学定理或计算机软、硬件系统进行形式验证,是

人工智能(artificial intelligence,简称 AI)的一种体现.Leibniz 早在 17 世纪时就形成了由机器证明定理的思想,然

而直到 19 世纪末现代逻辑的创立和发展,以及 20 世纪 40 年代计算机的出现,才使得这一设想的实现具有了现

实可能性

[2]

始于 20 世纪 50 年代和 60 年代,机械化定理证明围绕计算机如何高度自动化地完成证明而展开.受当时倡

导的人工智能潜能的影响,自动定理证明(automated theorem proving,简称 ATP) 技术的研究经历了一段炽热的

研发期,也取得了许多具有影响力的成果;但是随着新问题、新技术和新思想的到来,完全自动定理证明的研究

渐入停滞期,对于大多数有意义的数学定理或计算机系统的正确性,交互式地进行证明可能是唯一可行的工作

方式

[3]

交互式定理证明(interactive theorem proving,简称 ITP)在 20 世纪 60 年代开始呈现,交互式定理证明工具也

称为证明助手(proof assistant).交互式意味着用户能够引导证明过程,在这个过程中,用户使用某种语言编写证

明纲要(outline);证明助手自动填充证明的细节,并检查证明,最终机器完成整个形式证明.这种证明纲要的思想

最初体现在 Wang 于 1960 年的著作中

[4]

.McCarthy 在 1961 年也指出:相比完全手工的数学证明,由计算机检查

的证明(纲要)可能更为简短和易于编写;在证明(纲要)的引导下,计算机能够生成大量证明细节,并检查每步证

明的正确性;这些大量的、机械性的证明工作对于实际定理的证明来讲,人工是很难胜任的

[5]

自动定理证明最初旨在证明数学定理.不过,McCarthy 同时指出:计算机能够检查的不仅仅是数学证明,而

且还包括复杂工程系统以及计算机程序是否符合它们的规范.事实正是如此,从 20 世纪 60 年代晚期开始,人们

认识到许多其他问题,譬如程序属性、专家系统和集成电路设计相关的许多问题等,都可以表示为定理,而由自

动定理证明工具予以解决

[6]

.并且,对于程序的机械化验证而言,交互式方式比完全自动化更为适用,也促进了许

多研究从完全自动化转换到交互式方式.

机械化定理证明的研究发展至今,已经产生了比较成熟的证明助手,如 Isabelle/HOL(http://isabelle.in.

tum.de/)、Coq(https://coq.inria.fr/)、HOL4(https://hol-theorem-prover.org/)、ACL2(http://www.cs.utexas.edu/users/

moore/acl2/)等.经过许多年的努力,分别在 Coq 和 Isabelle/HOL 的支持下,出现了首个验证的 C 优化编译器,称为

CompCert

[79]

,以及第一个验证的操作系统微内核 seL4

[1012]

,已应用于安全攸关的工业开发中.这一领域的研究

已经催生了每年举办的交互式定理证明(interactive theorem proving,简称 ITP)国际会议,全世界范围的研究者们

在这一会议上分享自己的研究成果.许多有关数据结构和算法分析、深度学习算法以及文件比较算法等研究成

果也正在被机器验证

[1316]

这些研究结果究竟是如何取得的?19 世纪末,德国哲学家、逻辑学家及数学家 Frege 试图证明“所有数学都

可归为逻辑”,结果创立了谓词逻辑;20 世纪,德国数学家 Hilbert 试图证明数学是没有矛盾的,他创建了现代证明

理论;荷兰数学家和哲学家 Brouwer 同样为了研究数学基础而开创了直觉主义的数学哲学

[17]

.建立在这些基础

之上,许多数学家、逻辑学家和计算机科学家在进一步研究的过程中提出了新的理论,在实践中不断发现新问

题,并给出有意义的解决方案.机械化定理证明的理论基石和支撑技术就来自这些交织进行的研究发展,并在长

达约 60 多年的持续研究过程中稳步向前推进.本文重点关注了对机械化定理证明具有重要影响力的理论和技

术、相应的实现以及它们的应用.

本文第 1 节阐述与机械化定理证明紧密相关的概念和理论、主流或具有持续影响力的技术,并剖析它们之

of 31

免费下载

软件学报计算机技术

关注

评论