自動推理及其在數(shù)學教育中的應用.doc

自動推理及其在數(shù)學教育中的應用張景中1，2，3，彭翕成1（1.華中師范大學 教育部教育信息技術(shù)工程研究中心，武漢 430079；2.廣州大學 教育軟件研究所，廣州 510006；3. 中國科學院 成都計算機應用研究所，成都 610041；）摘要：本文介紹了自動推理的研究歷史以及研究意義，并分別從幾何作圖、符號運算、幾何證明、動畫設計和機器學習等5個方面論述了自動推理在數(shù)學教育中的應用。最后，對智能軟件的開發(fā)提出了一些建議。關(guān)鍵詞：人工智能；自動推理；智能軟件一、自動推理是人工智能中最成功的部分人工智能的研究內(nèi)容，包括人類智能的機理和如何用機器模擬人的智能。人的智能包括感知與反應（人和動物都有的智能）以及運用符號計算與進行推理（人類獨有的智能）。能看、能聽，并對看到、聽到的事情做出反應，這些智能不光是人有，很多動物都有。植物有沒有呢？植物能不能感受到外界呢？從表面現(xiàn)象看植物好像有，比如說，暖了，它慢慢就要發(fā)芽；冷了，它就要趕快結(jié)籽。北方有句俗話說“立秋十八天，寸草結(jié)籽”。植物能感知世界，但它沒有神經(jīng)系統(tǒng)，不像動物反應那么快。動物的智能是很明顯的，它能看見、聽見周圍的東西，有什么危險，有什么機遇，它都能夠感覺到，它能區(qū)別開來。譬如說我們在電視上經(jīng)常看到，一個獵豹看見羚羊，它知道是個機遇，就會去追；如果看到比它兇、比它大的動物，比方說獅子，它就會躲。這表現(xiàn)出來一種智能。但是有些智能是人才有的，會使用符號，會去推理；而動物對外界的反應都比較直接。比方說養(yǎng)豬，飼養(yǎng)員去喂它，它對飼養(yǎng)員就有好感，飼養(yǎng)員來了之后它就要叫，知道是來喂它的，但它不會推理出來：喂肥之后，將來是要殺我的，他不會無緣無故地喂我。豬沒有這個邏輯思維能力，而且一代一代地也不會傳遞這個信息。實際上，動物是沒有思維能力的，而人可以用符號，用語言推理。動物的符號是生理符號，通過發(fā)出各種不同的聲音，像鯨魚有鯨魚的聲音，海豚有海豚的聲音，以此來互相傳遞信息，但是現(xiàn)在還沒有發(fā)現(xiàn)動物使用符號，利用文字。在這一點上，人是獨特的，人可以進行很復雜的推理，這種智能是人獨有的智能。人通過推理，可以由此及彼，由表及里，去粗取精，去偽存真，所以自動推理在人工智能中是個非常重要的部分1。如果去掉了推理，就等同于一般動物的智能了。讓機器怎么看，機器怎么聽，這是不夠的，很多復雜的事情，機器還是做不了。計算機到現(xiàn)在有六十多年的歷史了，現(xiàn)在看來，自動推理是人工智能中最為成功的部分，用得也最多。人工智能的其他很多部分，雖然下了很大功夫研究，但進展比較慢。二、自動推理研究的歷史追本溯源，中國古代有一部書，叫做九章算術(shù)，它就把當時人們關(guān)心的數(shù)學問題分成九類，比方說計算體積，計算面積等等共九類，并對這九類分別給出解答。它給出的解答是機械化的，無論是數(shù)學水平高的或是低的，只要學了這個方法，按照方法操作就一定能夠找到問題的答案；而自動推理的基本思想就是希望對一類一類問題分別給出一個一個確定的，能夠機械地執(zhí)行的解決方案，所以吳文俊院士認為，“算法思想是中國古代數(shù)學中產(chǎn)生的?！蔽鞣降臄?shù)學，基本上源于古希臘的幾何，它提一些公理，提一些假設，根據(jù)這些假設，看能證明什么，一個一個定理的做。中國古代沒有提出一般的假設，沒有提出公理系統(tǒng)，只提出很多問題，針對每個問題，找出解答的方法。當然，這兩種方法在學術(shù)上講，對科學的發(fā)展各有長處。從一段時間看，中國沒有公理系統(tǒng)，在科學的發(fā)展上是受到影響了的，吃了虧的?，F(xiàn)在有了計算機，中國古代的算法思想，自動推理的思想，機械化的思想，又重新發(fā)揚光大起來。2西方古代雖然沒有算法思想，但到了十六、十七世紀，法國的笛卡爾提出一個設想： “一切問題化為數(shù)學問題，一切數(shù)學問題要化為方程組，化為代數(shù)方程組，代數(shù)方程組化為一個方程，這一個方程我們就能解決?！钡芽栠@個宏偉的計劃實現(xiàn)起來是比較困難的。比笛卡爾又晚了差不多一百多年，德國的萊布尼茨提出過用機器推理的思想。他很明確地提出要建立一門通用的語言，用符號來代表邏輯關(guān)系，這樣的話，就能做一個機器進行推理。如果在人們爭論不休的時候，讓機器推一推，看看到底誰對，但是他的通用語言沒有設計成功。 后來，建立一門通用的語言用符號來代表邏輯關(guān)系是布爾。他提出我們大家知道的布爾代數(shù)，又叫邏輯代數(shù)。計算機的邏輯運算就基于這個邏輯代數(shù)。再后來，希爾伯特提出用機械的方法證明一類的幾何問題。哪一類的呢？就是只涉及到關(guān)聯(lián)性幾何命題。什么叫關(guān)聯(lián)性？就是點在直線上，直線通過點，兩個直線相交或平行這類性質(zhì)。如果一個命題只涉及到這些性質(zhì)的話，他就有辦法能夠手到擒來。大家不要以為只涉及到關(guān)聯(lián)性質(zhì)就很簡單。其實涉及到關(guān)聯(lián)性質(zhì)的幾何定理有時比較麻煩，例如有名的帕普斯定理，巴斯卡定理。這樣的定理，很多人不知道怎么下手。希爾伯特這個設想就具有機械化的思想，但一直沒人注意到這一點，直到吳文俊院士將其指出。到希爾伯特為止，都還是在設想，是紙上談兵，因為自動推理是要用機器來推理的，但那時并沒有機器。上個世紀30年代，圖靈提出了自動機和理想的計算機的模型以及怎樣評判機器的智能的問題。40年代以后，計算機研制成功，大家對自動推理的研究就更加熱鬧了。1950年左右，塔斯基給出了初等數(shù)學的判定定理，認為是一切初等數(shù)學的問題都是可判定的。研究了幾千年的初等數(shù)學，塔斯基一個方法就能徹底解決，讓大家都很震驚。但該方法在計算機上實現(xiàn)起來需要的時間，遠遠超過了人們所能夠接受的范圍。到了1960年，美籍華人王浩設計了程序，幾分鐘之內(nèi)就證明了三百多條定理，但都是些比較簡單的邏輯定理，其中沒有幾何定理。證明幾何定理始終是比較難的問題，要證明幾何定理，要做推理，就得有計算機推理的軟件。推理涉及到符號運算，而一般的計算器都只能進行數(shù)值計算。為了用符號的演算來進行推理，就要研發(fā)能對符號進行演算的數(shù)學軟件。符號運算軟件在六十年代研發(fā)成功，是計算機科學領域里具有里程碑意義的進展。我國數(shù)學機械化研究的成果，首先是1976年，吳文俊院士在中國科學上發(fā)表了證明幾何定理的吳方法。本來幾何定理的證明在國外是非常難的，研究了二十五年，進展很慢，被稱為人工智能中最不成功的領域。有了吳法之后，最不成功的領域就變成了最成功的領域。吳先生的方法，它的特點是非常快，一個幾何命題，常常是幾秒鐘就可以回答對還是不對。但為什么對？它不能給出一個簡單的、人能夠?qū)W習的、能夠判斷的、能夠檢驗的、能夠理解的過程。所以，人們就希望進一步有可讀的證明，就是說，計算機能不能像人一樣的寫出個證明，人能夠理解。這個問題，筆者與幾位合作者在1992年把它突破了。我們提出了幾何定理可讀證明的生成方法，開始是面積方法，后來還可以推廣到其它的幾何不變量。1另外，吳文俊院士的方法是證明等式型命題的。垂直、平行、線段相等、角度等于多少度，都叫等式型的幾何命題，可以用代數(shù)的等式來表示。那么不等式的怎么辦？不等式在實踐上的用處，在現(xiàn)代科技中的運用是非常廣的。1980年，吳文俊院士在上海的一個會上說，不等式的機器證明是一大難題。這一大難題后來被楊路教授突破了，他提出的方法，可以很快地證明不等式。有人用他的方法證明了一千多個不等式，其中五百多個都是其它雜志上、書上提出來沒有解決的。自動推理有關(guān)的歷史性事件中還有兩件是比較出名的。1976年，兩個青年數(shù)學家哈肯和阿佩爾在計算機上算了1200個小時，解決了一個著名的數(shù)學難題四色定理，這成為計算機幫助人們推理，解決重大數(shù)學問題一個突出的例子。后來1997年，IBM的“深藍”戰(zhàn)勝了世界象棋冠軍，更是哄動一時，產(chǎn)生巨大的廣告效應。這充分說明計算機能夠自動推理，在某些特定的領域可以超過人腦3。 三、自動推理在數(shù)學教育中的應用 自動推理有哪些應用呢，可以說，凡是用到計算機的地方，或多或少都要用到自動推理。但用得比較多的，還是在數(shù)學方面4，5。數(shù)學活動，大體上就是作圖、計算、證明，而這三者通常是聯(lián)系在一起的。以證明一個幾何題為例，首先需要讓計算機理解題意，最好是繪制一個計算機能夠理解的圖形；推理過程中需要用到符號運算，最后才能得到證明。3.1自動推理與幾何作圖計算機作圖問題，從計算機研發(fā)成功開始，就一直受人關(guān)注。數(shù)學教育中最受歡迎的是動態(tài)幾何作圖。所謂的動態(tài)幾何：在拖動圖中某些點或某些線時，圖形在變動中能保持當初作圖時被賦予的幾何屬性不變。中點仍是中點，垂線仍是垂線，等等。通過幾何圖形的動態(tài)變化，可體現(xiàn)以前在紙上無法觀測到的幾何原理，使人能更直觀地深刻理解圖形中的幾何規(guī)律，從而達到真正理解幾何原理的目的。這種動態(tài)幾何，是上個世紀八十年代發(fā)展起來的計算機幾何作圖。動態(tài)幾何用到了自動推理，但不同的動態(tài)幾何軟件智能性是不同的。我們選取5個最基本的需求：畫點、線、圓、垂線段以及圓的切線，來對比傳統(tǒng)教學、一般動態(tài)幾何軟件和智能動態(tài)幾何軟件的優(yōu)劣性。傳統(tǒng)教學中，老師們用圓規(guī)畫圓，用三角板（或直尺）畫線（包括線段、直線、射線三種），還要用到粉筆；至于作垂線段和圓的切線，一般是拿三角板大致擺放，直接畫就。這樣的作圖操作簡單，缺陷是畫好之后，圖形靜止，不易觀察出圖形之中隱藏的幾何性質(zhì)。一般的動態(tài)幾何軟件都有3個最基本的工具，分別用來作點、線、圓，而且作線工具一般還分為線段、直線、射線三種分支工具。若要過直線外的一點向該直線作垂線段，操作上比較麻煩，以幾何畫板為例，需要16個動作，分別是(1)單擊“直尺工具”圖標；(2)作線段AB；(3)單擊“點工具”圖標；(4)作點C；(5)單擊“選擇工具”圖標；(6)選擇線段AB；(7)執(zhí)行菜單命令“構(gòu)造|垂線”，作出垂線；(8)單擊“點工具”圖標；(9)作垂線與AB的交點，即垂足；(10)單擊“選擇工具”圖標；(11)選擇垂線；(12)執(zhí)行菜單命令“顯示|隱藏垂線”；(13)單擊“直尺工具”圖標；(14)從點C到垂足連線段。其中每次執(zhí)行菜單命令都是兩個動作，總共16個動作。至于過圓外一點作該圓的切線則更麻煩，不單是操作上的麻煩，而且還需要一定的數(shù)學功底。與黑板作圖相比，最大優(yōu)點是，所作圖形能夠在拖動之后保持幾何性質(zhì)不變，有利于師生學習理解；缺點是操作較為麻煩；需要指出的是，也不是絕對的操作麻煩，譬如畫圓，黑板作圖需要轉(zhuǎn)個圈，這一操作在黑板上不是很容易進行，而用動態(tài)幾何軟件作圓，則只要用作圓工具，一點擊一拖動一松手就成，圖形相當標準。用智能動態(tài)幾何軟件作圖，除了身兼二者之長之外，還會給人帶來更多的方便。傳統(tǒng)教學中，有個別老師圖省事，把圓規(guī)的那根桿子當尺片用，這就不需要三角板了。這反映了人的一種心態(tài)，希望用較少的工具完成較多的任務。把作點、線、圓的工具合為一個工具，明顯能夠減少工具之間的切換，提高工作效率。至于作垂線段和切線，則可根據(jù)軟件的智能提示輕松完成，因為一般動態(tài)幾何軟件作圖，很多動作都是人與計算機在溝通，不是必須的動作，是可以省略的。選中智能畫筆之后，進入智能作圖狀態(tài)，計算機就時時刻刻估計揣摩人的意愿，通過鼠標的位置和狀態(tài)猜測人要作什么，及時顯示出提示向人請示。在智能作圖狀態(tài)，單擊左鍵作點，按下左鍵拖動畫線，單擊左鍵再按下左鍵拖動作圓；還可以作線段中點、平行線、垂直線、等長線段、圓的切線、圓和直線的交點、平行四邊形、等腰三角形等20多種基本幾何圖形。講課時直接畫就是，不必使用菜單，顯得更為流暢。這也就是智能化軟件的優(yōu)越性，工具的高度精簡，功能反而增強。真正的智能化軟件，其智能性是可以選擇的，適當限制其智能化程度，讓用戶用最基礎的工具進行搭建。也就是說，智能動態(tài)幾何軟件是涵蓋了一般的動態(tài)幾何軟件的。再舉個作圖有關(guān)的小例子：標注角。人去標注，會按照是不是直角來標注；一般的動態(tài)幾何軟件則分不清楚；而智能動態(tài)幾何軟件則會自動判斷是不是直角，并給予不同標注（圖1）。基本的作圖，智能軟件就體現(xiàn)出極大的優(yōu)越性；復雜作圖，可看作基本作圖的多次組合，那么優(yōu)越性就越發(fā)顯著了。 圖1除了繪制平面幾何圖形之外，函數(shù)圖象也是是中學課程中一個重要內(nèi)容，而不少同學也感覺學起來有困難。智能化軟件不但能夠迅速快速作出函數(shù)圖象，還可以對函數(shù)的一些基本要素進行分析；而且不單針對確定的函數(shù)，帶有參數(shù)的函數(shù)也同樣能夠分析。以新課程改革增加的三次函數(shù)為例，利用智能教育平臺進行函數(shù)單調(diào)性和極值的分析，畫好函數(shù)圖象之后，設置一個變量尺用來控制參數(shù)a，圖2顯示當?shù)臅r候，函數(shù)為增函數(shù)，沒有極值點；當改變參數(shù)a，當?shù)臅r候，情況變得比較復雜，如圖3所示。 圖2 圖33.2自動推理與符號運算 推理的基礎實際上是數(shù)學計算，因為邏輯推理可以化為布爾代數(shù)中的計算。在50年代，王浩就指出，用量的復雜來克服質(zhì)的困難，用大量的計算來代替推理。所以說符號運算在自動推理中有著相當重要的作用。我們舉個例子來說明符號計算。用符號計算軟件展開，它不但能很快展出來，而且能排好版。如果說是在課堂上代替老師作計算，就能給老師們帶來很大的方便。算，可以慢慢算，用楊輝三角也是算得出來的。但有時候，慢慢算也為難，譬如說做因式分解。你不知道一個多項式能不能分解。比方說，這個因式到底能不能分解，人就很難判斷。但是計算機馬上就能分解出來，分解成。像這樣分解，就要動很多腦筋。對因式分解的研究，是自動推理中很難的一塊，很多數(shù)學家，發(fā)表論文上千篇，才能作到現(xiàn)在這個程度。對計算機來說，手到擒來，馬上就可以知道，而且還可以告訴你不能再分解了。符號運算還包括計算不定積分、微分、排列組合、大數(shù)運算等諸多方面（圖4），這給我們工作學習帶來很大方便，現(xiàn)在理工科的很多項目離開符號運算軟件，根本完成不了。 圖43.3自動推理與幾何證明經(jīng)過30多年的努力，我國科研工作者取得了舉世矚目的成績?，F(xiàn)在，用自動推理軟件來證明幾何問題，已經(jīng)不僅僅簡單地判斷命題的對錯，而且可以自動生成人能夠看懂的證明過程6，7。下面這個題目是數(shù)學通報2007年第7期數(shù)學問題解答欄目的問題1683。原證法用到三角形相似和托勒密定理，而托勒密定理是現(xiàn)在的初中生不太熟悉的，而智能軟件自動生成的證明只用到了三角形相似，證明過程也比原證法簡單。這說明計算機自動生成的證明完全可以和人工證明相媲美。如圖5，在中，過A、B、C三點作圓交BD于E，過B、C、D三點作圓交CA延長線于F。求證：。 圖5 證明：0: 點B, C, D, F共圓1: BFC = BDC (0)2: ABCD是平行四邊形3: ABCD (2)4: DBA = BDC (3)5: DBA = BFC (1 4)6: 點A, B, C, E共圓7: AEB = FCB (6)8: ABEBFC (5 7)9: AB/BE=BF/CF (8)10: DBF = DCF (0)11: BAC = DCF (3)12: BAC = DBF (10 11)13: FCB = FDB (0)14: ABCBFD (12 13)15: AB/AC=BF/BD (14)16: AC/BD=BE/CF (9 15)又比如，最近十來年流行開放性題型。如果要問一個三角形和它的三條高線以及垂心（圖6），這個極為簡單的幾何圖形中有多少組成比例的線段。如果讓人去找，花費大量時間不說，而且未必能夠找全，而采用自動推理，不到3秒鐘，就能全部找出來。不單找出總共105組成比例的線段，而且找到了有42對相似三角形，相等的角有111組等信息。圖63.4自動推理與動畫設計現(xiàn)在網(wǎng)絡越來越發(fā)達，遠程教育發(fā)展很快。這中間也要用到自動推理，譬如圖像的傳輸問題。圖像文件較大，圖像組成的動畫文件則更大，占的帶寬也大。用自動推理的方法來設計動畫，可以讓動畫變得非常小。舉個例子，如圖7所示，這個動畫是一個三角形的車輪在走，為了保證車子的平穩(wěn)，路就要修成曲線的。路修成彎曲時，車子就可以走得平穩(wěn)。這個動畫如果用普通的工具來做就要占較大的空間。現(xiàn)在這個動畫不但包括三角形車輪，如果拖動下面這個尺子上的滑鈕，它可以變成四邊形的車輪。變成四邊形之后，下邊整個曲線就變了。那么再拖動一下，它就變成五邊形的了，還是這樣子地滾。六邊形、七邊形、八邊形，都可以讓它變出來，變得越多，下面的地就越平。那么這個很復雜的動畫，如果用普通做動畫的方式來做，它只做一個車輪的滾動就要占比較大的空間。如果用自動推理的方法，用數(shù)學機械化的思想，在智能教育平臺上構(gòu)造這樣一個動畫，這個文件有多大呢？如果把這個動畫做成網(wǎng)頁，只有8K。它實際上傳輸?shù)氖且幌盗忻罱M成的模型，模型的內(nèi)容包括這個動畫的制作原理，生成曲線的方程以及控制方程的參數(shù)等，這些都是文本數(shù)據(jù)，所以文件非常小。接收方根據(jù)模型，自動生成動畫即可。 圖7講到網(wǎng)絡傳輸，不能不提到網(wǎng)絡上數(shù)學公式的書寫問題。平時大家寫公式，大多采用公式編輯器。使用公式編輯器，需要在鍵盤和鼠標之間作較多的切換，極大地影響輸入速度，而且也不能直接在網(wǎng)絡上使用。而采用智能軟件，我們可以直接輸入文本，然后自動轉(zhuǎn)化為數(shù)學中所需要的形式。如圖8所示，左邊部分為輸入內(nèi)容，右邊部分為顯示內(nèi)容，其中xl表示向量，yh表示圓弧，jf表示積分，這也是為了國人的使用方便。 圖83.5 交互推理與機器學習另外很多數(shù)學問題，光用計算機很難做出來，就要用交互推理。就是計算機做一做，人出點主意，人告訴它下一步怎么做，叫交互推理。舉個例子，三角公式化簡很麻煩，我們可以做交互推理。譬如要化簡，要化成，那就要下命令, 讓機器用關(guān)系。那么對如何辦呢，讓機器用降冪公式，然后再推理。推了一步，還有平方?jīng)]有化簡，那再推一次，接著再做恒等變形，約去分子分母的公因式，就差不多了。這個例子說明人在操縱著機器，人出主意，用機器做計算推理，這是交互推理的基本思想。此外，還有機器學習的研究。機器在推理時，開始第一遍它不會，第二遍它自己就會做了。機器學習實現(xiàn)起來困難較大，雖有所進展，但不是很理想。四、智能軟件的開發(fā)需要長期努力數(shù)學活動離不開推理，所以探討數(shù)學機械化和自動推理，就很難區(qū)分。國家曾經(jīng)有個973項目，叫做數(shù)學機械化與自動推理平臺。就是說，研究的是數(shù)學機械化，最后落實要做個計算機自動推理平臺8。目前，我們在數(shù)學機械化的應用上，比方說證明幾何定理，計算機視覺，圖像壓縮等方面，有一些先進成果，但是在軟件方面，在自動推理平臺方面，我們國家還遠遠落后于世界的先進水平。目前最流行的數(shù)學機械化的軟件，一個是美國的Mathematica，一個是加拿大的Maple。在這方面，盡管973代表了我們國家最高級的科研項目，但目前我們做出來的數(shù)學軟件，在效率上還趕不上Mathematica和Maple。關(guān)鍵問題是，一要有堅實的經(jīng)濟實力作支撐，另外要持之以恒。靠一代人做幾年，或者一個小組做幾年是不行的，要一代一代的升級。自動推理也好，數(shù)學機械化也好，最基本的工具是數(shù)學軟件。凡是數(shù)學家會做的事情，編成程序，人人都能用計算機做了。這樣一來，用起來就非常方便。這樣重要的東西，如果我們長期用國外的，對我們國家科技發(fā)展是很不利的。本文提到的自動推理的一些功能，在我們研發(fā)的Z+Z智能教育平臺超級畫板中已經(jīng)基本實現(xiàn)了，有興趣的讀者可參看文9，10，也可以在/下載試用。另外，國際上比較有影響力的符號運算軟件還有Maxima和scilab，動態(tài)幾何軟件還有Geogebra，這些都是開源軟件，不存在盜版問題，大家可以放心使用。參考文獻1張景中.計算機怎樣解幾何題談談自動推理M.北京：清華大學出版社；廣州：暨南大學出版社.20002吳文俊主編.王者之路 機器證明及其應用M.長沙：湖南科學技術(shù)出版社,1999.3李傳中，張景中.智能知識平臺的構(gòu)想及其實現(xiàn)J.世界科技研究與發(fā)展.2001.64王曉波，張景中，王鵬遠.“Z+Z智能教育平臺”與數(shù)學課程整合J.信息技術(shù)教育.2006.65張景中.數(shù)學機械化與現(xiàn)代教育技術(shù).信息技術(shù)教育J.2003.016 Shang-Ching. Chou, Xiao-shan Gao,Jing-zhong Zhang. Machine Proofs in Geometry: Automated Production of Readable Proofs for Geometry TheoremsM.World Scientific,19947孫熙椿.平面幾何定理的機器證明M.南寧：廣西教育出版社,1999.8張景中，李傳中.自動推理與教育軟件智能平臺J.廣州大學學報(社會科學版).2001.29李傳中，左傳波.超級畫板范例教程M.北京：科學出版社,2004.10張景中，彭翕成.動態(tài)幾何教程M.北京：科學出版社.2007.9 Automat