LeanTutor: Towards a Verified AI Mathematical Proof Tutor

Este artículo presenta LeanTutor, un prototipo de tutor de demostraciones matemáticas basado en IA que combina las capacidades de los modelos de lenguaje grandes con la corrección verificable de los demostradores de teoremas Lean, y lo evalúa mediante el nuevo conjunto de datos PeanoBench.

Lo esencial

Imagina que estás aprendiendo a cocinar un plato muy complejo, como un soufflé. Tienes dos tipos de ayuda disponibles:

1. El Chef de IA (como ChatGPT): Es un chef muy charlatán y rápido. Te explica las recetas con palabras bonitas y te da consejos. Pero, a veces, se inventa ingredientes que no existen, te dice que el horno está a 200 grados cuando en realidad es 300, o te da la receta completa del soufflé en lugar de dejarte cocinarlo tú mismo. Es genial para conversar, pero no puedes confiar ciegamente en que su matemática (o su cocina) sea perfecta.
2. El Robot Checo-Exacto (como Lean): Es un robot que revisa cada paso de tu receta con una lupa microscópica. Si te saltas un paso o usas la sal equivocada, el robot te detiene y dice: "Error: esto no es válido". Es 100% preciso y nunca miente. El problema es que el robot solo habla un idioma muy raro y difícil (código de programación) que a los estudiantes les cuesta horrores aprender.

LeanTutor es el proyecto de este paper que intenta crear el súper-tutor perfecto combinando a ambos.

¿Cómo funciona LeanTutor?

Imagina que LeanTutor es un traductor mágico que conecta al estudiante con el Robot Checo-Exacto, usando al Chef de IA como intermediario. Funciona en tres pasos, como una línea de montaje:

1. El Traductor (Autoformalizador):
   El estudiante escribe su prueba matemática en español normal (o inglés, en el caso del paper), como si estuviera hablando con un amigo. El sistema toma esas palabras y las traduce instantáneamente al "idioma del robot" (código Lean).

   • La analogía: Es como si el estudiante dijera "sumo los dos números" y el sistema lo convirtiera automáticamente en rw [add_zero] para que el robot lo entienda.

2. El Inspector (Verificador de Pruebas):
   Una vez traducido, el Robot Checo-Exacto revisa el código.

   • Si todo está bien, el robot dice "¡Siguiente!".
   • Si hay un error, el robot grita "¡ALTO! Aquí hay un fallo".
   • Lo genial: Si el estudiante se equivoca, el sistema no solo dice "está mal", sino que sabe exactamente dónde está el fallo porque el robot lo detectó.

3. El Mentor (Generador de Feedback):
   Aquí es donde entra la magia. El sistema toma la información del Robot (el error exacto) y se la pasa al Chef de IA. Pero le da una instrucción especial: "No le des la respuesta completa. Dile al estudiante qué está mal y hazle una pregunta para que lo piense".

   • En lugar de decirte "La respuesta es 5", el tutor te dice: "¿Te has dado cuenta de que olvidaste sumar el cero en el primer paso? ¿Qué pasaría si lo intentas de nuevo?".

¿Por qué es importante?

El problema con los tutores actuales es que o bien son demasiado fáciles (la IA te da la respuesta y no aprendes nada) o demasiado difíciles (tienes que aprender un lenguaje de programación para usar un verificador matemático).

LeanTutor intenta encontrar el "punto dulce":

• Te permite hablar en tu idioma natural.
• Te da retroalimentación inmediata y privada.
• Pero lo más importante: Se asegura de que la matemática sea 100% correcta porque la verifica con el Robot, no solo con la IA que a veces alucina.

El "Gimnasio" de Pruebas (PeanoBench)

Para probar si su sistema funcionaba, los autores crearon un "gimnasio" llamado PeanoBench. Imagina que es un libro de ejercicios de matemáticas donde cada problema tiene dos versiones:

1. La versión escrita por humanos (como en un examen).
2. La versión escrita en código para el robot.

Además, crearon versiones "trampa" donde los estudiantes (o sus avatares) cometían errores comunes, como saltarse un paso o asumir cosas sin probarlas. Usaron este libro de ejercicios para entrenar y probar a LeanTutor.

Los Resultados y los Retos

• Lo bueno: El sistema funcionó bastante bien. Fue capaz de traducir las ideas del estudiante al código, detectar errores y dar pistas útiles sin arruinar la sorpresa de la solución. Funcionó mejor cuando tenía una "solución de referencia" (como un libro de respuestas del profesor) para comparar.
• Lo difícil: A veces, traducir el lenguaje humano al lenguaje del robot es complicado. Si el estudiante escribe algo muy confuso o con un estilo muy peculiar, el traductor puede fallar. Si el traductor falla, el tutor no puede ayudar.

En resumen

LeanTutor es como tener un profesor particular que nunca se equivoca en la matemática, pero que te habla como un amigo y te guía paso a paso sin darte la respuesta en bandeja de plata. Combina la fluidez de la inteligencia artificial con la precisión infalible de los verificadores matemáticos, para que los estudiantes aprendan a pensar críticamente sin frustrarse con códigos extraños ni confundirse con respuestas falsas.

Es un primer paso (un "concepto") hacia un futuro donde la IA nos ayude a aprender matemáticas de verdad, no solo a copiar respuestas.

Resumen técnico

Aquí tienes un resumen técnico detallado del artículo "LeanTutor: Towards a Verified AI Mathematical Proof Tutor", traducido y estructurado en español:

1. El Problema

El uso indiscriminado de Modelos de Lenguaje Grande (LLMs) como ChatGPT en la educación matemática presenta desafíos significativos:

• Alucinaciones y errores: Los LLMs son propensos a generar respuestas incorrectas pero convincentes y a fallar en la identificación de errores de razonamiento.
• Falta de pedagogía: Tienden a dar la respuesta completa en lugar de guiar al estudiante, lo que obstaculiza el desarrollo del pensamiento crítico.
• Limitaciones de los probadores de teoremas tradicionales: Herramientas como Lean ofrecen corrección verificada, pero su sintaxis formal es difícil de aprender para los estudiantes, lo que limita su adopción como tutores.

Existe una necesidad urgente de un sistema híbrido que combine la fluidez en lenguaje natural de los LLMs con la rigurosidad matemática de los probadores de teoremas.

2. Metodología: LeanTutor

Los autores proponen LeanTutor, un sistema de tutoría de pruebas matemáticas que integra LLMs y el probador de teoremas Lean. El sistema funciona como un ciclo de retroalimentación en lenguaje natural (NL) pero con verificación formal en el backend.

Arquitectura del Sistema

LeanTutor consta de tres módulos principales:

1. Autoformalizador / Verificador de Pruebas:
   • Traduce paso a paso las pruebas escritas por el estudiante en lenguaje natural a código Lean.
   • Utiliza un enfoque "paso a paso" (step-by-step) en lugar de generar la prueba completa de una vez.
   • Compila cada paso en Lean para verificar la corrección. Si el compilador devuelve un error, se identifica el paso como incorrecto.
   • Utiliza un contexto que incluye una solución de referencia (staff solution), un diccionario de teoremas y tácticas, y ejemplos de pocos disparos (few-shot).
2. Generador del Siguiente Paso (Next Step Generator - NSG):
   • Se activa cuando la prueba del estudiante está incompleta o es incorrecta.
   • Realiza una búsqueda en profundidad (DFS) dirigida por un LLM para generar candidatos de tácticas Lean.
   • Aplica un "control de progreso" para evitar ciclos y tácticas prohibidas, asegurando que los pasos generados avancen hacia una prueba completa sin revelar la solución final prematuramente.
3. Generador de Retroalimentación en Lenguaje Natural:
   • Combina los errores del compilador de Lean, el estado de la prueba y la táctica sugerida por el NSG.
   • Genera tres tipos de retroalimentación: identificación del error, preguntas o pistas (hints) para guiar al estudiante, y un "paso final" explícito (bottom-out hint) si es necesario.

Dataset: PeanoBench

Para evaluar el sistema, los autores crearon PeanoBench, un conjunto de datos derivado del Natural Numbers Game (NNG4):

• Contenido: 371 pruebas de Aritmética de Peano.
• Estructura: Cada prueba tiene una versión en lenguaje natural y una versión formal equivalente en Lean.
• Variaciones: Incluye soluciones correctas (basadas en staff, estilo ecuacional y estilo de justificación) y pruebas incorrectas generadas algorítmicamente omitiendo pasos lógicos clave.

3. Contribuciones Clave

• Marco Híbrido Verificado: Demuestra la viabilidad de combinar LLMs (para la interfaz de usuario) con probadores de teoremas (para la verificación lógica) en un entorno de tutoría.
• Autoformalización Fiel: Propone un enfoque paso a paso para la autoformalización, que es más robusto para detectar errores tempranos que la generación de pruebas completas.
• Métrica de Evaluación Nueva: Desarrollan una métrica para medir la "autoformalización fiel" que no solo verifica la coincidencia de cadenas de texto, sino que compara los estados de prueba (proof states) normalizando los nombres de las variables. Esto permite evaluar si una táctica generada es semánticamente equivalente a la referencia, incluso si la sintaxis varía.
• Dataset Especializado: PeanoBench, diseñado específicamente para evaluar tutores de pruebas, con variaciones de estilo y errores comunes de estudiantes.

4. Resultados

Los experimentos se centraron en la evaluación del autoformalizador y del sistema completo (LeanTutor vs. una línea base que usa solo LLM).

• Rendimiento del Autoformalizador:

  • El modelo con solución de referencia en contexto (Staff Solution) superó significativamente a la línea base.
  • Precisión de tácticas (Correctas): 56.8% (con Staff) vs. 32.9% (línea base).
  • Precisión de pruebas completas (Correctas): 18.0% (con Staff) vs. 6.7% (línea base).
  • Pruebas Incorrectas: El enfoque paso a paso fue superior al de "prueba completa" para detectar errores, logrando un 30.1% de éxito en la formalización de pruebas incorrectas (vs. 14.4% de la línea base).
  • Hallazgo: El modelo depende en gran medida de la solución de referencia; cuando la formalización requerida no estaba en la referencia, el rendimiento caía.

• Evaluación del Sistema Completo (LeanTutor):

  • Se evaluó la retroalimentación generada en 4 ejes: Precisión, Relevancia, Legibilidad y Fuga de Respuesta (Answer Leakage).
  • LeanTutor superó a la línea base en Precisión y Relevancia de la retroalimentación.
  • Ambos modelos tuvieron puntuaciones similares en Legibilidad y Fuga de Respuesta (aunque se esperaba una fuga alta en los "pasos finales").
  • La evaluación humana confirmó que LeanTutor es más útil para identificar errores específicos y guiar al estudiante sin dar la respuesta completa inmediatamente.

5. Significado y Futuro

• Validación Pedagógica: El trabajo demuestra que es posible crear tutores de matemáticas que no solo sean conversacionales, sino matemáticamente correctos, mitigando el riesgo de alucinaciones.
• Desafíos Abiertos:
  • La autoformalización fiel sigue siendo difícil debido a las diferencias de granularidad entre el lenguaje natural y el formal.
  • El sistema actual asume la existencia de una solución de referencia formalizada, lo cual puede ser una carga para los instructores.
  • El dataset se limita a aritmética básica; generalizarlo a matemáticas universitarias más complejas (álgebra lineal, cálculo) es el siguiente paso.
• Impacto: LeanTutor abre la puerta a sistemas educativos que utilizan verificadores externos para garantizar la integridad del aprendizaje, un enfoque crucial para cursos donde el razonamiento lógico es el objetivo principal.

En resumen, el paper presenta un prototipo funcional que supera las limitaciones de los LLMs puros en matemáticas mediante la integración con un probador de teoremas, ofreciendo una ruta prometedora para la tutoría de pruebas matemáticas verificada.