组合几何的数学机械化方法与模型的可解释性

报告题目：组合几何的数学机械化方法与模型的可解释性

报告人：冷拓 副教授 上海大学

主持人：沈超敏 副教授

报告时间：2020年11月13日（星期五）10:00 - 11:00

报告地点：中北校区理科大楼B504

报告摘要：

  数学中既有结构，也有计算。这种天然特性的两方面-亦是不可替代的两面-在悠久的历史场合中相互作用，促进了数学的成长。然而自现代计算机诞生以来，它也正以两种不同的方式对数学发生着影响。一方面，它作为数学的工具，使得数学中的计算比以往任何时候都要更具威力，直接影响着数学中的价值观念和方法的平衡；另一方面，它作为数学的载体，通过大量计算机的创新性应用，间接地改变着数学地内容与结构，从而给数学带来了前所未有的繁荣和发展。 

  在这种变革的背景下诞生了数学机械化这样一门数学的新分支，它关注实际可行性更甚于理论可行性。经过吴文俊先生、张景中先生等前辈的开拓，在求解某些问题类过程中的机械化算法构建，也早已成为计算机科学中的重要分支。另一方面，回到近些年兴起的机器学习热点，基于数据、统计与算力的深度学习模型在充分展示其能力的同时，却一直缺少推理和解释性方面的突破。随着图神经网络显示出的巨大潜力，可推理、可解释且无偏见的机器学习模型成为人工智能领域正在寻找的下一代智能范式。

  报告人与其建立的神经符号混合计算与机器证明小组则一直聚焦于用符号计算、数值计算与图神经网络结合的机械化算法求解离散几何中有代表性的几个公开问题及其反问题，如Thomson问题(n≥7)，Tammes问题，Erdos-Szekeres问题等；并致力于改进和推广层相关度传播、深度泰勒分解等算法，给出上述机器证明模型的可解释性。这些研究内容既是数学机械化的深化，也是下一代人工智能范式的延展，因此可视作是对符号学派和联结学派融合与交叉的一次探索。获得这些有难度的离散几何公开问题解答不仅本身有积极的数学意义，推进过程中可能产生的一些新的理论和方法也将是计算机科学领域正在引起重视的创新试验。

报告人简介：

  冷拓，上海大学计算机学院与人工智能研究院副教授。硕士就读于法国里尔科技大学，博士毕业于中国科学院。2018年初赴英国帝国理工学院短期访学，2018-2019年在美国斯坦福大学任长期访问学者。对数学机械化、深度学习与模型可解释性的研究取得了一系列成果，也在医疗图像分析、数据建模等应用领域做了一定的工作。近年来在各类相关国际学术会议邀请做大会或小组报告多次，如2014 MIA、 2019 MICCAI等。主持国家自然科学基金青年项目与面上项目各一项，主持上海市教委优秀青年教师资助项目一项，作为核心数学人员参与国家和省部级项目多项，曾担任上海市科委重点创新项目“大数据可视分析平台关键技术及典型应用”的学术组组长。部分成果转化为各类工业与经济应用，曾于2017 年获得上海市科技进步三等奖。在国际学术期刊和相关国际会议上发表论文20余篇，其中包括独立作者与第一作者的十余篇。