几何定理机器证明是指通过机器自动地证明几何定理,常用的证明方法可分为三类：代数法、向量法以及基于推理数据库的搜索法。上述三类方法都属于确定性方法,即只要按正确的步骤计算执行,总能得到确定性的结果。然而,当涉及到复杂问题时,确定性方法的复杂度会偏高,从而严重影响到解题的效率。于是,便有了与“确定性”方法相对应的能够高效执行的“概率性”方法。为此,国外已有研究学者开始探索概率性方法在几何定理机器证明的应用,并取得了一定的成效。但是目前国内尚未有人对概率性方法进行研究,并且已有的确定性方法和概率性方法尚存在复杂度过高或者对非线性类构造性几何定理的证明力度偏弱等问题。本文针对已有的确定性方法和概率性方法的证明速率偏低或占用内存过大等问题,从代数簇构造理论出发,对几何定理机器证明的概率性方法做了以下研究工作：(1)提出一种改进的估算余式次数上界的算法。分析构造性几何定理的多项式组代数簇的不可约分解的基本特点,在此基础上提出了一种改进的估算余式R(结合假设部分的多项式组消去结论部分多项式的全部约束变元后得到的只含独立变元的多项式)关于每个独立变元次数的上界的快速算法。在改进的算法的基础上,成功推导出构造性几何定理的余式R关于每个独立变元次数的上界满足Bound1=O(30[n/2])。此外,若定理限制为线性类的构造性几何定理,则还可将其上界改进为Bound2=O(3n)。(2)提出三种统计总体采集标准。在改进算法和相关推论基础上,结合Schwartz-Zippel定理和统计学理论,提出了三种不同的具有一定针对性和适用范围的统计总体采集标准。其中,第一和第二种采集标准是基于改进的算法提出来的,而第三种则是针对改进算法的推论提出来的,二者具有不同的适应范围。在实验部分,我们还设计了对比实验对这三种采集标准的适用范围进行分析和评价。(3)比较分析两种实例检验方法。给出两种不同的随机实例检验方法,即数值检验法和连续伪除检验法。文中还进一步探讨了这两种检验方法对退化情况及多项式组可约性情况的处理方法。最后还结合多组对比实验数据对这两种不同的检验方法的适用性进行评价。(4)开发基于概率检测组合模型的几何定理证明器——-ProbProvero在上述理论研究和分析的基础上,本文还进一步设计了概率检测组合模型并对模型进行了显著性检验及统计错误分析。进一步地,我们采用Maple编程语言实现此基于概率检测组合模型的几何定理证明器——ProbProver。通过ProbProver证明器,我们成功在2秒内证明了代数法难以证明的Five Circles和Miquel定理。为了进一步证实本文提出的基于概率检测组合模型的几何定理证明器具有一定的高效性,本文从多个维度出发,对若干个复杂程度不尽相同的几何定理进行了多组重复实验。实验数据表明,本文提出的基于概率检测组合模型的几何定理证明器具有显著的高效性,并具有一定的应用前景。