用形式化语言解决立体几何难题,推理过程可验证且通用。
Hilbert-Geo: Solving Solid Geometric Problems by Neural-Symbolic Reasoning

- 构建首个统一的立体几何形式化语言框架,支持符号推理。
- 在两个数据集上达77.3%和84.1%准确率,显著超越大模型。
- 方法兼具可读性与严谨性,适用于平面与立体几何。
几何问题求解作为典型的多模态推理任务,近年来取得显著进展,但多数工作聚焦于平面几何,对立体几何因三维空间图示和复杂推理而表现不佳。为此,本文提出Hilbert-Geo,首个面向立体几何的统一形式语言框架,包含丰富的谓词库和专用定理库。基于此,提出Parse2Reason方法,分两步:先利用条件描述语言(CDL)将自然语言问题与视觉图示转化为形式化表达;再结合定理库进行关系推理与代数计算,生成严格正确、可验证且人类可读的推理链。该框架亦适用于平面几何。为推动研究,我们构建了专家标注的数据集SolidFGeo2k和PlaneFGeo3k,均含形式化语言标注、解题过程与答案。大量实验表明,该方法在SolidFGeo2k上达到77.3%准确率,在MathVerse-Solid子集上达84.1%,显著优于Gemini-2.5-pro(54.2%)与GPT-5(62.9%)。在PlaneFGeo3k上达80.2%准确率,证明其通用性。代码与数据已开源。
原文摘要 · Abstract (English)
Geometric problem solving, as a typical multimodal reasoning problem, has attracted much attention and made great progress recently, however most of works focus on plane geometry while usually fail in solid geometry due to 3D spatial diagrams and complex reasoning. To bridge this gap, we introduce Hilbert-Geo, the first unified formal language framework for solid geometry, including an extensive predicate library and a dedicated theorem bank. Based on this framework, we propose a Parse2Reason method containing two steps of first parsing then reasoning. In the parsing step, we utilize conditional description language (CDL), a formalized language composed of predicates specifically designed to construct geometric conditions, to represent both problem description (natural text) and solid diagrams (visual image). In the reasoning step, we leverage those formal CDL and the theorem bank to perform relational inference and algebraic computation, generating strictly correct, verifiable, and human-readable reasoning processes. Notably, our proposed Hilbert-Geo is also applicable to plane geometry. To advance geometric reasoning, we curate two expert-annotated dataset SolidFGeo2k and PlaneFGeo3k, which are furnished with geometric formal language annotations, solutions and answers. Extensive experiments show that our proposed method achieves the state-of-the-art (SOTA) performance 77.3% in SolidFGeo2k and 84.1% in MathVerse-Solid (one small subset in MathVerse dedicated to solid geometry), substantially outperforming leading MLLMs, such as Gemini-2.5-pro (54.2% on SolidFGeo2k) and GPT-5 (62.9% on MathVerse-Solid). In addition, our method achieves the SOTA accuracy 80.2% in PlaneFGeo3k, demonstrating the generality of the Hilbert-Geo in geometric reasoning. Our code and datasets are released at https://github.com/PremiLab-Math/Hilbert-Geo.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。