近期，人为智能领域国际学术会议IJCAI 2025（中国推算机学会CCF A类会议）颁布审稿了局，亿万先生MR推算机工程与科学学院冷拓副教授课题组的钻研成就“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所示。

团队屡次受邀在北京大学、复旦大学、北京航空航天大学等驰名高校，以及中国数学年会推算机数学前沿论坛等沉要学术会议上作约请汇报？翁庾樘岢龅腇ormalGeo大局化系统作为基础性理论框架，已有效支持了多项衍生钻研：北京大学团队基于FormalGeo提出了一种名为DFE-GPS的新框架，通过三阶段训练加强模型对几何图形的理解与推理能力，提升多模态大说话模型在几何问题求解中的阐发。中国科学技术大学团队提出了GeoGen步骤，该步骤基于FormalGeo自动天生几何问题的多步推理蹊径，确保逻辑正确性，进而训练专用的大说话模型，将多模态大说话模型的天然说话推理步骤转换为符号系统的大局化暗示，便于符号验证。通过这种符号-神经集成加强多模态大说话模型求解几何问题的能力。

近年来，推算机学院钻研生人才造就工作正逐步深刻专业领域前沿，一些高质量科研成就在不休产出。这些成就将为推算机学院学科建设、钻研生造就起到沉要的支持作用。

FormalGeo主页：https://formalgeo.github.io/