En el artículo «MATP-BENCH: Can MLLM be a good automated theorem prover for multimodal problems?», los autores investigan la aplicabilidad de los modelos de lenguaje grandes multimodales (MLLMs) al problema de la demostración automática de teoremas que involucran componentes tanto textuales como visuales. Motivados por las limitaciones de los enfoques puramente textuales en dominios como la geometría, donde los diagramas constituyen información esencial, desarrollan un marco de evaluación sistemático para esta clase de problemas.

La contribución principal consiste en la construcción de MATP-BENCH, un conjunto de datos que contiene más de 1000 problemas matemáticos multimodales formalizados en tres asistentes de demostración: Lean 4, Coq e Isabelle/HOL. El corpus abarca problemas de complejidad variable, desde el nivel de secundaria hasta competiciones matemáticas avanzadas, proporcionando así un banco de pruebas comprehensivo para evaluar capacidades de razonamiento multimodal.

Los experimentos incluyen seis modelos representativos: tres con capacidades especializadas de razonamiento (OpenAI-o1, Claude-3.7-Sonnet-Thinking, Gemini-2.0-Flash-Thinking) y tres sin estas capacidades (GPT-4.1, Qwen2.5-VL-Instruct-70B, Llama3.2-Vision-Instruct-11B). Los resultados revelan que, si bien los modelos demuestran competencia en la comprensión de problemas y formalización de enunciados, exhiben deficiencias significativas en la construcción de cadenas de inferencia válidas.

El análisis establece que la principal limitación no radica en las capacidades de percepción visual sino en la insuficiencia del razonamiento simbólico formal. Los autores concluyen que los MLLMs actuales no constituyen demostradores automáticos efectivos para problemas multimodales, identificando la brecha entre comprensión multimodal y razonamiento lógico como el desafío fundamental a resolver.

MATP-BENCH se posiciona como el primer banco de prueba estándar para este dominio, proporcionando una base metodológica para la evaluación de futuros desarrollos en demostración automática multimodal.