摘 要:
将几何定理机器证明的研究方法概括为确定性算法与概率性算法两大类，针对已有的确定性算法和概率性算法的证明速率偏低或占用内存过大等问题，提出一种改进的概率性算法。主要是在改进对多项式中独立变元次数的上界估计的算法的基础上，结合SchwartzZippel定理和统计学理论，通过随机检验若干实例来证明几何定理，并能控制证明结果不真的概率在给定的小范围内。通过改进的概率性算法，成功在2秒内证明出代数法难以证明的五圆定理。最后的多组对比实验进一步表明，改进的概率性算法具有明显高效性。
关键词:几何定理机器证明；确定性算法；概率性算法；构造性几何；变元次数上界
中图分类号: TP181
文献标志码:A
英文标题
Improved probabilistic algorithm of mechanical geometry theorem proving
英文作者名
CHEN Mingyan1*, ZENG Zhenbing2
英文地址(
1.Shanghai Key Laboratory of Trustworthy Computing(East China Normal University), Shanghai 200062, China;
2.Department of Mathematics, Shanghai University, Shanghai 200444, China
英文摘要)
Abstract:
The research methods of mechanical geometry theorem proving were summed up into two categories, deterministic algorithms and probabilistic algorithms, and then an improved probabilistic algorithm was proposed to overcome the drawbacks such as poor efficiency or memory consumption in the existing methods. That was, the upper bounds of the degrees of variables in the pseudoremainder were estimated by adopting an improved algorithm, and then on the basis of combining SchwartzZippel theorem and statistical theory, a geometric theorem could be proved by checking several random instances, the probability of error result could also be calculated and controlled within any given small range. Through the improved probabilistic algorithm, the Five Circles Theorem had already been proved successfully within two seconds which is quite difficult to be proved by existing algebra methods for its high complexity. Comparative experiment results also show that the improved probabilistic algorithm is high efficient.
英文关键词Key words:
mechanical geometry theorem proving; deterministic algorithm; probabilistic algorithm; constructive geometry; upper bound of the degree of variable
0 引言
几何定理机器证明是指通过机器自动地证明几何定理，是数学机械化的重要部分。常用的方法可分为三种：代数法、向量法及基于推理数据库的搜索法。其中，代数法的证明效率最高。代数法又包括吴方法［1-2］、Grbner基方法［3］、结式消元法［4］、例证法［5］、数值并行法［6-8］等。吴方法是代数方法的代表，是吴文俊于1977年提出来的一种用代数的方法来证明几何定理的方法。其他几种代数法则是在吴方法思想影响和启发下提出来的。通常，在最坏的情况下，Grbner基方法的算法复杂度会呈现双指数。与Grbner基方法相比，吴方法的算法复杂度相对较低，但当涉及到较复杂的几何定理时，吴方法和Grbner基方法都会因中间计算过程过度膨胀而出现瓶颈。1986年，洪加威提出一个美妙设想：若要判断一类平面几何定理是否为真，只需近似地验证一个特定的数值例子即可。
这就是著名的例证法。然而，具有高计算复杂度的例证法难以有效地在计算机上实现。后来，Hou［9］研究发展了一种这种例证法的单例实验法。继洪加威的例证法，1989年，张景中等发展的数值并行法以数值计算和并行处理方式有效地减少了内存消耗和证明时间，成为第一个具有实践性意义的数值方法［6-8］。然而，数值并行法对需要验证实例的数目及选取标准都有严格的要求，且对较复杂的几何定理而言，需要验证实例的数目会很庞大，这将严重影响证明效率。最终，张景中等结合代数法和面积等几何不变量，提出了能给出证明几何定理可读证明的方法［10-11］，并将这种方法推广到非欧几何定理的机器证明和自动发现［12］。
相同的是，上述方法以及向量法、搜索算法都属于确定性算法，即只要按正确的步骤计算执行，总能得到确定性的结果。然而，当涉及到复杂的问题时，确定性算法的复杂度会偏高，严重影响到解题的效率。于是，便有了与“确定性”算法相对应的能够高效执行的“概率性”算法［13］。概率性算法在计算机代数中的应用极为广泛，如素数判定、求解最大不变因子等。概率性算法具有两个重要特点：1)算法能够在规定时间内快速执行完毕，并返回执行结果；2)返回结果可能不真，但能将结果不真的概率控制在一定的范围内。能否用概率性算法代替确定性算法，以提高几何定理证明的效率呢？答案是肯定的。
第7期
陈明雁等：改进的几何定理机器证明的概率性算法
计算机应用 第34卷
1 概率性算法在几何定理机器证明的应用
1997年，Carrá Ferro等［14］根据SchwartzZippel定理［13,15］，结合使用吴方法，通过随机验证若干实例来证明几何定理，并给出证明结果为真的概率。其核心思想是，根据Brownawell［16］和Kollar［17］给出的关于多项式根式理想的指数的界及Gallo等［18-19］给出的关于WuRitt特征列变元的次数的界，估算伪余式全次数的上界, 据此确定随机验证实例的数目及其取值范围，最后结合SchwartzZippel定理计算证明结果正确的概率。若一个构造性几何定理由l步尺规作图构成，Carrá Ferro等估算出伪余式关于独立变元的全次数的上界为c2l33l3ll2(c为常数)。由于c2l33l3ll2的值非常庞大，致使Carrá Ferro等未能在计算机上实现其算法。