近期，，，人工智能领域国际学术聚会IJCAI 2025（中国盘算机学会CCF A类聚会）宣布审稿效果，，，j9九游会盘算机工程与科学学院冷拓副教授课题组的研究效果“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/