高老師介紹“笛卡爾構(gòu)想（1596-1650）”所蘊(yùn)含的機(jī)器自動證明定理是人類一個古老的夢想，萊布尼茨的“通用符號演算”（1646-1716）是自動推理的目標(biāo)，“希爾伯特形式主義與判定問題”在數(shù)學(xué)上真正將自動推理提成了一個嚴(yán)格的數(shù)學(xué)問題，至少在理論上完整解決了自動推理，并指出了自動推理在有效性追求方面產(chǎn)生的幾個重大影響：（1）邏輯人工智能開啟了符號主義人工智能；（2）計算理論：自動推理的計算復(fù)雜性，它開辟了計算復(fù)雜性理論領(lǐng)域；（3）交互式定理證明與形式化數(shù)學(xué)：不必自動證明定理，而是自動驗證給定的證明是否正確；（4）數(shù)學(xué)機(jī)械化（吳文俊，1979）：在數(shù)學(xué)的各個學(xué)科選擇適當(dāng)?shù)姆秶床惶∫灾劣谑ヒ饬x、又不能太大以至于不可判斷，實現(xiàn)機(jī)械化，推動數(shù)學(xué)發(fā)展與腦力勞動機(jī)械化。高老師強(qiáng)調(diào)自動推理是人工智能的重要起源，邏輯人工智能產(chǎn)生了一系列重要人工智能發(fā)現(xiàn)且在各行各業(yè)都能發(fā)揮重大作用。

對于深度學(xué)習(xí)與自動推理融合，高老師闡述到深度學(xué)習(xí)是新一輪人工智能突破的基礎(chǔ)，基于深度學(xué)習(xí)的突破包括：模式識別(在很多方面超越人類)、AlphaGo（在各種棋類戰(zhàn)勝人類）、AlphaFold（預(yù)測蛋白質(zhì)結(jié)構(gòu)）、ChatGPT（部分通用智能）等；并分享了邏輯推理與機(jī)器學(xué)習(xí)、深度推理是深度學(xué)習(xí)與自動推理的融合，又結(jié)合紐結(jié)理論、矩陣乘法、ChatGPT求解數(shù)學(xué)問題、神經(jīng)-符號自動推理DNN、視覺推理等具體問題來說明深度學(xué)習(xí)如何增強(qiáng)自動推理及如何用DNN實現(xiàn)自動推理過程和直接學(xué)習(xí)視覺推理任務(wù)。雖然深度學(xué)習(xí)與自動推理融合被認(rèn)為是下一代AI的方向之一，但目前還遠(yuǎn)未達(dá)到自動推理“涌現(xiàn)”的目標(biāo)，高老師強(qiáng)調(diào)其面臨的主要挑戰(zhàn)為（1）基于DNN的邏輯推理：ChatGPT是否通過學(xué)習(xí)數(shù)學(xué)書籍并融合邏輯推理可以達(dá)到自動推理過程的“涌現(xiàn)”？（2）使用邏輯提升DNN性能：找到適合于深度推理的有效表示，就像用于圖像識別的CNN、用于自然語言翻譯的Transformer。

機(jī)器學(xué)習(xí)組件已廣泛應(yīng)用于安全攸關(guān)的信息物理融合系統(tǒng)，而對于如何保障其安全性？高老師首先解釋：驗證系統(tǒng)的正確性就是證明一個定理，因此智能系統(tǒng)正確性驗證的核心是自動推理。接著高老師闡述了基于嚴(yán)格數(shù)學(xué)基礎(chǔ)對系統(tǒng)進(jìn)行規(guī)約、開發(fā)和驗證的技術(shù)是自動推理正確性驗證的形式化方法，自動推理在軟硬件驗證技術(shù)及芯片與基礎(chǔ)軟件的應(yīng)用是自動推理正確性驗證的成功案例。最后他講解了對抗樣本存在下的學(xué)習(xí)（對抗學(xué)習(xí)）、如何用幾何變換產(chǎn)生對抗樣本及對抗深度學(xué)習(xí)的數(shù)學(xué)理論。

高老師最后總結(jié)：（1）自動推理是邏輯主義人工智能的源泉，由此產(chǎn)生了計算理論等重要學(xué)科方向，以及SAT求解器、Coq定理證明器、Maple符號計算等重要軟件工具；（2）融合深度學(xué)習(xí)與自動推理是未來人工智能發(fā)展的主要方向之一，現(xiàn)在還處在初始階段，有待深入研究；（3）安全驗證是自動推理的主要成功應(yīng)用場景之一，智能系統(tǒng)安全具有更大的挑戰(zhàn)性，需要迫切解決。

報告結(jié)束后，周愛輝研究員主持了提問環(huán)節(jié)。嘉賓們分別代表網(wǎng)友提出了三個問題，分別是：基于符號的邏輯推理與基于統(tǒng)計的機(jī)器學(xué)習(xí)結(jié)合的前景如何？關(guān)鍵難度在哪？目前人工智能在各個領(lǐng)域都有應(yīng)用，但普遍的問題是缺少理論的保證，因此在一些涉及安全或者機(jī)械制造等關(guān)鍵領(lǐng)域很難得到真正的應(yīng)用。那如何使得人工智能的方法安全可靠有哪些可行的思路？基于邏輯和數(shù)學(xué)機(jī)械化的人工智能是否可以和目前基于學(xué)習(xí)的人工智能結(jié)合，來保證設(shè)計算法的安全可靠？ ChatGPT在幾何定理自動證明，或者說數(shù)學(xué)定理的自動證明的有什么進(jìn)展嗎？ChatGPT在這方面，將來的發(fā)展?jié)摿θ绾?？這三個問題是通過中國數(shù)學(xué)會微信公眾號收集遴選的。高小山研究員對這些問題做了詳細(xì)地回答。