Geoint-R1：以动态辅助构造形式化多模态几何推理
Geoint-R1: Formalizing Multimodal Geometric Reasoning with Dynamic Auxiliary Constructions
把几何图形理解与形式化证明（Lean4）结合，并显式生成辅助构造元素，为视觉推理模型提供了可验证的中间步骤监督信号；其基准与标注方式可用于评测多模态模型在图形-文本联合推理上的严谨性。
原文依据 Geoint-R1 uniquely integrates auxiliary elements construction, formal reasoning represented via Lean4, and interactive visualization.
摘要译文
由模型翻译 · 术语统一 · 请对照原文核对关键结论数学几何推理对科学发现与教育发展至关重要，它要求精确的逻辑与严格的形式化验证。尽管多模态大语言模型（MLLMs）的最新进展提升了推理任务的表现，但现有模型通常在形式化几何推理上表现不佳，尤其是在动态构造并验证辅助几何元素时。为应对这些挑战，我们提出 Geoint-R1，一个多模态推理框架，旨在从文本描述与视觉图形中生成可形式化验证的几何解答。Geoint-R1 独特地整合了辅助元素构造、以 Lean4 表示的形式化推理以及交互式可视化。为系统性地评测并推进形式化几何推理，我们提出 Geoint 基准，包含 1,885 道经过严格标注的几何问题，覆盖平面几何、空间几何与立体几何等多样主题。每道题均包含结构化文本标注、用于辅助构造的精确 Lean4 代码，以及经专家验证的详细解题步骤。大量实验表明，Geoint-R1 显著超越现有多模态与数学专用推理模型，在需要显式构造辅助元素的难题上尤为突出。
英文原文摘要 1328 字符
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.