TrustGeoGen: Motore di Dati Scalabile e Formalmente Verificato per la Risoluzione Affidabile di Problemi Geometrici Multi-modali

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

April 22, 2025

Autori: Daocheng Fu, Zijun Chen, Renqiu Xia, Qi Liu, Yuan Feng, Hongbin Zhou, Renrui Zhang, Shiyang Feng, Peng Gao, Junchi Yan, Botian Shi, Bo Zhang, Yu Qiao

cs.AI

Abstract

La risoluzione di problemi geometrici matematici (GPS) richiede spesso un'integrazione efficace di informazioni multimodali e una coerenza logica verificabile. Nonostante il rapido sviluppo dei modelli linguistici di grandi dimensioni nella risoluzione generale di problemi, rimangono irrisolte sia le questioni metodologiche che quelle relative ai benchmark, soprattutto considerando il fatto che gli attuali benchmark sintetici per GPS spesso non sono auto-verificati e contengono rumore e informazioni auto-contraddittorie a causa delle illusioni dei LLM. In questo articolo, proponiamo un motore di dati scalabile chiamato TrustGeoGen per la generazione di problemi, con verifica formale per fornire un benchmark principiato, che riteniamo getti le basi per ulteriori sviluppi di metodi per GPS. Il motore sintetizza dati geometrici attraverso quattro innovazioni chiave: 1) generazione multimodale allineata di diagrammi, descrizioni testuali e soluzioni passo-passo; 2) verifica formale che garantisce percorsi di ragionamento conformi alle regole; 3) un meccanismo di bootstrapping che consente l'escalation della complessità tramite la generazione ricorsiva di stati; e 4) i nostri algoritmi GeoExplore series che producono simultaneamente varianti multi-soluzione e tracce di backtracking auto-riflessive. Attraverso la verifica logica formale, TrustGeoGen produce il dataset GeoTrust-200K con integrità modale garantita, insieme al testset GeoTrust-test. Gli esperimenti rivelano che i modelli all'avanguardia raggiungono solo il 49,17% di accuratezza su GeoTrust-test, dimostrando la sua severità valutativa. Crucialmente, i modelli addestrati su GeoTrust raggiungono una generalizzazione OOD su GeoQA, riducendo significativamente le incoerenze logiche rispetto alle pseudo-etichette annotate da OpenAI-o1. Il nostro codice è disponibile all'indirizzo https://github.com/Alpha-Innovator/TrustGeoGen.

English

Mathematical geometric problem solving (GPS) often requires effective integration of multimodal information and verifiable logical coherence. Despite the fast development of large language models in general problem solving, it remains unresolved regarding with both methodology and benchmarks, especially given the fact that exiting synthetic GPS benchmarks are often not self-verified and contain noise and self-contradicted information due to the illusion of LLMs. In this paper, we propose a scalable data engine called TrustGeoGen for problem generation, with formal verification to provide a principled benchmark, which we believe lays the foundation for the further development of methods for GPS. The engine synthesizes geometric data through four key innovations: 1) multimodal-aligned generation of diagrams, textual descriptions, and stepwise solutions; 2) formal verification ensuring rule-compliant reasoning paths; 3) a bootstrapping mechanism enabling complexity escalation via recursive state generation and 4) our devised GeoExplore series algorithms simultaneously produce multi-solution variants and self-reflective backtracking traces. By formal logical verification, TrustGeoGen produces GeoTrust-200K dataset with guaranteed modality integrity, along with GeoTrust-test testset. Experiments reveal the state-of-the-art models achieve only 49.17\% accuracy on GeoTrust-test, demonstrating its evaluation stringency. Crucially, models trained on GeoTrust achieve OOD generalization on GeoQA, significantly reducing logical inconsistencies relative to pseudo-label annotated by OpenAI-o1. Our code is available at https://github.com/Alpha-Innovator/TrustGeoGen