Source-linked AI summary
Geoint-R1: Formalizing Multimodal Geometric Reasoning with Dynamic Auxiliary Constructions
Jingxuan Wei, Caijun Jia, Qi Chen, Honghao He, Linzhuang Sun, Conghui He, Lijun Wu, Bihui Yu, Cheng Tan
TL;DR
Existing multimodal models struggle with formal geometric reasoning, especially dynamic auxiliary construction and verification. Geoint-R1 combines supervised fine-tuning, verification-guided reinforcement learning, and curriculum learning, alongside the 1,885-problem Geoint benchmark. Experiments report superior performance over existing state-of-the-art multimodal and mathematical reasoning models, especially on tasks requiring explicit auxiliary constructions.
Problem
Existing multimodal approaches lack rigorous geometric reasoning and struggle to dynamically construct and verify auxiliary elements in complex multimodal problems.
Source: Introduction · p. 1Method
Geoint-R1 generates formally verifiable geometric solutions using supervised fine-tuning, verification-guided reinforcement learning, and curriculum learning, with Geoint as its benchmark.
Source: Introduction · p. 1Results
Geoint-R1 achieves superior performance over existing state-of-the-art multimodal and mathematical reasoning models, especially on tasks requiring explicit auxiliary constructions.
Source: Conclusion · p. 8Takeaways & Limitations
The authors present Geoint-R1 as a foundation for future formalized multimodal reasoning research and as having potential for geometric problem-solving applications.
Source: Conclusion · p. 8Geoint-R1 still struggles with strict theorem application, logical completeness, and symbolic accuracy, especially in complex geometric scenarios.
Source: Error Analysis · p. 7
Abstract
from arXiv · showhide
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.
Introduction
Existing multimodal approaches lack rigorous geometric reasoning and dynamic auxiliary construction. Geoint defines a formal multimodal task and benchmark, then introduces Geoint-R1; experiments report superior performance over state-of-the-art multimodal reasoning models.
Introduction
- Existing approaches lack rigorous reasoning and dynamic construction and visualization of auxiliary elements in complex multimodal geometry.The task also requires formally verifiable reasoning steps and visual feedback aligned with geometric structures and user intent.Source: Introduction · p. 1
- The formal geometric reasoning task requires complete, verifiable solutions from textual descriptions and geometric diagrams.It requires identifying, formally constructing, and visually demonstrating auxiliary elements, beyond semantic correctness alone.Source: Introduction · p. 1
- Geoint contains 1,885 geometry problems across plane, spatial, and solid geometry, with structured text, diagrams, and Lean 4 formal representations.The proof assistant represents geometric elements and relationships in a verifiable framework.Source: Introduction · p. 1
- Geoint-R1 combines supervised fine-tuning and reinforcement learning guided by verification rewards, with curriculum learning for increasingly complex tasks.The reward model assesses correctness, auxiliary-construction accuracy, and structured-output adherence.Source: Introduction · p. 1
- Experiments report Geoint-R1 outperforms state-of-the-art multimodal reasoning models.The introduction's accompanying validation claim is truncated.Source: Introduction · p. 1
Related Work
Existing mathematical and visual-reasoning benchmarks and methods cover varied multimodal tasks, but the cited work does not provide a complete framework linking formal reasoning with visualized auxiliary constructions.
Mathematical Benchmarks
- Existing geometry benchmarks cover varied topics and formats, but do not provide formal representations for stepwise visual reasoning or interactive constructions within a complete framework.Geoint links formalized reasoning steps with visualizations of auxiliary constructions.Source: Mathematical Benchmarks · p. 2
Visual Reasoning
- Visual-reasoning methods use tools, programmatic approaches, and learning strategies, but are not designed for precise mathematical problems with stepwise auxiliary construction and visual feedback.The cited approaches span visual question answering, image manipulation, planning, and related tasks.Source: Visual Reasoning · p. 2
Methodology
Geoint-R1 predicts reasoning steps, auxiliary constructions when needed, and a final answer from a problem's text and diagram. It is trained through supervised fine-tuning followed by reinforcement learning with a verification reward model.
Methodology
- Geoint-R1 maps a geometry problem's textual description and visual diagram to reasoning steps, optional formal auxiliary constructions, and a final answer.Source: Methodology · p. 2
Stage 1: Supervised Fine-Tuning
- Supervised fine-tuning uses negative log-likelihood to teach geometric solution structure and formal-construction syntax from reference solutions.Problems without auxiliary lines use an empty reference construction set.Source: Stage 1: Supervised Fine-Tuning · pp. 2–3
Stage 2: RL with Verification Reward Model
- Reinforcement learning refines the SFT policy using a verification reward model and a curriculum that presents easier problems before harder ones.Problems are ranked by ascending difficulty, estimated from the fraction of sampled candidate solutions that are incorrect.Source: Stage 2: RL with Verification Reward… · p. 3
Verification Reward Model
- The verification reward is a weighted sum of correctness, auxiliary-line construction, and output-format components.Auxiliary-line credit requires matching the reference constructions, while the format component checks the required think-answer template.Source: Verification Reward Model · p. 3
Geoint Dataset
Geoint is a multimodal benchmark for formal and interactive geometric problem solving, with annotations for auxiliary constructions. Its analysis describes the dataset's composition and uses distinct automatic evaluation procedures for answer-based and proof-based questions.
Geoint Dataset
- Geoint contains 1,885 geometry question-answer pairs spanning plane and solid geometry, with structured text, diagrams, and annotations for auxiliary constructions.Problems are manually reviewed, and Lean4 proofs and TikZ diagrams are attached to textual descriptions.Source: Geoint Dataset · pp. 3–4
Data Analysis
- Geoint balances auxiliary-line and non-auxiliary-line problems across topics, while auxiliary-line problems have longer average answers and code.The dataset includes answer-based and proof-based questions with varied diagrammatic and formalized solution lengths.Source: Data Analysis · p. 4
Evaluation Metrics
- Answer-based questions are scored by exact or mathematically equivalent final answers, while proof-based questions receive weighted process scores across five criteria.Proof criteria are logical validity (30%), completeness (20%), correctness (20%), auxiliary-line construction (20%), and clarity (10%).Source: Evaluation Metrics · p. 5
Experiment
Geoint-R1 achieves the highest overall accuracy across answer- and proof-based tasks, with strong results on auxiliary-line problems. Ablations and case studies examine its components and behavior, while error analysis identifies remaining reasoning failures.
Experiment
- Training uses supervised fine-tuning followed by reinforcement learning; comparisons include open- and closed-source multimodal models and math-specific models.The setup freezes the vision encoder and multimodal projector during SFT and uses Qwen2.5-VL-7B for both stages.Source: Experiment · p. 5
Main Results
- 64.72% overall accuracy makes Geoint-R1 the leader; it leads answer-based tasks at 57.01%, while GPT-4o leads proof-based tasks at 77.99%.Geoint-R1 and Gemini-1.5-pro both exceed 72% on proof-based questions.Source: Table 3 · p. 5, Main Results · pp. 5–6
Results on Auxiliary Line Problems
- On auxiliary-line problems, Geoint-R1 scores 68.63% on answer questions and 68.40% on proofs, near the strongest proof-based baselines.GPT-4o scores 74.81% on proofs; most open-source models achieve less than 40% accuracy on these problems.Source: Figure 4 · p. 6, Results on Auxiliary Line Problems · p. 6
Results on Non-Auxiliary Line Problems
- On non-auxiliary problems, Geoint-R1 reaches 51.77% answer accuracy and 76.39% proof accuracy; all models outperform their auxiliary-line results.The passage attributes the difference likely to lower complexity and the lack of required explicit geometric constructions.Source: Figure 5 · p. 6, Results on Non-Auxiliary Line Problems · p. 6
Ablation Study
- Removing LLM Verify, reinforcement learning, or curriculum learning lowers average accuracy; removing verification reward has the largest effect, especially on auxiliary-line problems.On proof-based tasks, Geoint-R1 averages 72.43%, and all ablated models fall behind.Source: Table 4 · p. 6, Ablation Study · p. 6
Case Studies
- In two examples, Geoint-R1 constructs useful auxiliary elements for a planar answer and a spatial proof, while GPT-4o fails to solve each example.For the spatial proof, Geoint-R1 connects the intersection of diagonals to E and proves OE ∥ PC.Source: Case Studies · p. 6
Error Analysis
- Error cases include misapplying the midline theorem, incomplete proportional reasoning after a correct construction, and variable or computational mistakes in multi-step solutions.The examples show difficulties with strict theorem application, logical completeness, and symbolic accuracy in complex geometry.Source: Error Analysis · p. 7
Conclusion
The paper presents Geoint-R1 for multimodal geometric reasoning and introduces Geoint, a 1,885-problem benchmark with Lean4 annotations. Experiments report strong performance, especially on problems requiring explicit auxiliary constructions.
Conclusion
- Geoint-R1 combines supervised fine-tuning, reinforcement learning with verification rewards, and curriculum learning to generate formally verifiable solutions with dynamic auxiliary-line construction.The framework is designed for increasingly complex geometric reasoning tasks.Source: Conclusion · p. 7
- Geoint contains 1,885 high-quality problems spanning diverse geometry categories and incorporates formal Lean4 code annotations.The benchmark is described as a multimodal geometry dataset.Source: Conclusion · p. 7
- Evaluations report that Geoint-R1 outperforms existing multimodal and mathematical reasoning models, particularly on tasks requiring explicit auxiliary constructions.The paper characterizes the framework as a foundation for future formalized multimodal reasoning research.Source: Conclusion · p. 8
Appendix Evaluation Prompts
The appendix presents evaluation prompts for answer-based and proof-based questions. The proof-based prompt follows the process-based approach of DeepTheorem (Zhang et al. 2025c).
Appendix Evaluation Prompts
- Figure 11 presents the evaluation prompt for answer-based questions.The passage identifies the prompt but does not describe its contents.Source: Figure 11 · p. 10
- The appendix distinguishes answer-based from proof-based evaluation prompts, with the latter following DeepTheorem’s process-based approach (Zhang et al. 2025c).Source: Figure 11 · p. 10, Figure 12 · p. 10
- Figure 12 presents the evaluation prompt for proof-based questions, following DeepTheorem’s process-based approach (Zhang et al. 2025c).The passage identifies the prompt but does not describe its contents.Source: Figure 12 · p. 10