TrustGeoGen: Formal-Verified Data Engine for Trustworthy Multi-modal Geometric Problem Solving

Abstract

Geometric problem solving (GPS) requires precise multimodal understanding and rigorous, step-by-step logical reasoning. However, developing capable Multimodal Large Language Models (MLLMs) for GPS is heavily bottlenecked by the scarcity of high-quality, verifiable data. Existing data acquisition paradigms either suffer from modality incompleteness and unverified logical gaps ("leaps-of-faith"), or rely on formal engines that generate rigid, structurally homogeneous data, failing to produce high-difficulty problems or foster genuine natural-language reasoning. To overcome these limitations, we introduce TrustGeoGen, an autonomous and formalized geometric data generation engine. TrustGeoGen strictly guarantees reasoning trustworthiness through formal verification while generating multimodally integrated data, including premises, visual diagrams, and solutions. To systematically scale problem difficulty, we incorporates difficulty-aware filtering and iterative bootstrapping mechanism. Furthermore, we propose "connection thinking" to bridge the semantic gap between rigid formal logic and fluent human-like reasoning, ensuring coherent logical transitions. We also introduce the GeoExplore family of sampling algorithms to extract diverse problem-solving trajectories based on various thinking templates. Extensive experiments demonstrate that training models on our synthesized dataset, GeoTrust, substantially enhances deep geometric reasoning capabilities and yields significant performance gains across out-of-distribution (OOD) benchmarks, including GeoQA, Geometry3K, and OlympiadBench.Our code and data can be found at https://github.com/InternScience/TrustGeoGen

Figures (9)

• Figure 1: Overview of TrustGeoGen: (1) Constructor builds geometric premises and visual diagrams; (2) Reasoner generates a formally validated reasoning graph; (3) Sampler utilizes GeoExplore algorithms to select conclusions and trace diverse reasoning paths; (4) Translator converts formal logic into fluent natural language using "connection thinking". A bootstrap mechanism amplifies problem difficulty iteratively.
• Figure 2: Simple illustration of how Translator works
• Figure 3: Simple examples of Multi-solution and Self-reflective traceback data.
• Figure 4: Data distribution and augmentation. (a) Distribution of reasoning lengths, with most samples below 60 steps and a sharp decline beyond 80; the zoomed-in view highlights the ultra-long reasoning range. (b) Distribution of premise ratios, reflecting variability in logical dependencies. (c) Comparison of reasoning lengths before and after bootstrap augmentation, showing increased deep-reasoning samples (reasoning length $\ge$ 40) and reduced shallow ones.
• Figure 5: Visualization examples of different difficulty levels in GeoTrust-test, where "reasoning length" indicates step length of reasoning path and "premise ratio" refer to the ratio of premises unutilized during formal reasoning and premises provided in the question.