机器证明
机器证明及其应用是我国攀登计划项目之一。该项目的核心内容主要是几何定理机器证明和非线性代数方程组理论、算法和应用。实际上,机器证明研究领域的范围要广泛得多。在国外则更一般地叫做自动推理。我们把几何定理机器证明和非线性代数方程组作为主攻方向,一方面是因为吴文俊先生在70年代的突出工作,使我国在此方向上具有了领先的优势;另一方面,这两个方向有鲜明的应用背景,近年来在机器证明领域也确是十分活跃的,值得重视。 由于传统的兴趣和多种原因,几何定理的机器证明在自动推理的研究中占有重要的地位。近20年来,几何定理机器证明的研究和实践有了很大的进展。 从古老的梦想到惊人的突破 能否建立一个通用的几何解题方法,成批地解决问题,以至万理一证,是历史上一些卓越科学家的梦想。 为此,笛卡尔发明了坐标系;莱布尼兹设想过推理机器;希尔伯特在其名著(几何基础)中给出了一类几何命题的机械化定理。电子计算机的出现推动了数学机械化。50年代,塔斯基用代数方法证明了初等几何的机械化的可能性。到60年代,斯拉格和莫色斯实现了符号积分,代数与分析计算问题的机械化已经初具规模,而几何定理的机器证明看来仍遥遥无期。接着,格兰特等提出用逻辑方法建立几何推理机,科林斯等改进了塔斯基的代数方法。直到1975年,仍找不到能用计算机判定非平凡几何命题的有效算法。 正当这一领域的热情由于进展缓慢而趋于冷落之际,吴文俊方法的提出给定理机器证明的研究带来勃勃生机。用吴法可在微机上很快地证明困难的几何定理。周咸青发展了吴法并把它实现为有效的通用程序,证明了512条非平凡定理,写成英文专著。这一进展是自动推理领域的一大突破,被国际同行誉为革命性的工作。 从机器判定到可读证明的自动生成 吴法的成功使一度冷落的几何定理机器证明研究活跃起来。用代数方法证明几何定理的方向受到重视。新的代数方法接连出现。在国外,周咸青等提出了用Grobner基方法构作几何定理机器证明的算法和程序并获得成功。在国内,洪家威提出了单点例证方法的理论设想,但因复杂度太大不能实现。张景中、杨路则提出数值并行方法,在低档微机(甚至计算器)上实现了非平凡几何定理的机器证明和机器发明。数值并行方法的优点是所需内存极小,且易于并行化。所有这些方法都属于代数方法。它们的提出和实现丰富了几何定理机器证明的研究。但与吴法相比,没有大的新突破。 代数方法不能使人满意的是,它所给出的"证明"是关于大多项式的繁复的计算,人难于理解其几何意义,也难于检验其是否正确。能否让计算机生成人能理解和易于检验的简明巧妙的证明,即所谓可读证明,是对自动推理和人工智能领域的一个挑战性的课题。一些著名的科学家认为,机器证明的基本思想是以量的复杂取代质的困难,这就很难想象用机器生成可读证明。国外一些学者从60年代即致力于几何定理可读证明自动生成的研究,30多年来进展不大,未能给出哪怕是一小类非平凡几何定理的机器证明的有效算法和程序。 作者以多年来所发展的几何新方法为基本工具,并提出了消点思想,和周咸青、高小山合作,于1992年突破了这一困难,实现了几何定理可读证明的自动生成。这一新方法既不以坐标为基础,也不同于传统的综合方法,而是一个以几何不变量为工具,把几何、代数、逻辑和人工智能方法结合起来所形成的开放系统。它选择几个基本的几何不变量和一套作图规则,并且建立一系列与这些不变量和作图规则有关的消点公式。当命题的前提以作图语句的形式输入时,程序可调用适当的消点公式把结论中的约束点逐个消去,最后达到水落石出。 消点的过程纪录与消点公式相结合,就是一个具有几何意义的证明。此算法对可构造等式型几何命题是完全的,但其应用范围不限于这一类命题。基于此法所编的程序,已在微机上对数以百计的困难的几何定理完全自动地生成了简短的可读证明,其效率也比其他方法为高。随所用的几何量的不同,它能生成面积法、向量法、复数法和全角法等多种风格的证明,也能用于立体几何。杨路、高小山、周咸青与作者合作,把消点法用于非欧几何可读证明的自动生成也获得成功,并得到一批非欧几何新定理。 消点法也可用于几何计算和公式推导。基于几何量和消点思想的新原理的建立,像是打开了几何定理机器求解的一个矿床。它也使几何定理机器证明的成果在数学教育中的应用有了现实可能。这一成果被国际同行誉为使计算机能像处理算术那样处理几何的发展道路上的里程碑,是自动推理领域30年来最重要的工作。 在多数情形下,消点法也可用笔纸证明不平凡的定理。它结束了两千年来几何证题无定法的局面,把初等几何解题法从四则杂题的层次推进到代数方程的阶段。 机器证明与人工证明媲美的新阶段 但是,比起人类在几千年间积累起来的丰富多彩的几何知识来,计算机目前所能做的仍是十分有限。应当把几何学家所掌握的方法更多地"教给"计算机,使计算机产生的解法可以与几何学家相比。为此,要分析几何学家有哪些解题方法,计算机已经学会了哪些,以确定下一步应当做什么和如何做。几何学家常用下列四种手段: W1.检验:对具体图形作观察和计算,以确信命题为真。 W2.搜索:依据常用的引理和已知条件去找寻题图中更多的几何性质。这样做如达不到目的,得到的信息就是进一步工作的基础。 W3.归约:从结论出发,利用已知信息消去依赖的几何量或几何元素,使结论的真假趋于显然或易于检验。 W4.转化:改变命题的形式,如几何变换、反证法、辅助线等。 手段W1的机器模拟已经实现。手段W3的机械化研究得到了最大的成功。吴法、GB法、面积法和向量法均属此类。手段W4充分体现了人的思维活动的灵活性与丰富性,尚难以机械化。手段W2,搜索,是传统几何证明活动中的常规方法,是归约的补充和转化的基础。我们基于前推模式设计并实现了一个"几何信息搜索系统"(GISS)。由于适当选择几何工具,合理组织数据和优化推理的过程,效果极好。文献中曾提出的用搜索法处理涉及圆的命题,以及找出所有可能推出的几何性质(达到推理不动点)的问题,均被我们的算法完满回答。我们的程序用C语言在NeXT工作站上实现,用于161个非平凡几何命题,均在合理的时间内达到不动点,并能发现新定理,证得其它方法不能证明的结果。程序已具有添加某些辅助线的功能。 非线性代数方程组的研究 机器生成可读证明的实现并不使代数方法失去价值。一些特殊问题及代数曲线、曲面的几何问题仍需用代数方法求解。代数方法与非线性代数方程组的理论和符号求解密切相关,有广泛应用,是自动推理的一大热点。数学、物理和工程技术中的许多问题,归根结底要靠解代数方程组。线性方程组还好办,非线性方程组就成了难关。特别是非线性方程组的符号求解,更难,理论上也更重要。 对非线性代数方程组的研究,19世纪就提出了各种结式方法。由于结式法涉及大行列式的计算,算不动,研究就冷下来。本世纪有了计算机,人们又研究新的算法。在60年代,国外提出GB法和Ritt法。GB方法是完全方法。Ritt方法经吴文俊先生改进后,也成了一种完全方法。叫Ritt-Wu方法,在我国简称吴法(把Ritt-Wu方法用于几何定理的机器证明,也叫吴法。国外有人把机器证明的吴法叫Ritt-Wu方法,是不确切的。Ritt和几何定理机器证明没有关系。)。两个方法哪个更好,目前还没有定论。用于几何定理机器证明,吴法确实比GB法强。我国学者还用吴法解决了许多重要问题,涉及理论物理、微分方程、样条理论和机器人。 虽已有了吴法、GB法等优秀的完全方法,但是道高一尺,魔高一丈,更难的问题要求更有力的新方法。近年来,国外一再提出新的思路和算法,欧共体还投资数百万美元组织项目专门研究非线性代数方程组的解法,但均无突破性进展。 最近,基于我们提出并加以完善的新的理论和算法———结式矩阵法,符红光编写了代数方程组符号求解和机器证明的MAPLE程序。新算法的特点是: (1)是非线性代数方程组符号求解和相容性判定的完全方法。 (2)不依赖于多项式的因式分解。 (3)用我们提出的弱非退化条件作零点分解,减少多余分支。 (4)子结式计算与数值检验配合,进行大范围消元。 (5)将所给方程组分解为三角列,便于机器证明和最终求解。 经许多例子的演算,它比已知的各种方法有更好的效果。此法能在PC486机上解六变量循环方程,反解各种类型的六关节机器人问题,这是其它方法做不到的。 非线性代数方程组研究的又一新进展是杨路等提出的实系数代数方程的判别式系统。这不但彻底解决了几世纪悬而未决的关于代数方程一个基本问题,也使几何不等式机器证明的难题得到了突破。杨路等最近所写的程序,能快速地证明许多几何不等式,根据已给条件推出几何不等式,并已改正和改进了国外一些关于几何不等式的结果。 展望与建议 预计在未来十年中初等几何等式型问题的机器求解将基本完成,并进入实用阶段。在前述成果的基础上,会出现新的热点: (1)在几何定理可读证明自动生成工作的影响下,用几何不变量为工具进行机器求解的研究会有新的进展。例如几何作图的机器求解,几何推理数据库的研究及微分几何可读证明的研究。 (2)几何不等式的机器求解,会随着实代数研究的进展而出现新的突破。 (3)非线性代数方程组的理论与算法,仍将是热点。结式法和插值方法等利于并行的算法会得到更多重视。 (4)微分多项式的机器推导研究将得到开展。 (5)机器证明的成果,特别是非线性代数方程组理论与算法的研究成果,将在数学、物理和工程技术中得到更多的应用。 目前,在几何定理机器证明方面,我国处于国际领先地位。在非线性代数方程组研究领域,竞争激烈,我国已进入先进行列,但还不能说领先。在数学机械化软件开发方面,由于起步晚、队伍小和资金不足等原因,我国远不及欧美先进国家。我们不应满足于某些方向上的领先地位。在继续进行几何定理机器证明研究并保持领先的同时,要把力量集中到非线性代数方程组的方向上来,特别应加强对实用而有效的算法的研究。在数学机械化推广应用方面,也应投入力量,发挥我们在理论与算法方向的优势,在软件开发方面赶超先进。在几何定理机器证明成果的基础上,开发高智能的教育软件和自主版权的符号演算数学软件,为我国科技、教育事业作出贡献。 (此文是作者在中国计算机学会第九次全国学术会议上所作的特约报告的详细摘要)