FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving
报告人：冷拓 (上海大学 )
时间：2024-05-15 15:00
地点：三教 407
报告摘要：
报告人与其建立的几何认知推理与机器证明小组近十年来一直致力于寻找符号学派与联结学派的结合点，运用符号计算、数值计算、图神经网络与大规模语言模型等技术手段向有难度的几何定理机器证明发起挑战，也可视作是对AI100 Report里提出的AI Open Grand Challenge中的IMO解题挑战的一种探索和正面回答。
在此报告中将展示我们构建的一个全新的、相容的平面几何形式化系统。这将是针对IMO级别的平面几何难题与可读式AI自动推理之间的一座重要桥梁，有了这个形式化系统，我们已经能够将一些现代的AI模型轻易接入，并实现接近人类的演绎式自动推理。在这套形式化体系下，AI已经能够像处理其他自然语言一样给出IMO级别的平面几何难题的演绎式推理解答，并且这种证明是可读可回溯可检验的。同时我们也构建了符合该形式化体系的高质量平面几何难题数据集FormalGeo7k与FormalGeo18k。
更进一步地，我们还开发了若干与现代AI技术结合的平面几何自动推理辅助工具与求解器，其中包括结合大语言模型的辅助定理序列预测器FGeo-TP, 基于超图理论的条件嵌入器FGeo-HyperGNet，基于强化学习的自动求解器FGeo-DRL。而将强化学习与蒙特卡洛树搜索等方法应用于平面几何的演绎式自动求解与证明，尚是领域内的首次尝试。
在上述研究过程中，我们亦逐渐实现和发展了一些全新的技术环节，得到了某种程度上出人意料的成果。这些研究内容既是数学机械化的深化，也是下一代人工智能范式的延展，因此可视作是对符号学派和联结学派融合与交叉的一次积极尝试。实现有难度的几何问题机器证明不仅本身有积极的数学意义，推进过程中可能产生的一些新的理论和方法也是计算机科学领域正在引起重视的创新试验。
报告人简介：
冷拓，上海大学计算机公司与人工智能研究院双聘副教授。斯坦福大学与帝国理工公司访问学者，现任上海大学WSTNet 国际联合实验室副主任。主持国家自然科学基金数学天元基金、面上项目、青年项目，主持上海市教委优秀青年教师资助项目，作为核心数学人员参与国家和省部级项目多项。2017 年获得上海市科技进步三等奖。在国际学术刊物和学术会议上以第一作者或独立作者发表论文30余篇，包括医学图像分析领域的国际顶级会议MICCAI和国际著名数学期刊PAMS, LAA, JMAA等。近年来在各类相关国际学术会议做大会或小组报告多次，如2014 MIA, 2019 MICCAI等。
