A Neuro-Symbolic Approach for Reliable Proof Generation with LLMs: A Case Study in Euclidean Geometry

Este artículo presenta un enfoque neuro-simbólico que combina la recuperación de problemas análogos y la verificación formal para mejorar significativamente la precisión en la generación de pruebas de geometría euclidiana por parte de modelos de lenguaje grandes, superando sus limitaciones en el razonamiento lógico riguroso.

Lo esencial

Imagina que tienes un genio muy talentoso, pero un poco despistado, llamado LLM (un modelo de lenguaje grande). Este genio es increíblemente bueno escribiendo historias, poemas y conversando, pero si le pides que resuelva un problema de matemáticas o escriba una prueba lógica estricta, a menudo se equivoca. ¿Por qué? Porque este genio aprendió "leyendo" millones de libros y aprendió a predecir qué palabra sigue a la otra, no a pensar con lógica rigurosa. Es como un actor que sabe recitar un guion perfectamente, pero si le cambias una línea, se pierde.

Los autores de este paper, Oren, Eitan y Dafna, decidieron darle a este genio un "sistema de apoyo" para que deje de adivinar y empiece a razonar de verdad. Lo llamaron un enfoque Neuro-Simbólico.

Aquí te explico cómo funciona su sistema usando una analogía sencilla:

El Problema: El Genio Solitario

Si le das al genio un problema de geometría (como "demuestra que estos dos ángulos son iguales"), él intenta adivinar la respuesta basándose en patrones que ha visto antes. A veces acierta, pero a menudo inventa pasos que no tienen sentido lógico o se salta reglas importantes. Es como intentar construir un puente sin planos: puede que parezca bonito, pero se caerá.

La Solución: El Equipo de Apoyo

Los autores crearon un equipo de dos expertos para ayudar al genio:

1. El "Detective de Analogías" (La Búsqueda de Problemas Similares)

Imagina que el genio se enfrenta a un problema nuevo y difícil. En lugar de empezar desde cero, el Detective busca en una biblioteca gigante de problemas antiguos que sean estructuralmente idénticos al nuevo, aunque cambien los nombres o los números.

• La analogía: Es como si fueras a cocinar un guiso nuevo y no supieras la receta. En lugar de adivinar los ingredientes, buscas en tu libro de cocina un guiso muy parecido que ya hayas hecho antes. Miras cómo lo hiciste la última vez (los pasos, los ingredientes) y usas eso como guía.
• En el papel: El sistema toma el problema nuevo, lo "abstrae" (quita los nombres específicos como "triángulo ABC" y los cambia por "triángulo genérico") y busca problemas similares. Luego le muestra al genio: "Mira, para resolver este problema parecido, hicimos estos 3 pasos. Úsalos como guía". Esto ayuda al genio a entender la estructura lógica correcta desde el principio.

2. El "Inspector de Calidad" (El Verificador Simbólico)

Una vez que el genio escribe su prueba (su "receta" o "plan"), no se la envía directamente al cliente. Primero pasa por el Inspector.

• La analogía: Imagina que el genio es un arquitecto que dibuja planos. El Inspector es un ingeniero estructural con una calculadora mágica. El Inspector no sabe cuál es la respuesta final, pero revisa cada paso del plano del genio. Si el genio dice "Pongo una viga aquí", el Inspector verifica: "¿Tengo permiso para poner una viga aquí? ¿Cumple con las leyes de la física?".
• En el papel: Si el genio se equivoca (por ejemplo, usa una regla de geometría incorrecta), el Inspector le dice: "Oye, en el paso 3, dijiste que estos ángulos son iguales, pero no demostraste por qué. Aquí están las reglas que sí aplican. Intenta de nuevo".
• El ciclo: El genio recibe la crítica, corrige su trabajo y vuelve a enviarlo. Esto se repite hasta que el Inspector dice: "¡Perfecto! La prueba es válida".

¿Qué lograron? (Los Resultados)

El paper prueba esto con problemas de geometría de nivel de examen (SAT). Los resultados fueron impresionantes:

• Sin ayuda: El genio (modelos como o1 o Gemini) acertaba solo el 10% de las veces en problemas difíciles.
• Con el equipo: Al usar al Detective (analogías) y al Inspector (verificación), la tasa de acierto subió al 80%.
• El ahorro: Además, al usar solo las "recetas" (teoremas) de los problemas similares, el sistema no tenía que leer todo el libro de cocina (18,000 teoremas), sino solo una pequeña lista de 2,500. Esto hace que el proceso sea más rápido y barato.

En Resumen

Este paper nos dice que no necesitamos esperar a que las IAs se vuelvan "humanas" o perfectas por sí solas. En su lugar, podemos crear un sistema donde:

1. La IA aprende de ejemplos similares (como un estudiante que mira ejercicios resueltos).
2. Un sistema lógico revisa y corrige sus errores paso a paso.

Es como pasar de tener un estudiante brillante pero despistado, a tener un estudiante brillante con un tutor experto y un corrector estricto. El resultado es un sistema que no solo "parece" inteligente, sino que es confiable y correcto, algo vital para aplicaciones reales donde un error no es una opción (como en medicina, ingeniería o seguridad).

Resumen técnico

Aquí tienes un resumen técnico detallado del artículo en español, estructurado según los puntos solicitados:

Título: Un Enfoque Neuro-Simbólico para la Generación de Pruebas Confiables con LLMs: Un Estudio de Caso en Geometría Euclidiana

Autores: Oren Sultan, Eitan Stern, Dafna Shahaf (Universidad Hebrea de Jerusalén).

---

1. El Problema

Los Grandes Modelos de Lenguaje (LLMs) actuales, a pesar de su rendimiento en tareas generales, enfrentan dificultades significativas en dominios formales que requieren deducción lógica rigurosa y razonamiento simbólico, como la generación de pruebas matemáticas.

• Causas raíz: La arquitectura de los LLMs se basa en la generación de secuencias probabilísticas aprendidas de patrones textuales, lo que carece de la certeza absoluta y la ausencia de ambigüedad necesarias en las matemáticas.
• Desafíos específicos: Las pruebas matemáticas exigen coherencia lógica sostenida y razonamiento jerárquico. Pequeños cambios superficiales en los problemas pueden causar caídas drásticas en el rendimiento, sugiriendo que los modelos a menudo dependen del "ajuste de patrones" en lugar del razonamiento matemático genuino.
• Consecuencia: La falta de fiabilidad impide su aplicación en tareas críticas de seguridad y en campos como la educación y la ciencia, donde la veracidad es innegociable.

2. Metodología

Los autores proponen un enfoque neuro-simbólico que combina las capacidades generativas de los LLMs con dos componentes estructurados complementarios: guía analógica y verificación simbólica. El sistema opera en un bucle iterativo (ver Figura 1 del artículo):

A. Abstracción y Recuperación de Problemas Análogos (Guía Analógica)

• Abstracción: Se transforma el problema objetivo y todo el conjunto de datos (FormalGeo-7k) reemplazando nombres de entidades (puntos, líneas) y valores numéricos por marcadores de posición (<word>, <num>). Esto permite identificar problemas estructuralmente similares independientemente de sus detalles superficiales.
• Recuperación: Se utiliza un regresor neuronal entrenado para predecir la similitud de las pruebas basándose en la similitud estructural de los problemas (construcción, condiciones y objetivo).
• Selección: Se recuperan los problemas análogos con mayor similitud y sus pruebas formales completas.
• Optimización del Diccionario: En lugar de proporcionar todo el diccionario de teoremas (196 teoremas), el sistema filtra y presenta al LLM solo los teoremas utilizados en las pruebas de los problemas análogos. Esto reduce el contexto de ~18k tokens a ~2.5k tokens, disminuyendo costos y reduciendo el espacio de búsqueda.

B. Generación de Pruebas por el LLM

• Se utiliza un prompt de few-shot learning que incluye: la descripción del problema objetivo, los problemas análogos recuperados con sus pruebas, y el diccionario de teoremas filtrado.
• El LLM genera una prueba formal paso a paso, invocando teoremas específicos del diccionario.

C. Verificador Simbólico y Retroalimentación Iterativa

• Verificador: Un sistema externo basado en lógica formal y razonamiento algebraico (utilizando el solucionador SMT Z3) verifica la prueba generada.
• Independencia: El verificador no conoce la solución; evalúa si la respuesta numérica y la conclusión se derivan lógicamente de las premisas y pasos proporcionados.
• Tipos de Errores (Tiers): El verificador clasifica los errores en tres niveles para dar retroalimentación específica:
  1. Sintaxis: Violaciones en la llamada a teoremas (argumentos incorrectos, teoremas no definidos).
  2. Premisas: Uso de teoremas sin que sus premisas hayan sido derivadas previamente.
  3. Objetivo no alcanzado: La prueba es sintácticamente correcta pero no llega a la conclusión deseada o la solución derivada difiere.
• Bucle: Si hay errores, el verificador devuelve una explicación en lenguaje natural. El LLM reescribe la prueba incorporando esta retroalimentación. Este ciclo se repite hasta obtener una prueba válida o agotar el límite de reintentos (máximo 5 reintentos por ejecución).

3. Contribuciones Clave

1. Sistema Neuro-Simbólico: Propuesta de un marco que integra la guía analógica (recuperación de problemas similares) y la verificación simbólica para mejorar la generación de pruebas en LLMs generales.
2. Verificador Específico para Geometría: Diseño de un verificador que evalúa la prueba completa (no solo la respuesta numérica) y proporciona retroalimentación estructurada y expresiva sobre la lógica del razonamiento.
3. Reducción de Costos y Contexto: Demostración de que filtrar el diccionario de teoremas basándose en problemas análogos mejora la precisión y reduce drásticamente el uso de tokens (de 18k a 2.5k en promedio).
4. Mejoras Cuantificables: Validación empírica de que el método supera significativamente a los modelos base en precisión de pruebas.
5. Recursos Abiertos: Liberación de código, datos procesados y scripts de evaluación.

4. Resultados

Los experimentos se realizaron en el conjunto de datos FormalGeo-7k (6,981 problemas de geometría de nivel SAT) utilizando dos modelos base: OpenAI o1 y Gemini-2.5-Flash.

• Rendimiento General (o1):
  • El modelo base (sin análogos ni verificador) alcanzó un 10% de precisión.
  • El enfoque completo (analogía + verificador + múltiples ejecuciones) alcanzó un 80% de precisión.
  • Mejora: Un aumento del 58% al 70% sobre el modelo o1 base.
• Rendimiento General (Gemini-2.5-Flash):
  • Se observaron mejoras del 52% al 64% sobre el modelo base.
• Análisis de Componentes (Ablación):
  • Recuperación de Analogías: Aumentó la precisión del 10% al 48% en la primera ejecución sin reintentos.
  • Retroalimentación del Verificador: Añadió un ~20% de mejora adicional al permitir reintentos.
  • Múltiples Ejecuciones: Contribuyó significativamente, especialmente en problemas difíciles (niveles 4-5), donde la mejora fue del 20-30%.
• Precisión vs. Respuesta Numérica: Mientras que el modelo base a menudo encontraba la respuesta numérica correcta pero fallaba en generar la prueba lógica (57.7% de éxito en pruebas vs. 90% en respuestas), el método propuesto logró un 100% de acierto en respuestas y un 80% en pruebas correctas, cerrando la brecha entre la intuición numérica y el razonamiento formal.
• Eficiencia: El método con análogos requirió menos reintentos y ejecuciones que el modelo base para alcanzar la solución correcta.

5. Significado e Impacto

• Fiabilidad en IA: El trabajo demuestra que es posible mejorar drásticamente la fiabilidad, precisión y consistencia de los LLMs en tareas críticas mediante la integración de componentes simbólicos.
• Escalabilidad: Al reducir el contexto necesario (filtrado de teoremas), el método hace viable la aplicación de LLMs en dominios formales complejos sin costos prohibitivos.
• Aplicaciones Futuras:
  • Educación: Sistemas de tutoría que ofrecen problemas análogos y retroalimentación paso a paso.
  • Seguridad y Ciencia: Validación de derivaciones complejas en sistemas donde el error no es una opción.
  • Generalización: Aunque probado en geometría, el marco es adaptable a otros dominios que admitan verificación basada en SMT (Satisfiability Modulo Theories).

En conclusión, este estudio establece un "planteamiento" (blueprint) escalable para construir sistemas de IA confiables en dominios STEM, combinando la flexibilidad de los LLMs con la precisión del razonamiento formal.