让AI像数学家一样严谨构造几何辅助线并验证证明。
Geoint-R1: Formalizing Multimodal Geometric Reasoning with Dynamic Auxiliary Constructions
- 用Lean4形式化逻辑构建几何辅助元素，确保推理可验证。
- 在1885道几何题上超越现有模型，尤其擅长复杂构造题。
- 适合研究形式化数学推理或AI几何教育的学者与开发者。
几何推理对科学发现和教育发展至关重要，需精确逻辑与严格形式验证。尽管多模态大模型在推理任务上取得进展，但现有模型在动态构造与验证几何辅助元素方面仍存在困难。为此，我们提出Geoint-R1，一种从文本描述和视觉图中生成可形式化验证几何解的多模态推理框架。该框架融合辅助元素构建、基于Lean4的形式化推理与交互式可视化。为系统评估并推动形式化几何推理发展，我们构建了包含1,885个严谨标注几何题的Geoint基准，覆盖平面、空间与立体几何，每道题含结构化文本注释、精确的Lean4辅助构造代码及专家验证的解题步骤。大量实验表明，Geoint-R1显著优于现有多模态与数学专用推理模型，尤其在需明确构造辅助元素的难题上表现突出。
原文摘要 · Abstract (English)
Mathematical geometric reasoning is essential for scientific discovery and educational development, requiring precise logic and rigorous formal verification. While recent advances in Multimodal Large Language Models (MLLMs) have improved reasoning tasks, existing models typically struggle with formal geometric reasoning, particularly when dynamically constructing and verifying auxiliary geometric elements. To address these challenges, we introduce Geoint-R1, a multimodal reasoning framework designed to generate formally verifiable geometric solutions from textual descriptions and visual diagrams. Geoint-R1 uniquely integrates auxiliary elements construction, formal reasoning represented via Lean4, and interactive visualization. To systematically evaluate and advance formal geometric reasoning, we propose the Geoint benchmark, comprising 1,885 rigorously annotated geometry problems across diverse topics such as plane, spatial, and solid geometry. Each problem includes structured textual annotations, precise Lean4 code for auxiliary constructions, and detailed solution steps verified by experts. Extensive experiments demonstrate that Geoint-R1 significantly surpasses existing multimodal and math-specific reasoning models, particularly on challenging problems requiring explicit auxiliary element constructions.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。