符號主義和連接主義是人工智能方法的兩大流派。歷史上，作為連接主義的代表，人工神經(jīng)網(wǎng)絡(luò)幾經(jīng)沉浮，目前攀上了發(fā)展的巔峰，高歌猛進(jìn)、如火如荼；而符號主義發(fā)展的巔峰之一，是吳文俊先生開創(chuàng)的機器定理證明。

吳先生曾經(jīng)指出，源自希臘的西方數(shù)學(xué)主要遵循“公理化”的原則來搭建理論大廈；而中國古代數(shù)學(xué)的傳統(tǒng)卻著重于構(gòu)造性算法化的證明，因而適合現(xiàn)代計算機科學(xué)發(fā)展的脈絡(luò)。

公理化系統(tǒng)首先建立一系列“不可辯駁”的公理（axioms），然后通過邏輯演算來推演引理、定理和推論，從而推演出整個理論體系。只要承認(rèn)公理，那么所有的推導(dǎo)結(jié)果必然自動為真。特別是所有的推演過程都可以嚴(yán)格檢驗，由機械完成。數(shù)千年來，公理化方法已經(jīng)成為各門科學(xué)發(fā)展的范式，從歐幾里得幾何，到牛頓力學(xué)，再到廣義相對論。在數(shù)學(xué)的所有分支幾乎都是以公理化系統(tǒng)為歷史總結(jié)，成為這一分支成熟的標(biāo)志，例如同調(diào)論（homology Theory）。饒有興味的是，在數(shù)學(xué)中許多艱深的概念由于過于抽象，無法直接描述，反而以更為抽象的公理化方法來加以定義，比如Milnor介紹矢量叢的Stiefel-Whitney示性類的概念就是用如此手法，然后又異常迂回曲折地構(gòu)造了一個真正的實例。

歷史上，以希爾伯特（Hilbert）為代表的數(shù)學(xué)家力圖用公理化方法來統(tǒng)一整個數(shù)學(xué)，建立一個包羅萬象的公理系統(tǒng)，來囊括所有的數(shù)學(xué)真理。哥德爾的不完備性定理否定了這一宏偉藍(lán)圖。哥德爾證明任意一個包含初等數(shù)論的公理系統(tǒng)，并且是自洽的，它必定包含某些命題，這些命題的真?zhèn)螣o法被該系統(tǒng)證明；如果此系統(tǒng)無矛盾，則其無矛盾性不可能在此系統(tǒng)內(nèi)證明。這意味著，對于任意包含有限公理的形式系統(tǒng)，存在一條數(shù)學(xué)真理，此系統(tǒng)可以表述但是無法證明，因此真理的探索過程是無止境的；同時，這一系統(tǒng)的無矛盾性，必須由其他系統(tǒng)來證明。這種現(xiàn)象比比皆是，例如某一數(shù)學(xué)領(lǐng)域最為根本的定理，往往用另外數(shù)學(xué)領(lǐng)域的方法來證明，代數(shù)的基本定理是說多項式方程存在根，這一定理只能用拓?fù)浞椒▉碜C明。

歐幾里得幾何的公理體系不包含初等數(shù)論，它是完備的。長期以來，人類經(jīng)過大量的生產(chǎn)實踐，都認(rèn)為歐幾里得幾何的幾條公理不證自明，是唯一“真實”的幾何。后來，羅巴切夫斯基將第五公設(shè)“過直線外一點存在一條平行線”修改成“過直線外一點存在無窮多條平行線”，通過邏輯演繹，建立了雙曲幾何。如果將此公設(shè)改成“過直線外一點不存在平行線”，則可以得到球面幾何。長期以來，人們一直將雙曲幾何和球面幾何作為純粹智力游戲的產(chǎn)物，傾向于認(rèn)為它們沒有真實的物理基礎(chǔ)。依隨科學(xué)的發(fā)展，歐氏幾何、球面幾何和雙曲幾何都成為黎曼幾何的特例，廣義相對論的建立使人們相信黎曼幾何物理真實性，從而不再糾結(jié)邏輯演繹結(jié)論的物理基礎(chǔ)。歷史的發(fā)展總是依循“否定之否定”的規(guī)律，共形幾何的發(fā)展揭示了所有的二維黎曼流形，在保角變換下都可以歸結(jié)為球面幾何、歐氏幾何和雙曲幾何中的一種，如圖1所示。近些年來，依隨計算機科學(xué)的發(fā)展，幾乎所有的曲面幾何計算問題都可以歸結(jié)在這些標(biāo)準(zhǔn)空間中的計算問題，因此對于這三種古老而“正統(tǒng)”的幾何研究日益復(fù)蘇。

圖1.曲面單值化定理，所有度量曲面歸結(jié)為球面幾何、歐氏幾何和雙曲幾何。

吳文俊先生為了弘揚中國數(shù)學(xué)構(gòu)造性算法化的傳統(tǒng)，將數(shù)學(xué)（特別是代數(shù)幾何）與計算機科學(xué)相結(jié)合，開創(chuàng)了機器幾何定理證明的方向，只手擎天地推動了數(shù)學(xué)機械化的發(fā)展。吳先生認(rèn)為在很大程度上，人們可以用復(fù)雜的計算推演來代替抽象的推理，從而用計算機來輔助數(shù)學(xué)家去發(fā)現(xiàn)自然結(jié)構(gòu)、獲取數(shù)學(xué)真理。吳先生發(fā)明的吳方法，完全可以證明所有歐幾里得幾何的定理，同時被廣泛應(yīng)用于許多數(shù)學(xué)和工程領(lǐng)域。

基于吳方法的自動幾何定理定理證明大致步驟如下：

1. 將幾何問題代數(shù)化，將給定的幾何條件翻譯成多項式方程，（hypothesis polynormials），將幾何結(jié)論也翻譯成多項式 （conclusion polynormials）

2. 用偽除方法（pseudodivision）將條件多項式變換成三角列形式，

代數(shù)簇包含條件多項式生成的代數(shù)簇的不可約分支（irreducible components）

3. 用三角列中的多項式偽除結(jié)論多項式，如果余式非0，則我們說命題不成立；

4. 檢查非退化條件，如果非退化條件滿足（所有初式的乘積非零），則我們說結(jié)論多項式由條件多項式生成。

圖2. 三角形垂心定理。

例如我們來證明三角形垂心定理：如圖2所示，三角形的頂點坐標(biāo)是

，

三個垂足為

，

由垂直條件得到多項式方程

,

我們假設(shè)AD和CE交于G點，AD和BF交于H點，。由G、E、C三點共線，H、B、F三點共線，增加方程

我們需要證明G和H重合，即 。

我們可以用吳方法來證明結(jié)論多項式可以由條件多項式推出，從而證明了垂心定理。很多時候，機器給出的證明非常出人意料，更為簡潔巧妙。

吳方法可以用來求解多項式方程組。將一般的多項式方程組化解為三角列形式，非常類似于線性方程組的高斯消元法（Gauss elimination）。我們通過數(shù)值方法求解單變元多項式，求得；然后將代入第二個方程，求得；再將，代入第三個方程

，求得；以此類推，逐步求得所有的未知變量

。

圖3. 機械臂逆向運動學(xué)。

在機器人（robotics）領(lǐng)域，機械臂路徑規(guī)劃是一個經(jīng)典問題。一條機械臂有多個關(guān)節(jié)，每個關(guān)節(jié)有旋轉(zhuǎn)自由度或者伸縮自由度，我們將這些自由度由變元

表示。機械手的位置和朝向由這些變元控制，同時它們可以表示成多項式函數(shù):

同時我們有限制 。在機器人應(yīng)用中，機器人通過三維掃描獲得物體的三維幾何位置信息，從而得到最終機械手的位置和朝向，通過反解各個關(guān)節(jié)的旋轉(zhuǎn)角度，和機械臂的伸縮，使得機械手達(dá)到目標(biāo)位置，從而可以實現(xiàn)抓取。這被稱為是逆向運動學(xué)問題（inverse kinematics），需要求解多項式方程組，而吳方法正是解多項式方程組的有力武器。

圖4. 五軸聯(lián)動數(shù)控機床（5-Axis CNC Machine）。

在機械制造、機械加工領(lǐng)域，雖然3D打印技術(shù)突飛猛進(jìn)，但是對于金屬機械部件的制造加工主要還是依賴于數(shù)控機床（Computer Numerical Control Machine）。如果加工器件的幾何形狀復(fù)雜，需要用到五軸聯(lián)動的數(shù)控機床，如圖3所示。在數(shù)控技術(shù)中，機械零件一般用分片有理多項式來表示（NURBS），加工刀具的軌跡和零件在空中的運動軌跡需要精確配合，以達(dá)到加工精度要求。這里，零件的表面是代數(shù)曲面，曲面上的軌線是代數(shù)曲線。加工時轉(zhuǎn)頭盡量垂直于曲面，同時控制運行速度和加數(shù)度，以及刀具施加的力量。如果加速度過大，有可能直接損壞刀具或零件。這里，需要求解大量的多項式方程組，吳方法在這個領(lǐng)域中大顯神威。

圖5. 光線跟蹤法渲染的猶他壺。（Ray Tracing Utah Teapot）

在計算機圖形學(xué)中，光線跟蹤法（Ray Tracing）提供了高質(zhì)量真實感繪制效果，因而在電影動漫中被廣泛應(yīng)用。許多曲面被表示成帶參數(shù)的樣條曲面（Spline Surface），即為分片多項式或者有理多項式，其一般表示形式為

,

這里是分片多項式，如圖5所示的猶他壺模型（Utah Teapot）。在光線跟蹤法中，每條光形被表示成一條射線 ，我們需要計算射線和曲面的交點，這占據(jù)了整個計算時間的以上。直接用曲面的參數(shù)形式計算交點比較困難，我們需要將曲面變換成隱式形式，即為，這一過程被稱為是參數(shù)曲面的隱式化。將射線方程代入隱式曲面，求解關(guān)于t的一元多項式方程，可以求解交點。參數(shù)曲面的隱式化可以直接應(yīng)用吳方法，消去變元，即得隱式曲面。

在計算機圖形學(xué)和計算機視覺中，形狀分析（shape analysis）是一個基本問題。形狀的整體對稱性是一個重要的指標(biāo)，近些年來曾經(jīng)引發(fā)過研究熱潮。這個問題的數(shù)學(xué)提法如下：給定一個帶度量的曲面，是一個微分同胚映射，滿足特定條件，所有這種映射構(gòu)成一個群，被稱為是曲面的對稱變換群。問題的核心是如何計算這個群。

例如，如果曲面嵌入在三維歐氏空間中，是歐氏空間的剛體變換（rigid motion），則被稱為是所謂的外蘊對稱變換群（extrinsic symmetry group）；如果是等距變換（isometry），即保持測地距離不變，

，

這里代表由度量所決定的兩點間的測地距離，或者表示成由誘導(dǎo)的拉回度量等于初始度量: 。這樣的群被稱為是內(nèi)蘊對稱群（intrinsic symmetry group）。

內(nèi)蘊和外蘊對稱比較容易理解，但是有一種對稱非常隱蔽，無法被人類直覺體會到，不過用代數(shù)幾何的方法卻非常簡單直觀：共形對稱。所謂的共形變換（conformal transformation）就是保持角度的變換，拉回度量和初始度量相差一個正的標(biāo)量函數(shù)，

。

由所有共形變換構(gòu)成的群被稱為共形對稱群（Conformal Symmetry Group）。

絕大多數(shù)的拓?fù)鋸?fù)雜曲面，其共形對稱群平庸，即只包含恒同映射。但是有一大類曲面，其共形變換群包含兩個元素

，

這種變換被稱為是對合變換（involution），這種曲面被稱為是超橢圓曲面（hyper-elliptic）。所有虧格為二的封閉曲面，嵌在三維歐氏空間之中，都是超橢圓的。那么，如何計算對合映射呢？

曲面的黎曼度量誘導(dǎo)局部的等溫坐標(biāo)，使得。所有的局部等溫坐標(biāo)構(gòu)成曲面的復(fù)解析結(jié)構(gòu)。周煒良定理表明，復(fù)射影空間

中的解析流形必是代數(shù)的。換言之，給定一個封閉帶度量曲面，則存在一個多項式定義的二維曲面，兩者之間存在共形雙射。

被稱為是的代數(shù)曲線表示。如果是超橢圓的，則其代數(shù)曲線可以變換成標(biāo)準(zhǔn)形式：

，

顯然，對合映射具有形式

。

所有對合映射的不動點（fixed point）被稱為是Weierstrass point。在標(biāo)準(zhǔn)度量（雙曲度量）下，如果一條測地線都把曲面分割成多個聯(lián)通分支，則此測地線必然經(jīng)過Weierstrass point。

圖6. 超橢圓曲面和對合映射。

如圖6所示，給定一個虧格為二的雕塑曲面，我們用Ricci 流計算其標(biāo)準(zhǔn)雙曲度量，求出Weierstrass Points，然后計算曲面上半純函數(shù)域（Meromorphic funciton field），轉(zhuǎn)換成代數(shù)曲線，。然后用吳方法，經(jīng)過雙有理變換變換成標(biāo)準(zhǔn)形式，由此得到對合映射。圖中，曲面被分解成兩個部分，對合映射將一部分映到另外一個部分。吳方法給出了計算曲面共形對稱群的方法。

我們看到，吳方法提供了非?；镜乃惴?，能夠求解多項式方程組，證明初等幾何定理，計算機器人路徑規(guī)劃，生成數(shù)控機床加工方案，進(jìn)行參數(shù)樣條曲面隱式化，求解代數(shù)幾何問題等等，從而廣泛應(yīng)用于純粹數(shù)學(xué)、計算數(shù)學(xué)以及眾多工程領(lǐng)域。

吳方法為人工智能的符號計算提供了堅實的理論基礎(chǔ)和高效的算法，特別是算法的每一步驟都可以被人類透徹理解，它代表了智能中嚴(yán)密清晰的邏輯思維層面，和連接主義中概率模糊的感性直覺層面互補。我們相信，在未來，吳方法必將在人工智能領(lǐng)域再放異彩。吳文俊先生的光輝思想將會被后人深入挖掘，繼承發(fā)揚，彪炳千秋！