高老師介紹“笛卡爾構想（1596-1650）”所蘊含的機器自動證明定理是人類一個(ge) 古老的夢想，萊布尼茨的“通用符號演算”（1646-1716）是自動推理的目標，“希爾伯特形式主義(yi) 與(yu) 判定問題”在數學上真正將自動推理提成了一個(ge) 嚴(yan) 格的數學問題，至少在理論上完整解決(jue) 了自動推理，並指出了自動推理在有效性追求方麵產(chan) 生的幾個(ge) 重大影響：（1）邏輯人工智能開啟了符號主義(yi) 人工智能；（2）計算理論：自動推理的計算複雜性，它開辟了計算複雜性理論領域；（3）交互式定理證明與(yu) 形式化數學：不必自動證明定理，而是自動驗證給定的證明是否正確；（4）數學機械化（吳文俊，1979）：在數學的各個(ge) 學科選擇適當的範圍，即不太小以至於(yu) 失去意義(yi) 、又不能太大以至於(yu) 不可判斷，實現機械化，推動數學發展與(yu) 腦力勞動機械化。高老師強調自動推理是人工智能的重要起源，邏輯人工智能產(chan) 生了一係列重要人工智能發現且在各行各業(ye) 都能發揮重大作用。

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

機器學習(xi) 組件已廣泛應用於(yu) 安全攸關(guan) 的信息物理融合係統，而對於(yu) 如何保障其安全性？高老師首先解釋：驗證係統的正確性就是證明一個(ge) 定理，因此智能係統正確性驗證的核心是自動推理。接著高老師闡述了基於(yu) 嚴(yan) 格數學基礎對係統進行規約、開發和驗證的技術是自動推理正確性驗證的形式化方法，自動推理在軟硬件驗證技術及芯片與(yu) 基礎軟件的應用是自動推理正確性驗證的成功案例。最後他講解了對抗樣本存在下的學習(xi) （對抗學習(xi) ）、如何用幾何變換產(chan) 生對抗樣本及對抗深度學習(xi) 的數學理論。

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

報告結束後，周愛輝研究員主持了提問環節。嘉賓們(men) 分別代表網友提出了三個(ge) 問題，分別是：基於(yu) 符號的邏輯推理與(yu) 基於(yu) 統計的機器學習(xi) 結合的前景如何？關(guan) 鍵難度在哪？目前人工智能在各個(ge) 領域都有應用，但普遍的問題是缺少理論的保證，因此在一些涉及安全或者機械製造等關(guan) 鍵領域很難得到真正的應用。那如何使得人工智能的方法安全可靠有哪些可行的思路？基於(yu) 邏輯和數學機械化的人工智能是否可以和目前基於(yu) 學習(xi) 的人工智能結合，來保證設計算法的安全可靠？ ChatGPT在幾何定理自動證明，或者說數學定理的自動證明的有什麽(me) 進展嗎？ChatGPT在這方麵，將來的發展潛力如何？這三個(ge) 問題是通過米兰体育官方网站入口微信公眾(zhong) 號收集遴選的。高小山研究員對這些問題做了詳細地回答。