|
|
为什么机器验证的形式化证明没有被数学界广泛采用？
关注者
660
被浏览
156,790
11 个回答
目前而言，形式化证明的确没有广泛的被数学届采用。主要原因包括：
- 自动化程度。能够用来形式化数学的定理证明器通常基于有相当表达力的逻辑（如HOL和CIC等），而在这类逻辑上的全自动推理还是相当困难的，与之相对的是弱表达力但是强自动化的逻辑如一阶逻辑甚至布尔逻辑。不可避免的，在高表达力的逻辑下进行证明需要相当的人工引导，所以这类证明系统被称之为交互式定理证明器(interactive theorem prover)。如何提高自动化（减少人工）一直是该领域的研究方向之一，而（提高）自动化的方法主要基于两类：a) 在不影响正确(soundness)的前提下，把一部分高表达力的逻辑下的问题转化到高自动化的逻辑中，并用成熟的自动定理证明器(如Z3,CVC4,Vampire,E,Spass等)来求解；b) 针对特定种类问题实现特定的策略(tactic), 比如当我们在定理证明中里遇到这样的一阶实数类问题 \forall x \in \mathbb{R}.\, x^2+2 x + 1\geq0 该如何解决？(目前的主流证明器中方法是sums-of-suquares，有兴趣的同学可以自行搜索)。尽管在过去三十年定理证明器中的自动化程度已经有了长足的提升，我们还是希望可以进一步的减少形式化证明的成本。目前而言，在已有前置定理的情况下，在Isabelle证明器中形式化分析类的证明平均一页需要一到两周。
- 数学定理的证明是有先后的，比如我们只能在形式化了Cauchy’s Integral Theorem之后才能开始Cauchy’s Residue Theorem以及Prime Number Theorem的证明。考虑到目前已被形式化的结果离前沿数学还有相当的距离，在这个方面我们还需要等待形式化的结果在各主流定理证明器中的积累。当然我们也可以直接假设一些重要的结果，不过这样会极大地损害我们对当前证明结果正确性的信心，毕竟我们是希望每一条证明出来的定理都能基于定理证明器核(kernel)中假设的显而易见的公理。
- 用户习惯。一定年纪的传统数学家还是比较难以接受在定理证明器中形式化自己的证明。所幸，不少新一代的数学／计算机学家对形式化证明已有一定的了解，包括CMU,Cambridge在内的大学都开设了相关的课程。一个做类型理论(type theory)的大佬曾经开玩笑说：“我们无法教授现在的数学家们形式证明，我们只要等待这一代数学家死掉了就好”(We can’t teach them (mathematicians) proof assistants. We just need to wait for them to die out.)。
- 交互界面，证明管理。形式化证明和码代码(C++,Java)没有本质上的区别，这里面都要涉及命名、重构、函数（定理）搜索等问题。对于写代码我们有包括Visual Studio等的大型集成开发环境(IDE),相比之下基于Emacs(Coq, HOL, PVS) 和jEdit(Isabelle)的定理证明开发环境还略显不足。
- 各主流的证明器采用不同的底层逻辑与基础定义。证明器有着不同的底层逻辑，包括基于集合论的Mizar (untyped set theory)和Isabelle/HOL(simply-typed set theory)，与基于类型论的Coq。 除以0的问题：Isabelle中定义x/0=0,Coq里通过依赖类型(dependent type)的方式要求用户排除这种情况。不同的证明范式给统一的数学形式化也造成了一定的困难。
尽管如此，形式化证明精确(no ambiguity)，高可信度(almost no “obviously” / gaps / bugs)且在一些时候相对可读(legible)的特点已经在数学界引起了不少人的注意。
比如，以下是一个在Isabelle定理证明器中,关于质数的平方根不是有理数的证明：
在Isabelle定理证明器的支持下，计算机能理解以上的证明并且能检查每一步推理的正确性（基于所假设的公理）。另外，这样的机械化证明也具有了一定的可读性(human readable)：完全不懂形式化证明的同学，也可以在不运行证明器的情况下对以上证明的思路有大致的概念。
另外一个例子。在Isabelle/HOL中，我们已经有了对Jordan Curve Theorem的形式化,其命题表述如下(当然证明就不在这里展开了)：
形式化证明的精确性体现在命题中各个函数都是被准确地机械化定义的，从而命题本身也不会有模凌两可的情况。比如其中的“有界”(bounded)定义如下：
而“边界”(frontier)有着如此定义：
另外，有兴趣的同学也可以看看前段时间在剑桥的Big Proof研讨会：
Isaac Newton Institute for Mathematical Sciences
不少大佬都在会上发表了自己对数学形式化的看法。其中一个比较有意思的设想是在大规模形式化还不现实的当下，鼓励大家在写数学文章的时候提交一个形式化的摘要（不需要证明，仅仅是对所解决问题的形式化表述）。
综合来说，形式化证明在数学上还处于启蒙阶段，但相信这样严格、精确、高可信的证明方式在以后会有着更大的影响力也能被更多的数学家所接受。
在此缅怀Michael J. C. Gordon, FRS 和 Vladimir Voevodsky。
形式化证明没有被广泛采用的原因有很多，但主要原因正如问题里提到的，一是复杂性，二是表达力。这个回答主要针对主流的，逻辑框架是类型论的定理证明器。
复杂性：
机器证明之所以诞生，是由于数学家有使证明 error-free 的需求。要在一个交互式定理证明器里形式化一个定理，用户会被要求填补上所有的技术细节，小到哪怕是一个MP规则。这就使得数学家感到在定理证明器中写证明非常繁琐。为了令机器自动填补平凡的细节，就需要写 tactics 来完成自动化。所谓“写 tactics”，有两种意思，一是指数学家使用 tactics 来构造证明，一些 tactics 常自带 unification 这样简单的自动化，这就免去了手动构造 proof terms 时需要补完所有细节的麻烦。二是指用户可以写自己的 tactics，这使得数学家可以根据自己的需求来添加自动化。
tactics 固然好，麻烦也有很多。第一种意义的使用 tactics，虽然减轻了使用者的负担，但会相应降低证明的可读性。这一方面是因为 tactics 通常是自结论开始反向应用定理，另一方面是因为有些tactics 会引入比较底层的定理。我们知道主流的定理证明器是基于类型论的，这样的系统里底层的定理通常是 type-theoretic 的。如果 type-theoretic 的定理被引入，比如像调用 recursor 的定理，就会使展开后的 proof terms 非常不好看，非常地不（常规意义上的）数学。数学家读写证明的目的之一是理解证明并从中提炼有用的想法；使用 tactics 写的证明相对难以理解，数学家自然就丧失了不少兴趣。第二种意义的使用 tactics 则加深了阅读困难，因为 tactics 本质是一段指引证明搜索的程序，大量的自定义 tactics 使得读证明变成读代码。更重要的是，因为 tactics 是一段代码，它本身的正确性是没有逻辑框架保证的，如果学过递归论，会知道不存在 tactics 验证程序，这使得读 tactics 比读错误的证明更容易浪费时间。
因此机器证明的复杂性是个两难的问题，如果减轻了使用者的负担，那么读者的负担就会加重，反之亦然。而这还是在假定用户和读者都熟悉类型论的情况下。要用好主流的定理证明器，熟悉类型论是必不可少的，而要精通类型论，对 lambda 演算和证明论就不得不有一定的了解，要学好证明论，又需要有扎实的数理逻辑功底，这些 prerequisites 都不是一两年内能积累起来的，所以形式化证明是有一定的学习成本的。
表达力：
表达力相对于复杂性的影响没有那么大。如果暂时不考虑“人类所能理解的所有数学内容”的精确定义，通常认为 CIC 是足以形式化数学家所要解决的问题的。但是 CIC 也有问题，它作为形式化全部数学的系统，不像 ZFC 那么简洁，“类型“也不具备“集合”那样的直观。要在类型论里定义一个数学对象，由于不能采用 ZFC 的公理和通常数学教材里的集合论定义，用户必须知道如何用类型论的语言来描述直观。
比如对于有穷树，集合论里可以定义一棵有穷树为一个图 T ，拥有一个节点 \rho(T) 使得对任意 \delta\in V(T) 存在唯一的 T 中的 \rho(T)\delta -路径。而一个图 G 则由一个有限集 V(G) 和 V(G)\times V(G) 上的一个子集 E(G) 组成。如果 \delta,\eta\in T ，那么一条 \delta\eta -路径是一个节点的有限序列 \delta_0,...,\delta_n 使得 \delta_0=\delta, \delta_n=\eta 并且对任意 i = 1,...,n 有 (\delta_{i-1},\delta_i)\in E(G) 。而在类型论里，要直接描述这个定义就相当繁琐，首先是类型论中简单定义的集合性质不同于集合论中的集合（比如你无法说出传递集）。其次，在集合上取卡式积，就其定义和应用而言都远没有在类型上定义的卡式积方便，这是因为在类型上定义的函数一旦被限制在集合上，会要求额外的定理来描述函数的性质。所以用户需要原生地在类型论中定义有穷树，这通常需要利用 inductive types 来完成：
\frac{t_1,...,t_n\in T}{cons~t_1...t_n \in T}
其中 0\le n 。实际实现中，由于 n=0 时会造成没有归纳基础，你可能需要引入一个单独的构造子 node ，或者用一些类型论技巧，比如利用定义 f:fin~n\to tree 来获得简洁优雅的良定义。
在表达力方面，通常不是系统本身有所限制，而是用户对类型论了解的多少限制了使用定理证明器的深度。
其实就复杂性和表达力两点总结而言，就是对使用形式化证明技术的数学家的类型论和逻辑要求非常高。不了解类型论，就难以找到合适地表达定理的方法，也难以优雅地构造 proof terms。如果要以 tactics 方式自定义 domain-specific 的自动化，那么又会在类型论的基础上加上对证明论和模型论的了解。你首先需要知道你想处理的目标理论是什么，比如是带有等词的完全一阶逻辑，还是无量词的 equational logic，还是它的 universal 片段？对每一个目标理论，你需要考虑：这个理论是可判定的吗？它有有穷模型性质吗？它接受量词消去吗？它接受 cut elimination 进而获得子公式性质吗？如果是可判定的，它的完备且高效的判定过程是什么？如果这个理论是半可判定的，那么应该怎样设计 heuristic ？要回答这些问题，用户就需要对递归论，模型论，和传统的判定过程有一定了解。这就是为什么说，数理逻辑中最能够被计算机科学应用的是（结构）证明论，（初等）模型论和（在 \omega 上的经典）递归论。
回到问题，将来有没有可能借助机器学习来做定理证明呢？当然是可能的，但是至今都没有突破性的方法，Alan Bundy 的圈子里的人尝试了 premise selection，虽然有一定效果，但是对于关键的构造 proof terms 并没有涉及。我们想知道的是，比如，机器学习有能力在读了数百万个证明后准确实例化某个引理中的存在量词吗？数学家又是如何洞察到一个特殊而复杂的数学对象满足引理中描述的某个性质的？
想起来答辩时老板问我的最后一个问题是，你觉得十年内，你做的这个定理的形式化，能被完全自动化吗，或者说机器能做到什么程度？我跟他说我完全看不到任何希望，我不知道什么算法能让机器具备数学家的直观。其实这倒不是我说的，是两年前我问老板时他自己跟我说的，他当时的说法是，他有生之年恐怕都看不到希望，虽然说得很委婉。
但是如果哪天机器真的完全实现了自动推理，那恐怕我们离强AI也就不远了。