近日，我院系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室徐揚教授團隊在一階邏輯自動定理證明器領(lǐng)域取得突破性進展。所研發(fā)的一階邏輯自動定理證明器CSI_V，采用該團隊原創(chuàng)的逆向并行邏輯演繹的科學方案，融合此前國際領(lǐng)先的證明器Vampire，針對該領(lǐng)域最頂級賽事——國際自動定理證明競賽（International Conference on Automated Deduction —— Automated Theorem Proving System Competition）近五年共2500個競賽問題，在標準實驗條件下進行了對比實驗，共證明出2446個定理，超過此前國際領(lǐng)先的證明器Vampire 180個定理（詳見下表。事實上，每多證明1個定理都是極其困難的?。b遙領(lǐng)先于此前國際領(lǐng)先的證明器Vampire，居國際領(lǐng)先！國際自動定理證明器競賽的主席、美國邁阿密大學Geoff Sutcliffe教授對徐揚教授團隊最新研發(fā)的證明器給予了極高的評價。

基于邏輯的自動定理證明器是人工智能領(lǐng)域最基礎(chǔ)、最核心、最科學的研究方向之一，涉及數(shù)學、邏輯學、計算機科學與技術(shù)等領(lǐng)域?；谶壿嫷淖詣佣ɡ碜C明器屬基礎(chǔ)性工具，具有十分重要的科學與應(yīng)用價值，廣泛應(yīng)用于自然科學、技術(shù)科學、社會科學等領(lǐng)域，特別是數(shù)學定理的證明與發(fā)現(xiàn)?；谶壿嫷淖詣佣ɡ碜C明器研發(fā)同時也是一個極其困難的問題，需要讓計算機從浩如煙海的條件中找到成功的證明路徑，經(jīng)常被比喻為“大海撈針”。

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

實驗結(jié)果對比表：