近期，NeurIPS 2026录用结果公布，上海大学计算机工程与科学学院冷拓教授课题组的研究成果“Agentic Geometry Problem Solving via Human-like Parallel Bidirectional Reasoning”被该会议主赛道（Main Track）接收，计算机工程与科学学院2024级博士研究生张效凯为论文第一作者，冷拓教授为唯一通讯作者。NeurIPS 是神经信息处理系统大会（Conference on Neural Information Processing Systems）的简称，是人工智能与机器学习领域最具影响力的国际顶级会议之一，也是中国计算机学会（CCF）A类会议，在世界范围内每年召开一次。今年，NeurIPS主赛道共收到30709篇有效论文投稿，最终接收了7900篇，录用率25.7%。
此次被录用的论文是冷拓教授课题组在几何问题自动求解方向系列研究中的第11篇成果，该工作构建了名为RAVS（Reflect Agent Verified Solve）的神经符号统一推理框架，其核心思想是“让大模型做擅长的高层规划，让符号系统做擅长的严格验证”：大语言模型作为规划者，负责理解题意、反思已探索路径并决定下一步策略；基于FormalGeo的形式化符号求解器作为执行者，负责定理应用、代数计算和逐步验证，二者通过“推理—执行—反思—记忆”闭环协同，从架构上避免大模型直接生成证明时常见的幻觉和逻辑跳步。同时，该工作还构建了首个完全统一前向推理与后向推理的双向符号推理引擎，对每个定理定义“前向应用”和“后向分解”两种可逆操作，使系统既能从已知条件正向推导，也能从目标反向拆解子目标，并在两个搜索方向相遇时完成证明。理论分析表明双向推理相较单向推理具有指数级复杂度优势；实验方面，RAVS 在FormalGeo7K基准上达到96.06%的求解准确率，在Geometry3K和GeoQA上分别达到98.11%和94.64%，均优于现有最优方法，且无需针对具体问题额外标注数据。该成果是FormalGeo形式化几何推理体系的重要升级，为高可靠、可验证的几何问题自动求解提供了“大模型规划+符号验证+双向推理”的新范式。
图1 RAVS整体架构
冷拓教授课题组在几何问题形式化表示与自动求解领域开展了系统性研究，通过融合数学机械化方法与深度学习技术，逐步构建了具有创新性的几何问题自动求解框架——FormalGeo。该框架涵盖几何形式化理论、几何形式化系统、推理计算引擎、几何问题解析器、几何问题求解器、几何问题数据集及评价指标，形成了完整的生态体系。经过近6年的积累，课题组研究成果已逐渐获得学界广泛认可，团队多次受邀在北京大学、复旦大学等知名高校，以及中国数学年会计算机数学大会、国际人工智能联合会等重要学术会议上作邀请报告。课题组提出的几何形式化系统作为基础框架，已有效支撑了多项衍生研究：北京大学团队以FormalGeo的形式化几何理论为基础，提出统一几何专家模型GeoUni，将几何问题求解、图形生成与问题生成整合到单一框架中；中国科学技术大学团队借助FormalGeo的符号系统，提出GeoGen框架，通过符号-神经集成增强多模态大语言模型的几何推理能力；此外，还有业界团队如腾讯混元、微软研究院AI Frontiers也基于该框架开展了相关研究。上述成果分别发表在ACM MM、CVPR、ICML等国际顶级会议上。
图2 FormalGeo研究内容逻辑关系图
2026年4月，FormalGeo迎来重大版本更新，表达能力更强、更具扩展性的FormalGeo-Beta版本正式发布。相较于先前版本，FormalGeo-Beta在形式化建模、系统扩展性、构图机制和推理能力等方面实现全面升级，进一步推动了几何形式化与自动推理的深度融合：1.形与数统一：几何关系与代数关系深度融合。每个关系同时具有几何形式和代数形式：几何形式用于快速推理与解题构建，代数形式用于实体构建、合法性检查、退化条件检查和隐含关系发现，使符号推理与数值计算在同一系统中统一，避免了推理与计算割裂。2.可扩展的形式化系统：自定义关系、测度与定理。用户可通过几何定义语言以JSON格式快速自定义关系、测度和定理，并可嵌入Python自定义运算，系统内置点、线、圆三类实体及多种代数关系与运算，具备很强的扩展性和领域适应能力。3.线性与非线性构图统一：实体构建语句自动解析为方程组求解。系统使用实体构建语句逐步构建点、线和圆，自动将几何约束解析为析取范式并转化为代数方程组求解；单实体构造为线性构图，多实体构造为非线性构图，二者实现统一，使复杂构型搭建更加灵活。4.前向与后向推理结合：几何谓词逻辑推理与结构化超图解题过程。系统以几何谓词逻辑表达式为推理核心，支持前向推理与后向推理，以及带参和无参两种定理调用方式；求解过程被建模为以条件为超结点、定理为超边的超图，并配有两种合法性检查，使解题过程透明、可控、可解释。
图3 FormalGeo-beta版本问题求解流程
新版本为构建模拟及超越人类的几何智能解题系统提供了可能。团队以新形式化系统为基础，构建了一整套无需人类参与的几何知识自动发现系统——EuclidMachine。其核心能力包括：基于约束的自动构图（可在构图过程中自动做辅助线）、基于符号推理的自动解题，以及基于结构挖掘的知识自动归纳机制（自动知识发现、直观几何与自动公理体系构建）。该系统致力于构建一个自主学习且可解释的几何定理自动证明与几何知识自动发现系统，亦即一个无需人类提供监督信息的神经-符号自动公理化系统，能够自动生成和求解难度达到甚至超越国际奥林匹克竞赛水平的几何问题，并给出人类可读的解题过程。
EuclidMachine不仅支持全自动求解，还支持交互式证明。系统能够将解题过程拆解为一系列可理解、可干预、可追溯的推理步骤，用户可以在关键节点进行提问、调整思路或补充条件，系统则实时反馈推理结果与证明状态，形成人机协同的证明环境。这一能力使其在教育场景中具有广阔的应用前景：学生可以借助交互式证明逐步理解几何定理的推导逻辑，教师可以将其作为动态教学工具，直观展示辅助线构造、定理应用与证明路径选择，从而将抽象的几何推理转化为可操作、可观察、可反思的学习过程。
图4 EuclidMachine教学软件交互式求解示例
目前，形式化推理引擎已经构建和测试完成，IMO基准构建和实验正在稳步推进中。未来，随着EuclidMachine的持续演进，一个能够自主学习、自动发现、可解释证明并支持人机协同的几何智能系统正加速走来，有望在数学智能、自动推理与智能教育领域开启全新的可能性。
