Resumo Técnico: Hilbert-Geo

Declaração do Problema

A resolução de problemas geométricos é uma tarefa crítica de raciocínio multimodal. Embora avanços recentes em Modelos de Linguagem Grandes Multimodais (MLLMs) tenham alcançado sucesso significativo em geometria plana, eles lutam consideravelmente com geometria sólida. O artigo identifica três obstáculos primários que impedem os MLLMs de dominar a geometria sólida:

1. Complexidade Espacial 3D: A geometria sólida exige modelagem precisa de relações espaciais 3D, estruturas ocluídas e transformações, o que frequentemente excede as capacidades de lógica espacial abstrata dos modelos atuais.
2. Fundamentação Multimodal: A interpretação de representações 2D de objetos 3D requer alinhamento visual-linguístico sofisticado. Os MLLMs frequentemente sofrem de erros de percepção e alucinações ao inferir informações espaciais implícitas a partir de diagramas.
3. Confiabilidade Quantitativa: Os MLLMs são propensos a erros de cálculo em tarefas quantitativas, minando a confiabilidade de suas soluções.

Existentes conjuntos de dados e benchmarks (por exemplo, SolidGeo, MathVerse-Solid) são descritos como dispersos, potencialmente contendo vazamento de dados, dependendo de respostas geradas por LLMs propensas a erros, ou incluindo problemas de modelagem de física/matemática de baixa relevância. Além disso, a maioria dos benchmarks avalia apenas respostas finais, falhando em detectar falhas no raciocínio.

Metodologia: Framework Hilbert-Geo

Para abordar esses desafios, os autores propõem o Hilbert-Geo, o primeiro framework de linguagem formal unificado especificamente projetado para geometria sólida. O sistema emprega um pipeline Parse2Reason consistindo em duas etapas distintas:

1. Linguagem Formal de Geometria Sólida

O núcleo do framework é uma extensão de linguagem formal do sistema existente FormalGeo (geometria plana).

• Biblioteca de Predicados: Uma biblioteca abrangente contendo 120 predicados, incluindo 35 predicados fundamentais, 20 tipos de entidades (por exemplo, Cubo, Cone, Prisma), 35 relações entre entidades (por exemplo, paralelismo/perpendicularidade entre planos) e 30 descritores de atributos.
• Banco de Teoremas: Uma extensão do sistema de teoremas de geometria plana, contendo 220 teoremas cobrindo premissas e conclusões para geometria sólida (por exemplo, fórmulas de volume de esfera, julgamentos de perpendicularidade linha-plano).
• Linguagem de Descrição Condicional (CDL): Uma linguagem formalizada usada para representar tanto descrições de problemas em linguagem natural quanto diagramas visuais. A CDL elimina ambiguidades multimodais ao fundamentar entidades textuais em estruturas visuais.

2. Pipeline Parse2Reason

• Parser de Formalização Multimodal (M2FP): Este módulo traduz texto em linguagem natural e diagramas visuais na CDL formal. Ele utiliza engenharia de prompts com exemplos few-shot projetados por especialistas para guiar os MLLMs na análise de condições geométricas em predicados estruturados. O parser garante consistência cross-modal verificando se as entidades no texto e nas CDLs de imagem são declaradas na CDL de construção.
• Motor de Raciocínio em Geometria Sólida (SGRE): Uma vez que o problema é formalizado na CDL, o SGRE realiza inferência relacional e computação algébrica. Ele opera como um motor baseado em busca que constrói uma árvore de raciocínio:
  • Inicializa uma árvore baseada em nós onde os nós representam estados geométricos.
  • Iterativamente combina nós expansíveis com o banco de teoremas, aplicando substituições lógicas e cálculos.
  • Gera processos de raciocínio estritamente corretos, verificáveis e legíveis por humanos.
  • O motor é projetado para lidar com a natureza NP-difícil do espaço de busca, embora note que uma explosão combinatória pode ocorrer em problemas altamente complexos.

Contribuições Principais

O artigo delineia quatro contribuições primárias:

1. Framework Formal de Geometria Sólida: Desenvolvimento de uma Biblioteca de Predicados e Banco de Teoremas especializados, adaptados para entidades 3D e relações espaciais, estendendo as fundações teóricas da formalização da geometria plana.
2. Parser de Formalização Multimodal: Um pipeline capaz de analisar tanto linguagem natural quanto diagramas visuais em uma linguagem formal unificada (CDL), resolvendo ambiguidades cross-modal.
3. Motor de Raciocínio Geométrico: Um motor dedicado para realizar dedução simbólica verificável em problemas formalizados, garantindo coerência lógica e rastreabilidade.
4. Conjuntos de Dados Anotados por Especialistas: A curadoria de dois conjuntos de dados de alta qualidade:
   • SolidFGeo2k: 1.908 problemas de geometria sólida com anotações formais, caminhos de raciocínio e respostas.
   • PlaneFGeo3k: 3.022 problemas de geometria plana com anotações rigorosas similares.
     Ambos os conjuntos de dados são anotados manualmente por especialistas do domínio para garantir precisão e consistência, abordando a escassez de recursos de raciocínio de alta qualidade.

Resultados Experimentais

Os autores conduziram experimentos extensivos comparando o Hilbert-Geo com MLLMs líderes (incluindo GPT-5, Gemini 2.5 Pro, Claude 3.7 Sonnet) e desempenho humano.

• Desempenho em SolidFGeo2k:
  • O Hilbert-Geo alcançou 77,3% de precisão (usando Gemini-2.5-Pro para análise), superando substancialmente o melhor MLLM, Gemini-2.5-Pro (54,2%), e o GPT-5 (50,6%).
  • Aproximou-se do desempenho humano (81,8%) e superou significativamente modelos de código aberto (por exemplo, Llama 3.3 70B em 33,6%).
• Desempenho em MathVerse-Solid:
  • O Hilbert-Geo alcançou 84,1% de precisão, superando o GPT-5 (62,9%) e o Gemini 2.5 Pro (59,7%).
• Desempenho em PlaneFGeo3k:
  • Demonstrando generalidade, o Hilbert-Geo alcançou 80,2% de precisão em tarefas de geometria plana, superando MLLMs líderes (GPT-5 em 68,1%) e aproximando-se do desempenho humano (87,9%).
• Análise de Erros:
  • A análise das falhas dos MLLMs revelou que erros de percepção visual e erros de raciocínio representam ~73-76% das falhas.
  • O Hilbert-Geo reduziu significativamente alucinações e erros de percepção visual ao impor restrições formais durante a fase de análise.
  • O motor de raciocínio não apresentou erros de cálculo ou raciocínio quando a CDL de entrada estava correta; as falhas foram atribuídas principalmente a distorções de análise ou explosão combinatória no espaço de busca.

Significado e Alegações

O artigo alega que o Hilbert-Geo representa um passo significativo para frente no raciocínio geométrico automatizado, fechando a lacuna entre percepção neural e rigor simbólico. Seu significado reside em:

• Abordando a Lacuna 3D: É o primeiro framework unificado a enfrentar os desafios únicos da geometria sólida, indo além das limitações de sistemas focados em geometria plana.
• Confiabilidade e Verificabilidade: Ao desacoplar percepção (análise) de raciocínio (dedução simbólica), o sistema gera soluções estritamente corretas, verificáveis e legíveis por humanos, mitigando a natureza de "caixa preta" e os riscos de alucinação de MLLMs puros.
• Benchmarking: A introdução do SolidFGeo2k e PlaneFGeo3k fornece um benchmark crítico e de alta qualidade para avaliar o raciocínio geométrico, afastando-se de conjuntos de dados dependentes de respostas potencialmente falhas geradas por LLMs.
• Generalidade: O sucesso do framework em tarefas de geometria sólida e plana demonstra a robustez da abordagem neuro-simbólica no manuseio de diversos cenários de raciocínio geométrico.

Os autores concluem que, embora déficits de percepção visual e raciocínio lógico permaneçam gargalos para os MLLMs atuais, abordagens estruturadas e formais como o Hilbert-Geo oferecem um caminho viável para superar essas limitações na lógica espacial e interpretação multimodal.