全国科技工作者日网络科普报告—自动推理与人工智能

美国人工智能前主席Winston教授指出：“人工智能就是研究如何使用计算机去做过去只有人才能做的智能工作”。推理（符号主义）、感知（联结主义）、协作（行为主义）是人最明显的三个智能工作，其中推理是人类最具代表性的智能行为之一，也是人工智能的核心与主要目标。自动推理主要研究定理的自动证明，它与人工智能的起源、成就与发展趋势相辅相成。

2023年5月30日是第七个“全国科技工作者日”。今年全国科技工作者日的主题是“点亮精神火炬”。在这个专属于科技工作者的日子里，中国数学会联合中国工业与应用数学学会、中国运筹学会特别邀请中国科学院数学与系统科学研究院高小山研究员，为广大科技工作者献上了精彩的网络科普报告“自动推理与人工智能”。中国数学会副理事长周爱辉研究员主持了报告，一起出席的还有中国工业与应用数学学会副理事长王兆军教授、中国运筹学会科普工作委员会主任刘歆研究员。

高老师的报告主要从三个方面展开：一、自动推理与逻辑主义人工智能；二、深度学习与自动推理融合；三、人工智能安全的数学理论。

自动推理与逻辑主义人工智能

高老师介绍“笛卡尔构想（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在这方面，将来的发展潜力如何？这三个问题是通过中国数学会微信公众号收集遴选的。高小山研究员对这些问题做了详细地回答。

简介报告专家

高小山，中科院数学与系统科学研究院研究员、国家数学与交叉科学中心执行主任。主要研究数学机械化、自动推理、人工智能数学理论及应用。曾获国家自然科学二等奖、吴文俊应用数学奖、吴文俊人工智能杰出贡献奖、国际计算机学会ISSAC杰出论文奖。曾担任3个973项目的首席科学家、国家基金委创新群体学术带头人、人工智能数学理论项目首席科学家。

文章来源：中国数学会