符號主義和連接主義是人工智能方法的兩大流派,。歷史上，作為連接主義的代表,，人工神經(jīng)網(wǎng)絡(luò)幾經(jīng)沉浮,，目前攀上了發(fā)展的巔峰，高歌猛進,、如火如荼,；而符號主義發(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)角度,，和機械臂的伸縮，使得機械手達到目標(biāo)位置,，從而可以實現(xiàn)抓取,。這被稱為是逆向運動學(xué)問題（inverse kinematics），需要求解多項式方程組,，而吳方法正是解多項式方程組的有力武器,。

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

在機械制造,、機械加工領(lǐng)域,，雖然3D打印技術(shù)突飛猛進，但是對于金屬機械部件的制造加工主要還是依賴于數(shù)控機床（Computer Numerical Control Machine）,。如果加工器件的幾何形狀復(fù)雜,，需要用到五軸聯(lián)動的數(shù)控機床,，如圖3所示。在數(shù)控技術(shù)中,，機械零件一般用分片有理多項式來表示（NURBS）,，加工刀具的軌跡和零件在空中的運動軌跡需要精確配合，以達到加工精度要求,。這里,，零件的表面是代數(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ù)控機床加工方案,，進行參數(shù)樣條曲面隱式化,，求解代數(shù)幾何問題等等，從而廣泛應(yīng)用于純粹數(shù)學(xué),、計算數(shù)學(xué)以及眾多工程領(lǐng)域。

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