彪炳千秋吴方法

符号主义和连接主义是人工智能方法的两大流派。历史上，作为连接主义的代表，人工神经网络几经沉浮，目前攀上了发展的巅峰，高歌猛进、如火如荼；而符号主义发展的巅峰之一，是吴文俊先生开创的机器定理证明。

吴先生曾经指出，源自希腊的西方数学主要遵循“公理化”的原则来搭建理论大厦；而中国古代数学的传统却着重于构造性算法化的证明，因而适合现代计算机科学发展的脉络。

公理化系统首先建立一系列“不可辩驳”的公理（axioms），然后通过逻辑演算来推演引理、定理和推论，从而推演出整个理论体系。只要承认公理，那么所有的推导结果必然自动为真。特别是所有的推演过程都可以严格检验，由机械完成。数千年来，公理化方法已经成为各门科学发展的范式，从欧几里得几何，到牛顿力学，再到广义相对论。在数学的所有分支几乎都是以公理化系统为历史总结，成为这一分支成熟的标志，例如同调论（homology Theory）。饶有兴味的是，在数学中许多艰深的概念由于过于抽象，无法直接描述，反而以更为抽象的公理化方法来加以定义，比如Milnor介绍矢量丛的Stiefel-Whitney示性类的概念就是用如此手法，然后又异常迂回曲折地构造了一个真正的实例。

历史上，以希尔伯特（Hilbert）为代表的数学家力图用公理化方法来统一整个数学，建立一个包罗万象的公理系统，来囊括所有的数学真理。哥德尔的不完备性定理否定了这一宏伟蓝图。哥德尔证明任意一个包含初等数论的公理系统，并且是自洽的，它必定包含某些命题，这些命题的真伪无法被该系统证明；如果此系统无矛盾，则其无矛盾性不可能在此系统内证明。这意味着，对于任意包含有限公理的形式系统，存在一条数学真理，此系统可以表述但是无法证明，因此真理的探索过程是无止境的；同时，这一系统的无矛盾性，必须由其他系统来证明。这种现象比比皆是，例如某一数学领域最为根本的定理，往往用另外数学领域的方法来证明，代数的基本定理是说多项式方程存在根，这一定理只能用拓扑方法来证明。

欧几里得几何的公理体系不包含初等数论，它是完备的。长期以来，人类经过大量的生产实践，都认为欧几里得几何的几条公理不证自明，是唯一“真实”的几何。后来，罗巴切夫斯基将第五公设“过直线外一点存在一条平行线”修改成“过直线外一点存在无穷多条平行线”，通过逻辑演绎，建立了双曲几何。如果将此公设改成“过直线外一点不存在平行线”，则可以得到球面几何。长期以来，人们一直将双曲几何和球面几何作为纯粹智力游戏的产物，倾向于认为它们没有真实的物理基础。依随科学的发展，欧氏几何、球面几何和双曲几何都成为黎曼几何的特例，广义相对论的建立使人们相信黎曼几何物理真实性，从而不再纠结逻辑演绎结论的物理基础。历史的发展总是依循“否定之否定”的规律，共形几何的发展揭示了所有的二维黎曼流形，在保角变换下都可以归结为球面几何、欧氏几何和双曲几何中的一种，如图1所示。近些年来，依随计算机科学的发展，几乎所有的曲面几何计算问题都可以归结在这些标准空间中的计算问题，因此对于这三种古老而“正统”的几何研究日益复苏。

图1.曲面单值化定理，所有度量曲面归结为球面几何、欧氏几何和双曲几何。

吴文俊先生为了弘扬中国数学构造性算法化的传统，将数学（特别是代数几何）与计算机科学相结合，开创了机器几何定理证明的方向，只手擎天地推动了数学机械化的发展。吴先生认为在很大程度上，人们可以用复杂的计算推演来代替抽象的推理，从而用计算机来辅助数学家去发现自然结构、获取数学真理。吴先生发明的吴方法，完全可以证明所有欧几里得几何的定理，同时被广泛应用于许多数学和工程领域。

机器几何定理证明

基于吴方法的自动几何定理定理证明大致步骤如下：

1. 将几何问题代数化，将给定的几何条件翻译成多项式方程，（hypothesis polynormials）

，将几何结论也翻译成多项式

（conclusion polynormials）

2. 用伪除方法（pseudodivision）将条件多项式变换成三角列形式，

代数簇

包含条件多项式生成的代数簇的不可约分支（irreducible components）

3. 用三角列中的多项式伪除结论多项式，如果余式非0，则我们说命题不成立；

4. 检查非退化条件，如果非退化条件满足（所有初式的乘积非零），则我们说结论多项式由条件多项式生成。

图2. 三角形垂心定理。

例如我们来证明三角形垂心定理：如图2所示，三角形的顶点坐标是

，

三个垂足为

，

由垂直条件得到多项式方程

,

我们假设AD和CE交于G点，AD和BF交于H点，

。由G、E、C三点共线，H、B、F三点共线，增加方程

我们需要证明G和H重合，即

。

我们可以用吴方法来证明结论多项式可以由条件多项式推出，从而证明了垂心定理。很多时候，机器给出的证明非常出人意料，更为简洁巧妙。

机器人路径规划

吴方法可以用来求解多项式方程组。将一般的多项式方程组化解为三角列形式，非常类似于线性方程组的高斯消元法（Gauss elimination）。我们通过数值方法求解单变元多项式

，求得

；然后将

代入第二个方程

，求得

；再将

，

代入第三个方程

，求得

；以此类推，逐步求得所有的未知变量

。

图3. 机械臂逆向运动学。

在机器人（robotics）领域，机械臂路径规划是一个经典问题。一条机械臂有多个关节，每个关节有旋转自由度或者伸缩自由度，我们将这些自由度由变元

表示。机械手的位置和朝向由这些变元控制，同时它们可以表示成多项式函数:

同时我们有限制

。在机器人应用中，机器人通过三维扫描获得物体的三维几何位置信息，从而得到最终机械手的位置和朝向，通过反解各个关节的旋转角度，和机械臂的伸缩，使得机械手达到目标位置，从而可以实现抓取。这被称为是逆向运动学问题（inverse kinematics），需要求解多项式方程组，而吴方法正是解多项式方程组的有力武器。

数控机床

图4. 五轴联动数控机床（5-Axis CNC Machine）。

在机械制造、机械加工领域，虽然3D打印技术突飞猛进，但是对于金属机械部件的制造加工主要还是依赖于数控机床（Computer Numerical Control Machine）。如果加工器件的几何形状复杂，需要用到五轴联动的数控机床，如图3所示。在数控技术中，机械零件一般用分片有理多项式来表示（NURBS），加工刀具的轨迹和零件在空中的运动轨迹需要精确配合，以达到加工精度要求。这里，零件的表面是代数曲面，曲面上的轨线是代数曲线。加工时转头尽量垂直于曲面，同时控制运行速度和加数度，以及刀具施加的力量。如果加速度过大，有可能直接损坏刀具或零件。这里，需要求解大量的多项式方程组，吴方法在这个领域中大显神威。

计算机图形学

图5. 光线跟踪法渲染的犹他壶。（Ray Tracing Utah Teapot）

在计算机图形学中，光线跟踪法（Ray Tracing）提供了高质量真实感绘制效果，因而在电影动漫中被广泛应用。许多曲面被表示成带参数的样条曲面（Spline Surface），即为分片多项式或者有理多项式，其一般表示形式为

,

这里

是分片多项式，如图5所示的犹他壶模型（Utah Teapot）。在光线跟踪法中，每条光形被表示成一条射线

，我们需要计算射线和曲面的交点，这占据了整个计算时间的

以上。直接用曲面的参数形式计算交点比较困难，我们需要将曲面变换成隐式形式，即为

，这一过程被称为是参数曲面的隐式化。将射线方程代入隐式曲面，求解关于t的一元多项式方程，可以求解交点。参数曲面的隐式化可以直接应用吴方法，消去变元

，即得隐式曲面。

计算机视学

在计算机图形学和计算机视觉中，形状分析（shape analysis）是一个基本问题。形状的整体对称性是一个重要的指标，近些年来曾经引发过研究热潮。这个问题的数学提法如下：给定一个带度量的曲面

，

是一个微分同胚映射，满足特定条件，所有这种映射

构成一个群，被称为是曲面的对称变换群

。问题的核心是如何计算这个群

。

例如，如果曲面嵌入在三维欧氏空间中，

是欧氏空间的刚体变换（rigid motion），则

被称为是所谓的外蕴对称变换群（extrinsic symmetry group）；如果

是等距变换（isometry），即

保持测地距离不变，

，

这里

代表由度量

所决定的两点间的测地距离，或者表示成由

诱导的拉回度量等于初始度量:

。这样的群被称为是内蕴对称群（intrinsic symmetry group）。

内蕴和外蕴对称比较容易理解，但是有一种对称非常隐蔽，无法被人类直觉体会到，不过用代数几何的方法却非常简单直观：共形对称。所谓的共形变换（conformal transformation）就是保持角度的变换，拉回度量和初始度量相差一个正的标量函数，

。

由所有共形变换构成的群被称为共形对称群（Conformal Symmetry Group）。

绝大多数的拓扑复杂曲面，其共形对称群平庸，即只包含恒同映射。但是有一大类曲面，其共形变换群包含两个元素

，

这种变换被称为是对合变换（involution），这种曲面被称为是超椭圆曲面（hyper-elliptic）。所有亏格为二的封闭曲面，嵌在三维欧氏空间之中，都是超椭圆的。那么，如何计算对合映射呢？

曲面的黎曼度量诱导局部的等温坐标

，使得

。所有的局部等温坐标构成曲面的复解析结构。周炜良定理表明，复射影空间

中的解析流形必是代数的。换言之，给定一个封闭带度量曲面

，则存在一个多项式定义的二维曲面

，两者之间存在共形双射。

被称为是

的代数曲线表示。如果

是超椭圆的，则其代数曲线可以变换成标准形式：

，

显然，对合映射具有形式

。

所有对合映射的不动点（fixed point）被称为是Weierstrass point。在标准度量（双曲度量）下，如果一条测地线都把曲面分割成多个联通分支，则此测地线必然经过Weierstrass point。

图6. 超椭圆曲面和对合映射。

如图6所示，给定一个亏格为二的雕塑曲面，我们用Ricci 流计算其标准双曲度量，求出Weierstrass Points，然后计算曲面上半纯函数域（Meromorphic funciton field），转换成代数曲线，

。然后用吴方法，经过双有理变换变换成标准形式

，由此得到对合映射。图中，曲面被分解成两个部分，对合映射将一部分映到另外一个部分。吴方法给出了计算曲面共形对称群的方法。

总结

我们看到，吴方法提供了非常基本的算法，能够求解多项式方程组，证明初等几何定理，计算机器人路径规划，生成数控机床加工方案，进行参数样条曲面隐式化，求解代数几何问题等等，从而广泛应用于纯粹数学、计算数学以及众多工程领域。

吴方法为人工智能的符号计算提供了坚实的理论基础和高效的算法，特别是算法的每一步骤都可以被人类透彻理解，它代表了智能中严密清晰的逻辑思维层面，和连接主义中概率模糊的感性直觉层面互补。我们相信，在未来，吴方法必将在人工智能领域再放异彩。吴文俊先生的光辉思想将会被后人深入挖掘，继承发扬，彪炳千秋！

---