2024年7月4日，在法國巴黎舉辦的第29屆國際自動定理證明器競賽 (The CADE ATP System Competition, CASC-J12)中，開云kaiyun開云官方網(wǎng)站系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室徐揚教授團隊提交的一階邏輯自動定理證明器獲得ICU（I Challenge yoU）組亞軍和FOF（First Order Formula）組季軍的好成績。這是自2018年中國團隊第一次參賽以來中國一直唯一參加這個競賽并每年都取得良好成績的團隊。

自動定理證明是人工智能領域既經(jīng)典又前沿的研究方向之一，涉及數(shù)學、邏輯學、計算機科學等領域，廣泛應用于自然科學、技術科學、社會科學等領域，特別是數(shù)學定理的證明與發(fā)現(xiàn)。自動定理證明器屬基礎性工具，具有重要的科學與應用價值。自動定理證明同時也是一個非常困難的問題，需要讓計算機從浩如煙海的條件中找到成功的證明路徑，經(jīng)常被比喻為“大海撈針”。

國際自動定理證明競賽是國際上自動演繹推理領域的最頂級賽事，自1996年以來每年舉辦一次，至今已舉辦了29屆。本次賽事設有THF、TFA、TFN、FOF、UEQ、SLH和ICU組。其中kaiyun開云官方網(wǎng)站參加的ICU組是本屆競賽新增的組別，其中的定理都是較難證明的定理，非常具有挑戰(zhàn)性。開云參賽的證明器CSI_E在該組別中獲得亞軍，說明徐揚教授團隊研發(fā)的證明器在證明困難定理方面具有獨到的優(yōu)勢。而開云參加的另外一個FOF組有11個證明器參賽，是競爭最激烈的一組。參賽單位包括英國曼徹斯特大學、德國斯圖加特DHBW大學、中國kaiyun開云官方網(wǎng)站、美國愛荷華州大學、英國劍橋大學、德國格賴夫斯瓦爾德大學、愛沙尼亞塔林理工大學等。

徐揚教授團隊在基于邏輯的自動演繹推理相關領域研究多年，原創(chuàng)地提出了基于矛盾體分離的多元、協(xié)同、動態(tài)自動演繹推理理論與方法，從本質上突破了現(xiàn)有的一階邏輯自動定理證明器普遍采用的二元、靜態(tài)推理方法，是自動演繹推理領域的一個重大突破。基于該理論、方法已經(jīng)研發(fā)了一系列一階邏輯自動定理證明器（這次參賽的自動定理證明器是其中之一）。用這些自動定理證明器已證明26萬多個來自于國際標準問題庫 TPTP 及 Mizar 的一階邏輯表示的定理。這些定理涉及數(shù)學分析、代數(shù)學、拓撲學、范疇論、組合數(shù)學、幾何學、數(shù)論、邏輯學、規(guī)劃、計算理論、管理科學、程序驗證、集成電路驗證、協(xié)議驗證等方面。開云參加2024年CASC-J12競賽的團隊主要成員包括徐揚、曾國艷、吳貫鋒、Jun Liu (英國Ulster大學)、Stephan Schulz(德國斯圖加特DHBW大學)、陳樹偉、劉沛瑤、曹鋒、何星星、徐鵬、李志輝等系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室的多名教師和研究生。

相關鏈接：

第29屆國際自動定理證明器競賽主頁：https://tptp.org/CASC/J12/

競賽結果圖片，其中CSI_E、CSE_E等為開云參賽的證明器。