TrustGeoGen: Motor de Dados Escalável e Formalmente Verificado para Resolução Confiável de Problemas Geométricos Multimodais

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

April 22, 2025

Autores: 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

Resumo

A resolução de problemas geométricos matemáticos (GPS) frequentemente requer a integração eficaz de informações multimodais e coerência lógica verificável. Apesar do rápido desenvolvimento de modelos de linguagem de grande escala na resolução geral de problemas, questões metodológicas e de benchmarks permanecem sem solução, especialmente considerando que os benchmarks sintéticos de GPS existentes muitas vezes não são autoverificados e contêm ruídos e informações contraditórias devido à ilusão dos LLMs. Neste artigo, propomos um mecanismo de dados escalável chamado TrustGeoGen para geração de problemas, com verificação formal para fornecer um benchmark fundamentado, que acreditamos estabelecer as bases para o desenvolvimento futuro de métodos para GPS. O mecanismo sintetiza dados geométricos por meio de quatro inovações principais: 1) geração alinhada multimodal de diagramas, descrições textuais e soluções passo a passo; 2) verificação formal garantindo caminhos de raciocínio compatíveis com as regras; 3) um mecanismo de bootstrapping que permite a escalada de complexidade por meio de geração recursiva de estados; e 4) nossos algoritmos da série GeoExplore, que produzem simultaneamente variantes de múltiplas soluções e traços de retrocesso autorreflexivos. Por meio da verificação lógica formal, o TrustGeoGen produz o conjunto de dados GeoTrust-200K com integridade modal garantida, juntamente com o conjunto de testes GeoTrust-test. Experimentos revelam que os modelos state-of-the-art alcançam apenas 49,17% de precisão no GeoTrust-test, demonstrando sua rigorosidade de avaliação. Crucialmente, modelos treinados no GeoTrust alcançam generalização OOD no GeoQA, reduzindo significativamente as inconsistências lógicas em relação às pseudoanotações geradas pelo OpenAI-o1. Nosso código está disponível em 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