近期，人工智能领域国际学术会议IJCAI 2025（中国计算机学会CCF A类会议）公布审稿结果，沙巴博彩公司,沙巴体育在线计算机工程与科学学院冷拓副教授课题组的研究成果“FGeo-HyperGNet: Geometric Problem Solving Integrating FormalGeo Symbolic System and Hypergraph Neural Network”被该会议接收录用，计算机工程与科学学院2024级博士研究生张效凯为论文第一作者，冷拓副教授为唯一通讯作者。IJCAI全称为国际人工智能联合会议（International Joint Conference on Artificial Intelligence），该会议是国际人工智能界最有影响力和权威性的盛会之一，在世界范围内每年召开一次，本届会议录用率约为19%。
几何学是一门历史悠久、历久弥新的学科，自欧几里得《几何原本》问世以来，其理论体系不断完善，而沙巴博彩公司,沙巴体育在线几何问题自动求解方法的探索始终与之相伴相生。特别是计算机出现以后，人们尝试利用其强大的计算和推理能力设计自动解题算法，在这一背景下诞生了数学机械化这一数学新分支。将数学知识转化成计算机能够理解的语言，显然易见是数学与计算机科学融合的第一步，也是必不可少的重要一步。几何问题包含图像、文本和数学符号等多种知识形式，解题过程涉及几何关系推理、数值计算、代数方程求解、图像推理和逻辑运算，难以纳入统一框架处理，使得几何问题形式化与自动求解成为一项长期的挑战。
冷拓副教授课题组在几何问题形式化表示与自动求解领域开展了系统性研究，通过整合数学机械化方法与深度学习技术，逐步构建了一个具有创新性的几何问题自动求解框架——FormalGeo，如图1所示。FormalGeo几何问题自动求解框架可划分为四个主要组成部分：几何形式化理论（图中红色部分）、几何形式系统（图中黄色部分）、几何问题求解器（图中蓝色部分）以及几何问题的自动形式化与逆形式化（图中绿色部分）。
图1 FormalGeo几何问题自动求解框架
此次被IJCAI 2025录用的工作是冷拓副教授课题组在几何问题自动求解系列的第7篇论文。该工作构建了一个名为FGeo-HyperGNet的神经-符号系统，用于实现类人的几何问题自动求解，整体架构如图2所示。该系统的符号部分是基于FormalGeo构建的形式化系统，能够自动执行几何关系推理与代数运算，并将解题过程组织为以已知条件为超结点、几何定理为超边的超图结构。该系统的神经部分HyperGNet是一种基于注意力机制的超图神经网络，其组成包括用于有效编码超图结构与语义信息的编码器，以及为解题过程提供指导的定理预测器。该系统通过神经部分预测解题所需的定理，符号部分应用定理并更新超图，形成“预测-应用”的迭代求解机制，最终实现可读、可回溯、可解释的几何问题自动求解。
图2 用于自动求解几何问题的神经符号系统整体架构
作者在三个几何问题求解数据集FormalGeo7K、Geometry3K和GeoQA对提出的方法进行测试，均创造了新的几何问题求解成功率记录（SOTA），分别为88.36%、85.64%和91.99%。相比于该领域现有SOTA方法，FGeo-HyperGNet在三个数据集上的提升分别为5.98%、20.44%和1.59%。特别是在求解高难度几何问题时，FGeo-HyperGNet显著优于现有SOTA方法。
图3 研究内容逻辑关系图
经过近5年的积累，冷拓副教授课题组在几何自动推理领域的研究成果已逐渐获得学界广泛认可，前期多项成果已经以论文形式发表，各部分研究内容的逻辑关系如图3所示。
团队多次受邀在北京大学、复旦大学、北京航空航天大学等知名高校，以及中国数学年会计算机数学前沿论坛等重要学术会议上作邀请报告。课题组提出的FormalGeo形式化系统作为基础性理论框架，已有效支撑了多项衍生研究：北京大学团队基于FormalGeo提出了一种名为DFE-GPS的新框架，通过三阶段训练增强模型对几何图形的理解与推理能力，提升多模态大语言模型在几何问题求解中的表现。中国科学技术大学团队提出了GeoGen方法，该方法基于FormalGeo自动生成几何问题的多步推理路径，确保逻辑正确性，进而训练专用的大语言模型，将多模态大语言模型的自然语言推理步骤转换为符号系统的形式化表示，便于符号验证。通过这种符号-神经集成增强多模态大语言模型求解几何问题的能力。
近年来，计算机学院研究生人才培养工作正逐渐深入专业领域前沿，一些高质量科研成果正在不断产出。这些成果将为计算机学院学科建设、研究生培养起到重要的支撑作用。
FormalGeo主页：https://formalgeo.github.io/
