高老师介绍“笛卡尔构想（1596-1650）”所蕴含的机器自动证明定理是人类一个古老的梦想，莱布尼茨的“通用符号演算”（1646-1716）是自动推理的目标，“希尔伯特形式主义与判定问题”在数学上真正将自动推理提成了一个严格的数学问题，至少在理论上完整解决了自动推理，并指出了自动推理在有效性追求方面产生的几个重大影响：（1）逻辑人工智能开启了符号主义人工智能；（2）计算理论：自动推理的计算复杂性，它开辟了计算复杂性理论领域；（3）交互式定理证明与形式化数学：不必自动证明定理，而是自动验证给定的证明是否正确；（4）数学机械化（吴文俊，1979）：在数学的各个学科选择适当的范围，即不太小以至于失去意义、又不能太大以至于不可判断，实现机械化，推动数学发展与脑力劳动机械化。高老师强调自动推理是人工智能的重要起源，逻辑人工智能产生了一系列重要人工智能发现且在各行各业都能发挥重大作用。

对于深度学习与自动推理融合，高老师阐述到深度学习是新一轮人工智能突破的基础，基于深度学习的突破包括：模式识别(在很多方面超越人类)、AlphaGo（在各种棋类战胜人类）、AlphaFold（预测蛋白质结构）、ChatGPT（部分通用智能）等；并分享了逻辑推理与机器学习、深度推理是深度学习与自动推理的融合，又结合纽结理论、矩阵乘法、ChatGPT求解数学问题、神经-符号自动推理DNN、视觉推理等具体问题来说明深度学习如何增强自动推理及如何用DNN实现自动推理过程和直接学习视觉推理任务。虽然深度学习与自动推理融合被认为是下一代AI的方向之一，但目前还远未达到自动推理“涌现”的目标，高老师强调其面临的主要挑战为（1）基于DNN的逻辑推理：ChatGPT是否通过学习数学书籍并融合逻辑推理可以达到自动推理过程的“涌现”？（2）使用逻辑提升DNN性能：找到适合于深度推理的有效表示，就像用于图像识别的CNN、用于自然语言翻译的Transformer。

机器学习组件已广泛应用于安全攸关的信息物理融合系统，而对于如何保障其安全性？高老师首先解释：验证系统的正确性就是证明一个定理，因此智能系统正确性验证的核心是自动推理。接着高老师阐述了基于严格数学基础对系统进行规约、开发和验证的技术是自动推理正确性验证的形式化方法，自动推理在软硬件验证技术及芯片与基础软件的应用是自动推理正确性验证的成功案例。最后他讲解了对抗样本存在下的学习（对抗学习）、如何用几何变换产生对抗样本及对抗深度学习的数学理论。

高老师最后总结：（1）自动推理是逻辑主义人工智能的源泉，由此产生了计算理论等重要学科方向，以及SAT求解器、Coq定理证明器、Maple符号计算等重要软件工具；（2）融合深度学习与自动推理是未来人工智能发展的主要方向之一，现在还处在初始阶段，有待深入研究；（3）安全验证是自动推理的主要成功应用场景之一，智能系统安全具有更大的挑战性，需要迫切解决。

报告结束后，周爱辉研究员主持了提问环节。嘉宾们分别代表网友提出了三个问题，分别是：基于符号的逻辑推理与基于统计的机器学习结合的前景如何？关键难度在哪？目前人工智能在各个领域都有应用，但普遍的问题是缺少理论的保证，因此在一些涉及安全或者机械制造等关键领域很难得到真正的应用。那如何使得人工智能的方法安全可靠有哪些可行的思路？基于逻辑和数学机械化的人工智能是否可以和目前基于学习的人工智能结合，来保证设计算法的安全可靠？ ChatGPT在几何定理自动证明，或者说数学定理的自动证明的有什么进展吗？ChatGPT在这方面，将来的发展潜力如何？这三个问题是通过中国数学会微信公众号收集遴选的。高小山研究员对这些问题做了详细地回答。