幾何機器明證引發(fā)的思考

張景中，彭翕成，鄒 宇

幾何機器明證引發(fā)的思考

張景中1，2，彭翕成1，鄒 宇2

（1．華中師范大學 國家數字化學習工程技術研究中心，湖北 武漢 430079；2．廣州大學計算科技研究院，廣東 廣州 510006）

時代發(fā)展要求教育資源智能化，而不是簡單的“電子化”．智能解答能在教育領域得以應用的基本要求是能被人理解接受，即有很好的可讀性．最新研究表明，人類的解答未必是最好的，計算機可能給出讓人驚訝的解答．計算機給出的解答甚至比題干還短，這看似“有?！背ＷR，但又引起思考，如何知識表示才能盡量簡潔而又方便推理．知識的創(chuàng)新表示，要盡量符合信息時代的要求，同時也可能造成原有知識體系的重新定位．

人工智能；教育應用；幾何定理；機器明證；知識表示和推理

1 教育智能化是時代發(fā)展的必然要求

2016年AlphaGo橫空出世，擊敗了人類圍棋世界冠軍，人機博弈舉世矚目，言必稱“人工智能”的時代已經到來[1-4]．人工智能研究包含但不限于以下研究課題：自然語言理解、數據庫的智能檢索、專家咨詢系統(tǒng)、博弈、機器人學、自動程序設計、定理證明等．這里研究的幾何定理機器證明屬于定理證明領域的分支，包括如何讓計算機自動出題以及解答．

解題研究是數學教學中的重要組成部分．學習數學離不開解題．學生要通過解題練習來掌握數學知識，老師需要通過試題分析來幫助學生提高．師生們面對各種難題，不會做怎么辦？考試出題人壓力更大，總被要求出題要有新意．一年當中，考試繁多，對題目需求量大，那么多的新題從何而來？

這些問題存在多年．對于出題人而言，雖絞盡腦汁創(chuàng)新，但由于受到習慣思維的約束，與已有試題“撞車”也是常事．與之相對的是，廣大師生（甚至包括家長）為解不出題，又找不到答案而苦惱．因此近十年來，各種題庫網站（包括APP）如雨后春筍般冒出，如菁優(yōu)網、魔方格、猿題庫、學霸君、作業(yè)幫等，頗受歡迎．其中智能手機的普及和拍照搜題技術的發(fā)展在其中起了很大的推動作用．只是題庫再大，畢竟有限．對題庫中沒有的題目，就無能為力了．所以，在線題庫相對紙質版的題典，只是題量更大，搜索更便捷．在智能化方面，并沒有本質提升．缺少智能性或智能化程度不高是現有教學資源的一大通病[5-6]．

因此，利用計算機來研究智能化地命題和解題，很有現實意義．計算機出題，可不受已有題目的干擾，容易創(chuàng)新．如同AlphaGo下棋，很多招法超出人的想象．計算機解題，則可與已有題庫網站形成互補．題庫網站主要解決題庫已有題目，而計算機解題系統(tǒng)可解決題庫中沒有的題目．對于題庫已有題目，計算機解答系統(tǒng)也可以生成解答，對照檢驗，看原有解答是否正確，又可給學習者提供多種解答思路．這也為接下來的自動批改打下基礎．

目前從宏觀上討論人工智能與教育應用的文章已經很多了，這里將分享作者最近從事幾何定理機器證明的一些思考．

2 機器證明可讀性是教育應用的基本要求

人工智能發(fā)展幾十年，發(fā)表了海量的學術論文．發(fā)展到一定階段，需要總結思考．在一些學術會議上，有人提出：人從小學到中學，讀書12年，到了18歲成年時，要通過高考，那么目前的計算機能否通過高考？這需要通過實踐來檢驗．

中國在2015年啟動了一個有關類人答題的863項目，其中包括初等數學的類人答題，要求計算機給出能被高考閱卷人認可的解答，解答所使用的方法和知識點必須在中小學課標范圍之內．2017年6月7日，國產高考機器人挑戰(zhàn)北京卷文科數學以及全國二卷文科數學的考試，分別用時22分鐘和10分鐘，得分為105分和100分．這是一個相當不錯的成績．這一成績的取得，與中國科研工作者長期的努力是分不開的．

1959年，IBM公司的Gelernter（曾參加1956年的達特茅斯會議）等人提出了后推搜索法來解幾何題，這一研究是20世紀50年代人工智能領域代表性成果之一，大大激發(fā)了人們對定理機器證明的興趣，確立了其在人工智能研究領域中的重要地位．但直到1976年，機器解答幾何題還停留在很初級的階段，只能解決一些很簡單的問題．

1977年，由于吳文俊先生創(chuàng)造性的工作，幾何定理機器證明取得了突破性進展．吳方法能判定幾何命題的真假，但其推理常涉及多達數百項甚至上千項的多項式計算，過程繁瑣，人們難以理解這些多項式的幾何意義，或者說證明的可讀性不令人滿意，檢驗起來困難．從學術上來說，吳方法在理論上立得住，實踐中也有章可循，甚至有些簡單問題手算都可以完成．但從教育應用而言，可讀性差嚴重影響推廣普及．

以吳方法為代表的代數方法大獲成功，人們自然希望乘勝追擊，對機器證明提出了更高的要求．在之后多次有關機器證明的國際學術會議上，都有人提出這樣的問題：能不能由計算機給出易于理解、易于檢驗的證明，即所謂可讀的證明？

定理的證明應該被同行檢驗，這是學術慣例．當年四色問題的機器證明不可讀，引發(fā)了一場哲學討論：什么才算一個數學證明？一般認為是，立足于一系列公理，從概念、定義、已有定理出發(fā)，采用演繹推理，得到新的結論．證明一方面要說服自己，當解答者理清思路，認識從模糊到清晰，才可能得出一個推理正確的證明．證明同時也要說服他人．所以一個好的證明除了推理正確，簡潔明了也很重要．畢竟其他人未必有足夠的時間和興趣來檢驗你的證明．因此有觀點認為[7]，證明就是某一特定時間，被某一特殊群體接受的解釋．Thomas Tymoczko認為[8]，數學證明應該有說服力（convincing）、可檢驗（surveyable）、形式化（formalizable）．用數學同行公認的語言進行表達，是為同行檢驗提供基礎；而檢驗的目的則是為了說服同行，得到學術共同體的認可．如果證明不可檢驗，形式化的工作白做，也不可能說服同行，因此可檢驗非常重要[9]．

是否“易于理解、檢驗”，是一個模糊概念，因人而異．數學水平高、知識面豐富的，當然理解能力強．對于教育應用而言，必須假定讀者對象為中學師生．

機器能否生成可讀證明？數理邏輯專家王浩先生認為，機器證明本質是用量的復雜來代替質的困難．吳文俊先生進一步指出，人作幾何題，可根據不同情形找尋不同的巧法，巧則巧矣，卻是一題一法；機器證明要用統(tǒng)一算法解決不同問題，解題過程不可能簡捷．機器證明是用冗繁但有章可循的計算來代替簡捷巧妙但法無定法的推演．

盡管已有權威的論斷，但仍然有研究者沒有放棄．1992年，張景中等[10]提出了面積消點法，實現了“可讀證明（readable proof）”．在當時看來，人能讀懂的機器證明，是極好的了，能與人工證明媲美了．

葉征等[11]認為，幾何定理常有圖形輔助，閱讀證明時需反復比對證明文本和文本所對圖形中的幾何元素．如判定三角形全等，首先要在圖形中找到這兩個三角形，然后判定這兩個三角形是否大致全等，之后再繼續(xù)．當證明較長，或幾何圖形變復雜，不管是人工證明，還是機器證明，即使所謂的可讀證明也會變得不易閱讀和理解．因此提出幾何定理可視證明（visually proof），希望采用計算機圖形動畫等方式幫助理解，使得幾何證明變得直觀．實踐表明，這是一種有效的方式．

問題是，當證明很長時，即便每一步都有幾何意義，即便每一步都有動畫輔助，讀者依然會感到吃力，難以堅持讀下去．可見，可視證明有助于讀者理解證明，但治標不治本．揚湯止沸，不如釜底抽薪．只有改善證明本身，使其變得簡短易懂，才可能根本解決．

楊路等[12]在攻克不等式機器證明這一難題時，提出了“明證（certificate）”這一目標，即證明一旦給出，讀者無需太多專業(yè)知識，很容易就能判斷證明是否正確，甚至是一目了然的．明證都無需專家審稿，普通讀者就能檢驗．

一個不等式，一旦寫成平方和的形式，其結論一目了然．那么，幾何問題能否也實現“明證”，一行搞定？

一方面來說，幾何問題實現明證，要比不等式容易．因為不等式涉及“高次”，且變量多．幾何題雖有時也涉及“高次”，但多數情況下是一次、二次；幾何題雖從未限定過點、線、圓的個數，但多數情況下個數都不太多．但從另外角度來說，幾何題要實現明證，又要比不等式難得多．因為不等式（這里主要指代數不等式）本身就是代數關系式，具備轉化變形的基礎．而幾何題涉及的幾何關系，需要通過轉換成代數形式，才有可能列出希望的“一行等式”．也就是幾何題比不等式多了一道轉化手續(xù)．解析幾何雖能實現幾何、代數之間的轉化，但表示幾何關系和表示幾何關系之間的關系十分繁瑣．因此有必要研究新的幾何表示，使得能簡潔明了表示幾何關系；又要找到一種比較簡單的方法，將幾何關系之間連接起來．

3 信息時代促使知識表示的再創(chuàng)造

一個知識點，往往存在多種表述形式．知識在傳遞給學生的時候，很有必要進行批判再加工．這里的批判，主要不是懷疑這些知識的正確性，而是檢查它在教育上的適用性．要用系統(tǒng)科學的觀點，聯系前后左右的教學，聯系學生的心理特征與年齡特征，看一看，問一問，哪種反映方式較優(yōu)？能不能找到更優(yōu)或最優(yōu)的反映方式．

學習幾何，可選歐氏幾何，或解析幾何，或向量幾何，或質點幾何，甚至可以創(chuàng)造新的幾何體系．哪種方案能更快更好地完成這一階段數學教育的任務呢？這需要仔細考察．在信息時代，還需要考慮該體系是否能被計算機簡單地形式化處理．

以中點為例加以說明．怎么表示點是線段的中點？方法很多．

文字描述：點是線段的中點．

圖形描述（圖1）：

圖1

歐氏幾何描述：=．但不要漏掉：、、共線，否則只能說明點在線段的中垂線上．

中位線定理：

重心定理：

圖2

四邊形是平行四邊形的充要條件是：

．

等式簡單變形，能得到新的幾何性質，說明這一體系易于擴展，生成新的知識．就是從這樣平凡之處著手，建立了點幾何體系[13-18]，并實現了多種基于點幾何的自動推理算法，其中以點幾何恒等式算法尤為漂亮．

從知識工程[19]的角度來看，知識獲取和知識表示是從人類已有的知識源進行抽取總結，并轉化成形式化的知識，便于用于問題求解．所謂形式化，是指利用計算機能接受并進行處理的符號和方式來表示人類知識．符號表示是指用符號和符號結構來表示各種概念和概念之間的關系．知識表示的選擇應滿足：① 充分表達領域知識；② 有利于運用知識進行推理，有利于提高搜索速度及推理效率；③ 便于知識的維護和管理；④ 便于理解和實現．

建構一種新的幾何體系，雖是為教育的目的，但若與計算機處理知識的方式吻合，則更加符合現代化教育的需求．在實現點幾何解答系統(tǒng)的過程中發(fā)現，點幾何體系的建立，符合知識工程的要求．而超過千例的計算機解題實踐更是表明，點幾何不僅符合數學直觀，能更方便地表達基本幾何事實，而且有助于幾何推理的簡捷化．下面僅舉兩例說明．

圖3

證法1：

[0]：點、、、共圓

[1]：∠=∠(0)

[2]：是平行四邊形

[3]：∥(2)

[4]：∠=∠(3)

[5]：∠=∠(1 4)

[6]：點、、、共圓

[7]：∠=∠(6)

[8]：△∽△(5 7)

[9]：/=/(8)

[10]：∠=∠(0)

[11]：∠=∠(3)

[12]：∠=∠(10 11)

[13]：∠=∠(0)

[14]：△∽△(12 13)

[15]：/=/(14)

[16]：/=/(9 15)

例2 如圖4，△的邊為定長，若邊的中線為定長，試求頂點的軌跡．

圖4

4 幾何定理明證引發(fā)的思考

思考1：人類的證明是最好的么？

在AlphaGo的對戰(zhàn)中，人類千百年來積累的千錘百煉的定式一次次被推翻．AlphaGo也走出了人類公認為壞棋的招法，但最終效果卻很好．棋手們長期形成的圍棋觀被顛覆，需要重新思考：什么是好棋，什么是壞棋？

目前研究的機器解答，大多有一個定語，叫類人解答．也就是希望機器和人生成的解答盡可能類似，甚至是能混淆．這一方面是很早之前圖靈測試的期待，另一方面也是教育應用的需要．問題是，人類解法也是多樣的，有平凡無奇的俗解，也有構思奇特的巧解，甚至還有妙不可言的神仙手，如同天外飛仙，超出常人所想．

人類解法之中，有高有低，長期以來人工智能專家追求的是計算機模仿生成人類的一般解法，因為套路化，方便操作．智能解答領域，能否像AlphaGo那樣，生成人類感到驚奇的解法呢．最新的研究表明，這是可能做到的．人給出的證明未必完美，機器證明可能超過人，給出更漂亮的解答．基于點幾何恒等式算法完成的例題解答有著很好的可讀性，因此具備出版并應用于中學教育的可能．目前已與兩家出版社達成出版意向．華東師范大學出版社出版《點幾何解題》，主要介紹點幾何在解數學競賽題方面的應用．科學出版社出版《點幾何》，主要介紹點幾何的教育價值和教育應用，以及自動推理算法介紹，并輔以翔實案例說明．這兩本書里的題目，大部分來自人工收集，少部分由計算機自動生成，解答主要由機器完成，人只在其中增加少量連詞和分析，使得讀起來更加順暢．計算機生成對聯、詩歌早有先例，此次生成幾何題集，在教育應用中效果如何，拭目以待．

思考2：解答能否比題干短？如何表示知識是最簡短的？

已有數學家證明，有些定理即使最短的證明也會很長很長．那么對于一般的初等幾何問題，證明最短能短到什么程度，能否短到與題干一樣長，甚至更短？從“常識”來說，題干由若干條件和結論組成，條件看起來是零散的，條件之間存在隱藏的邏輯關系，而解答正是要把這些隱藏的邏輯關系找出來，隱藏關系顯現化的過程常常需要引入其它定理來說明，這樣才能將零散的條件（每個條件至少要用一次）串成一個完整的邏輯鏈，完成證明．這“必然”使得證明比題干要長，甚至有的要長幾倍，甚至十幾倍．一個兩三行的幾何題，證明花費一兩頁的，并不少見．這真的是必然的嗎？

最近的研究表明，只要采取一種比較簡潔而幾何意義豐富的知識表示形式，以及找到一種簡單的推理方式，是可以做到解答比題干還短的．推而廣之，如何使得知識表示簡單而意義豐富，推理簡明容易實現，效率高且易于理解，這是一項很有研究意義又任重道遠的工作．若能成功，即使是某一領域的部分成功，也能使得現有的推理體系大大簡化，人們對事物之間關系看得更加清楚，大大減輕教與學的負擔．

思考3：新的知識表示方式，可能造成原有的知識體系重新定位．

近幾十年來，為了適應信息時代的需要，世界各國的中學數學教材都做了相應的改變，主要表現在對傳統(tǒng)的初等數學進行了改造，滲透現代數學思想和方法．20世紀60年代，以新數學運動為代表的教育改革運動，喊出了“歐幾里得滾蛋”“打倒歐家店”的口號．英國一位教授認為[20]：“這幾十年來，學生沒有學系統(tǒng)的平面幾何，英國并沒有出現科學人才危機，可見學不學歐氏幾何無關緊要．”歐氏幾何當然有其學習價值．只是信息時代需要學習的內容比以前大大增加了，而課時有限，如何進一步精簡綜合學習內容，值得研究．

歐氏幾何自《幾何原本》算起，已有兩千多年．學習的難點，是構造千變萬化的輔助線，使得圖形中出現全等或相似圖形．讓學生掌握輔助線的添加，需要花費大量時間，但對進一步數學學習的用處卻并不明顯．而最新的點幾何恒等式解題研究，其實質是將幾何關系用向量形式表示，然后判斷條件和結論之間是否“線性相關”．也就是表面研究的是初等幾何，實際滲透的是高等代數的思想，為高等數學的學習打下基礎．采用新的知識表示，會使得原來看似不相關的知識體系變得連通起來，對原來的知識體系的價值也要重新定位評估．在信息化高速發(fā)展的今天，知識體系的改造盡量符合知識工程的需求也是大勢所趨．

[1] TURING A M. Computing machinery and intelligence [J]. Mind, 1950, 59 (236): 433-460.

[2] 吳砥，饒景陽，王美倩．智能教育：人工智能時代的教育變革[J]．人工智能，2019（3）：119-124．

[3] 馬玉慧，柏茂林，周政．智慧教育時代我國人工智能教育應用的發(fā)展路徑探究——美國《規(guī)劃未來，迎接人工智能時代》報告解讀及啟示[J]．電化教育研究，2017，38（3）：125-130．

[4] 宋靈青，許林．人工智能教育應用的邏輯起點與邊界——以知識學習為例[J]．中國電化教育，2019（6）：14-20．

[5] 張景中，李傳中．自動推理與教育軟件智能平臺[J]．廣州大學學報（綜合版），2001，15（2）：1-6．

[6] 張景中．自動推理與教育技術的結合[J]．中國青年科技，2001（8）：26-28．

[7] BALACHEFF N. Processus de preuves et situations de validation [J]. Educational Studies, 1987, 18 (2): 147-176.

[8] TYMOCZKO T. The four-color problem and its philosophical significance [J]. The Journal of Philosophy, 1979, 76 (2): 57-83．

[9] 張曉貴．對數學證明的審查與數學可謬性[J]．科學技術哲學研究，2018（4）：58-62．

[10] ?CHOU S C, GAO X S, ZHANG J Z. Machine proofs in geometry [M]. Singapore: World Scientific, 1994: 155.

[11] ?YE Z, CHOU S C, GAO X S. Visually dynamic presentation of proofs in plane geometry [J]. Journal of Automated Reasoning, 2010, 45 (3): 213-241.

[12] 楊路，夏壁燦．不等式機器證明與自動發(fā)現[M]．北京：科學出版社，2008：152．

[13] 張景中．點幾何綱要[J]．高等數學研究，2018（1）：1-8．

[14] ?ZHANG J Z, PENG X C, CHEN M. Self-evident automated proving based on point geometry from the perspective of Wu’s method identity [J]. Journal of Systems Science & Complexity, 2019, 32 (1): 78-94.

[15] 張景中，彭翕成．點幾何的教育價值[J]．數學通報，2019，58（2）：1-4，12．

[16] 張景中，彭翕成．點幾何的解題應用：計算篇[J]．數學通報，2019，58（3）：1-5，58．

[17] 彭翕成，張景中．點幾何的解題應用：恒等式篇[J]．數學通報，2019，58（4）：11-15．

[18] 彭翕成，張景中．點幾何的解題應用：復數恒等式篇[J]．數學通報，2019，58（5）：1-4．

[19] 楊炳儒．基于內在認知機理的知識發(fā)現理論[M]．北京：國防工業(yè)出版社，2009：37．

[20] 張奠宙．數學教育改革的十個問題[J]．教育學報，1993（3）：12-15．

Thinking Inspired by Geometric Machine Certificate

ZHANG Jing-zhong1, 2, PENG Xi-cheng1, ZOU Yu2

(1. National Engineering Research Center for E-Learning, Central China Normal University, Hubei Wuhan 430079, China;2. Institute of Computing Science and Technology, Guangzhou University, Guangdong Guangzhou 510006, China)

The development of times requires intelligent education resources, rather than simple “electronic”. The basic requirement that intelligent solutions can be applied in the field of education is that they can be understood and accepted by people, that is, they have good readability. Our latest research suggests that human solutions are not necessarily the best, and that computers may offer surprising solutions. The fact that a computer gives a solution even shorter than the stem of the problem seems “contrary” to common sense, but it also leads to the question of how to represent knowledge in such a way as to be as concise and convenient as possible for reasoning. The innovation representation of knowledge should conform to the requirements of the information age as far as possible, and at the same time may cause the repositioning of the original knowledge system.

artificial intelligence; educational application; geometric theorems; machine certificate; knowledge representation and reasoning

2019-12-20

國家自然科學基金項目——點幾何及其機器證明（11701118）

張景中（1936—），男，河南汝南人，中國科學院院士，研究員，博士生導師，主要從事機器證明、教育數學和教育技術研究．彭翕成為本文通訊作者．

G40-03

A

1004-9894（2020）01-0001-05

張景中，彭翕成，鄒宇．幾何機器明證引發(fā)的思考[J]．數學教育學報，2020，29（1）：1-5．

[責任編校：周學智、張楠]