九年磨一劍，AI先鋒齊聚一試鋒芒。11月29日—12月1日， 由中國人工智能學會主辦的“第九屆吳文俊人工智能科學技術獎頒獎典禮暨2019中國人工智能產業年會”將在蘇州隆重舉辦。屆時，學會將對81個成果授獎。

伴隨智能科技的不斷深化，人工智能正在全球範圍內蓬勃興起，大批AI科技先鋒不斷湧現，他們以優質的科技成果大力推動了人工智能的發展。自2011年學會設立“吳文俊人工智能科學技術獎”以來，該獎項已成爲我國表彰、鼓勵科技從業者及企業的至高榮譽殿堂。

爲全面實施創新驅動發展戰略，貫徹落實國家《新一代人工智能發展規劃》，通過推薦評選優秀的智能科學技術成果，切實調動廣大智能科技工作者的積極性和創造性，表彰獲得2019年度吳文俊人工智能科學技術獎的學者與專家，促進人工智能技術在各行業領域賦能，大力提升我國智能科學技術創新與產業化發展水平，加快建設成爲世界人工智能創新中心和應用高地，中國人工智能學會將於 2019年11月29日—12月1日在蘇州隆重舉辦“第九屆吳文俊人工智能科學技術獎頒獎典禮暨2019中國人工智能產業年會”。誠邀您蒞臨本屆頒獎大會，共襄盛舉。

獲獎者風采

高小山，中國科學院數學與系統科學研究院研究員、常務副院長，主要從事數學機械化研究，是吳文俊開創、具有重要國際影響的數學機械化領域目前的學術帶頭人。2019年，榮獲第九屆吳文俊人工智能傑出貢獻獎。

獲獎者簡介

高小山，現任中國科學院數學與系統科學研究院研究員、常務副院長，主要從事數學機械化研究，是吳文俊開創、具有重要國際影響的數學機械化領域目前的學術帶頭人。2019年，榮獲第九屆吳文俊人工智能傑出貢獻獎。

建立了微分差分系統機器證明基本方法：微分稀疏結式、微分周形式、差分特徵列方法，實質性開拓了數學機械化的適用範圍，是數學機械化研究的重要突破。合作建立了幾何定理機器證明的消點法，首次實現了定理可讀證明的自動生成，極大提高了機器證明的質量，使定理機器證明進入到機器證明可以與傳統證明比美的新階段。針對智能CAD、機器人、計算機視覺等機器智能中的關鍵問題，發展了幾何約束求解的系統高效算法，解決了視覺定位與並聯機器人構型基本問題，將數學機械由定理機器證明開拓到自動作圖新方向。針對在高端數控智能製造多種重要實用約束，設計了快速的時間最優運動插補控制算法，在國家重大科技專項支持的商用數控系統中實現，顯著提高了數控加工精度與速度，在航空製造領域得到應用。

出版專著4部，發表論文130餘篇，谷歌學術他引4500餘次。曾獲國家自然科學二等獎（第三），中科院自然科學一等獎（第二），第36屆國際計算機學會SIGSAM/ISSAC傑出論文獎,香港求是傑出青年學者獎，第4屆亞洲數學技術會議最佳論文獎，國家十五重大科技成就網絡展，吳文俊應用數學獎，國家基金委傑出青年基金。作爲首席科學家主持三個數學機械化973項目，獲科技部“十一五國家科技計劃執行突出貢獻獎”。

獲獎理由

高小山在數學機械化研究中取得了系統與原創成果，對該領域的發展做出了重要貢獻。他提出了幾何約束求解的完整高效算法並解決了最佳空間並聯機構構型與視覺定位基本問題，將機器證明開拓到自動作圖新方向。合作建立了基於不變量的消去理論，使機器證明進入到與傳統證明比美的新階段。將數學機械化核心理論開拓到微分差分系統，開拓了機器證明的適用範圍、降低了計算複雜度。針對智能數控加工重要實用約束，設計了快速時間最優插補算法，顯著改進了加工效率與精度。

項目介紹

針對智能CAD、機器人、計算機視覺、智能數控加工等機器智能中的重要需求，建立了幾何定理機器證明的消點法、微分差分系統機器證明基本方法、發展了幾何約束求解的系統高效算法，實質性開拓了數學機械化的適用範圍並得到重要應用。具體成果包括：

1.幾何自動作圖及其在智能CAD、機器視覺與機器人中的應用

提出了幾何自動作圖的C樹分解法與軌跡相交法，在多項式時間內計算出在等距變換下所有封閉解，將其餘問題分解爲極小模式，並給出求解多類極小模式的顯示公式與快速算法，完整地解決了幾何自動作圖問題。引進了最一般的空間並聯機構GSP平臺，發展了代數幾何方法求解其運動學正解，對於多種情形首次給出了顯示解，解決了具有優良運動學性質的並聯機器人構型基本問題。解決了視覺定位基本問題之一P3P解的完全分類公開問題,首次給出P3P問題的完整解析解，給出了數值求解的穩定性判定準則與完整與穩健的求解算法。

2.幾何定理機器證明的消點法

合作建立消點法，將幾何不變量引入自動推理，對構造型幾何命題發展了完整的消去理論，克服了“中間過程爆炸”難題，首次實現了自動生成可讀證明，使幾何定理機器證明進入到機器證明可以與傳統證明比美的新階段。消點法已被國外學者在主流自動推理平臺Coq、Isabelle/HOL，Theorema中實現並用於安全攸關係統驗證、力學系統機器證明等。

3.微分差分系統的消去理論與高效算法

結式、周形式與特徵列方法是數學機械化基本算法,由於存在根本困難，長期未能拓展到微分差分情形。本項目證明了Ritt於1950年提出的微分維數猜想“一般”正確，克服了定義微分周形式的障礙，首次給出微分周形式與微分稀疏結式的嚴格定義；建立了微分周形式與微分稀疏結式完整理論，引進了微分簇的“微分次數”新不變量，定義了微分簇的周座標新概念；給出了微分幾何機器證明的單指數算法。發現並證明了代數不可約的差分特徵列是非平凡的這一關鍵結果，突破了差分特徵列非平凡判定需要無窮次差分的難點，建立了差分特徵列算法並用於組合恆等式機器證明。

4.機器人與高端數控最優插補控制算法

針對在高端數控加工與機器人運動多種重要實用約束，包括jerk、jounce、加工誤差、動力學等確定與隨機約束，設計了多項式時間的時間最優5軸聯動數控機牀的運動插補控制算法，在國家重大科技專項“高檔數控機牀及基礎製造裝備”支持的商用數控系統中實現，加工效率提高了40%-150%，加工精度顯著改進，並應用於航空領域高速高精加工。

實驗室簡介

中國科學院數學機械化重點實驗室是國際計算機數學領域的科研、人才培養、學術交流的主要中心之一。

“數學機械化”是由實驗室的創始人吳文俊院士創立的一個研究方向。20世紀70年代，吳文俊提出藉助於計算機的強大計算進行自動推理將是信息時代數學發展的重要趨勢之一，也將爲腦力勞動機械化提供重要支撐。吳文俊建立了幾何定理機器證明的“吳方法”與方程求解的 “吳零點分解定理”，成爲數學機械化的奠基性成果。吳文俊因此獲得國際自動推理最高獎“Herbrand自動推理成就獎”、首屆國家最高科技獎、有“東方諾貝爾獎”之稱的邵逸夫數學獎，被國家授予首屆“人民科學家”榮譽稱號。

實驗室的中青年科研人員也取得了一系列高水平的科研成果，並獲得了十數項國內重要獎勵與多項國際獎勵，包括國家自然科學二等獎三項，國家技術發明二等獎，ACM/SIGSAM ISSAC傑出論文獎三項等。實驗室是我國數學機械化研究的主要組織者。主持國家“973”項目三項，國家基金委優秀創新羣體項目等。

數學機械化實驗室在幾何自動推理、特徵列方法、計算微分差分代數幾何、智能數控插補等方面在國際上有明顯優勢。特別是在幾何自動推理方面，國際學術界公認實驗室做出了開創性成果。數學機械化實驗室也是國際符號計算方面的主要中心之一。舉例說明，符號計算最權威的國際會議是ACM/SIGSAM ISSAC，已經舉辦了48屆。實驗室成員曾經當選爲ACM/SIGSAM副主席、ISSAC大會主席（3位）、ISSAC指導委員會主席（3位）、ISSAC程序委員會主席，作ISSAC邀請報告（3次）。國際著名學者M. Singer指出實驗室“是國際上符號計算最強的研究羣體之一，產生領軍人物、有基礎意義的研究成果和軟件，對整個科學界有很強的影響力”。

獲獎感言

十分榮幸獲得吳文俊人工智能傑出貢獻獎，衷心感謝中國人工智能學會的肯定與鼓勵，感謝各位同行的支持。我在吳文俊先生身邊工作了30多年，深知他對數學機械化有很高的期望。他希望：“通過數學的機械化，推動腦力勞動機械化”；他展望到：“槍炮使人們在體力上難分強弱，通過腦力勞動機械化，計算機將使人們在智力上難分聰明愚魯。”我的工作只是吳文俊先生這些宏大設想的一小步。讓我們真誠祝願他的希望儘快成真，祝願我國人工智能事業蓬勃發展。

相關文章