Geoint-R1: Formalizing Multimodal Geometric Reasoning with Dynamic Auxiliary Constructions

TL;DR

Geoint-R1 is a multimodal framework that enhances formal geometric reasoning by integrating auxiliary construction, formal verification with Lean4, and visualization, supported by a comprehensive benchmark.

Contribution

It introduces Geoint-R1, a novel multimodal reasoning system that constructs and verifies auxiliary geometric elements, advancing formal reasoning in geometry.

Findings

Outperforms existing models on complex geometry problems

Successfully integrates auxiliary element construction with formal verification

Provides a new benchmark for formal geometric reasoning

Abstract

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.