A method for the automated generation of proof exercises with comparable levels of proving complexity

Este artículo presenta un método automatizado para generar ejercicios de demostración matemática con niveles de complejidad comparables, utilizando pruebas de tablaux basadas en reglas extraídas mecánicamente para controlar la dificultad en cursos de matemáticas discretas.

Lo esencial

Imagina que eres un profesor de matemáticas. Tu trabajo no es solo dar clases, sino también crear cientos de ejercicios para que tus alumnos practiquen. Diseñar un buen problema de demostración (como probar que un conjunto está incluido en otro) es como escribir una receta de cocina perfecta: tiene que ser lo suficientemente difícil para que el alumno piense, pero no tan difícil que se rinda.

El problema es que crear estos ejercicios manualmente consume muchísimo tiempo. Si quieres que todos los alumnos tengan ejercicios de la misma dificultad, tienes que ser un experto en estimar cuánto esfuerzo mental requiere cada uno.

Este paper presenta una solución automática: un "robot" que crea ejercicios de demostración matemática que son igualmente difíciles entre sí.

Aquí te explico cómo funciona, usando analogías sencillas:

1. El problema: ¿Qué significa "igual dificultad"?

En el pasado, los intentos de automatizar esto fallaban porque medían la dificultad de forma superficial.

• El error: Decir "este problema es difícil porque tiene 5 símbolos" o "porque es largo".
• La realidad: Dos problemas pueden tener la misma longitud, pero uno puede ser un laberinto simple y el otro un laberinto con trampas ocultas. La dificultad real está en cómo se resuelve, no en cómo se ve.

2. La solución: El "Esqueleto del Pensamiento"

Los autores proponen no mirar el problema, sino mirar el esqueleto de la solución.

Imagina que cada ejercicio de demostración es un edificio.

• La dificultad no depende de qué color tenga la fachada (los símbolos matemáticos), sino de cuántos pisos tiene el edificio y cómo están conectados los ascensores.
• Para medir esto, el sistema usa una herramienta llamada "Tableros de Corte" (Cut-based Tableaux).

La analogía del "Corte":
Piensa en un tablero de ajedrez. Para ganar, no puedes moverte al azar; debes seguir reglas estrictas. El sistema de los autores crea un "tablero" donde cada movimiento (paso de la demostración) está estrictamente controlado.

• Si el "edificio" de la solución tiene 3 pisos y 2 ascensores, es un ejercicio de nivel "medio".
• Si otro ejercicio también tiene un edificio de 3 pisos y 2 ascensores, es automáticamente de la misma dificultad, aunque los materiales (los números o letras) sean diferentes.

3. ¿Cómo crea el robot ejercicios nuevos? (La Máquina de Copiar Estructuras)

El proceso tiene dos pasos mágicos:

Paso A: Encontrar la "Huella Digital" del ejercicio original.
El sistema toma un ejercicio que tú ya sabes que es bueno (por ejemplo, "Demuestra que A intersectado con B está dentro de A").

• Construye la solución paso a paso.
• Mide la "estructura" de esa solución: ¿Cuántos pasos? ¿Qué tipo de reglas se usaron?
• Esto crea una plantilla de dificultad.

Paso B: La "Máquina de Cambiar Piezas".
Aquí es donde ocurre la magia. El sistema tiene un banco de piezas (símbolos matemáticos como "unión", "intersección", "pertenencia").

• Toma la plantilla del ejercicio original.
• Empieza a cambiar las piezas, pero solo si la estructura del edificio se mantiene igual.
• Ejemplo: Si en el original usaste "Intersección" (∩) en un paso clave, el sistema puede cambiarla por "Diferencia" () o "Unión" (∪), siempre y cuando la lógica interna del edificio no colapse ni se haga más grande.

Es como si tuvieras un Lego. Si tienes una torre de 5 bloques, puedes cambiar el bloque rojo por uno azul, o el cuadrado por uno triangular, pero la torre seguirá teniendo 5 bloques de altura. La dificultad (altura) se mantiene, pero el ejercicio (color/forma) es nuevo.

4. ¿Por qué es genial esto?

• Para el profesor: Ya no tienes que pasar horas inventando problemas. Le das un ejemplo y el sistema te devuelve 50 ejercicios nuevos que son "gemelos" en dificultad.
• Para el alumno: Todos reciben ejercicios que son justos. No hay quien tenga suerte con un problema fácil y quien tenga mala suerte con uno imposible.
• La precisión: A diferencia de los sistemas de Inteligencia Artificial que adivinan la dificultad basándose en lo que dicen los humanos (que a veces se equivocan), este sistema calcula la dificultad basándose en la lógica pura. Es como medir la distancia con una regla en lugar de estimarla con la vista.

En resumen

Este paper presenta un arquitecto automático para matemáticas. En lugar de construir edificios desde cero (crear ejercicios desde cero), toma la estructura de un edificio existente (un ejercicio de demostración) y genera nuevas versiones del mismo edificio usando diferentes materiales, garantizando que todos tengan exactamente la misma complejidad estructural.

Esto permite a los educadores llenar sus clases con ejercicios personalizados, justos y de calidad, sin perder horas de su vida diseñándolos uno por uno.

Resumen técnico

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

Resumen Técnico: Generación Automatizada de Ejercicios de Prueba con Niveles Comparables de Complejidad

1. El Problema

La generación automática de preguntas (AQG, por sus siglas en inglés) es una herramienta prometedora para reducir la carga laboral de los educadores en el diseño de ejercicios. Sin embargo, existe una barrera significativa para su adopción en entornos pedagógicos formales, especialmente en lógica y matemáticas: la falta de control granular sobre la dificultad de los ejercicios generados.

• Limitaciones de enfoques existentes: Los métodos actuales suelen basarse en la estructura sintáctica de las fórmulas (número de conectivos, profundidad) o en modelos de aprendizaje automático que clasifican la dificultad basándose en juicios humanos.
  • Los enfoques sintácticos fallan porque dos fórmulas con la misma estructura pueden requerir estrategias de prueba muy diferentes.
  • Los enfoques basados en aprendizaje automático carecen de explicabilidad y pueden ser inconsistentes debido a la subjetividad de los expertos.
• Necesidad: Se requiere un método que genere ejercicios de prueba (conjeturas demostrables) donde la "complejidad de la prueba" sea comparable y controlable, basándose en el esfuerzo real necesario para resolverlos, no solo en su apariencia superficial.

2. Metodología

El artículo propone un método para generar ejercicios de prueba en lenguajes de primer orden (típicos de cursos de Matemática Discreta) que comparten un nivel de complejidad de prueba comparable. La metodología se basa en tres pilares fundamentales:

A. Pruebas Específicas de la Teoría (Theory-Specific Proofs)
En lugar de usar lógica formal estándar con símbolos lógicos ($\neg, \land, \forall$, etc.), el método utiliza tablas analíticas basadas en cortes (cut-based tableaux) donde las fórmulas son "específicas de la teoría" (fórmulas atómicas sin conectivos lógicos ni cuantificadores).

• Extracción de Reglas: A partir de un conjunto de axiomas definicionales de una teoría (ej. Teoría de Conjuntos), se extraen reglas de expansión lineales. Estas reglas se obtienen transformando los axiomas a una Forma Normal Implicacional de Reglas (RINF).
• Restricciones Analíticas: Las reglas extraídas deben cumplir restricciones para garantizar la reducción de complejidad:
  1. Las variables en la conclusión deben estar presentes en las premisas.
  2. El símbolo predicado en la conclusión debe ser "menor" (según una relación bien fundamentada) que en las premisas.
  3. Si los predicados son iguales, la profundidad de la fórmula en la conclusión debe ser menor.

B. Definición de Complejidad de Prueba
La complejidad no se mide por el tamaño de la fórmula, sino por la estructura deductiva de la prueba mínima.

• Isomorfismo Deductivo: Dos ejercicios tienen complejidad comparable si sus pruebas mínimas son deductivamente isomórficas. Esto significa que sus "árboles de justificación" (la estructura de cómo se cierran las ramas de la tabla) son isomórficos y preservan la isomorfía sintáctica de las fórmulas.
• Tamaño Deductivo: Se define como la suma de los nodos en los árboles de justificación de todas las ramas de una prueba.

C. Procedimiento de Generación
El algoritmo de generación opera en dos pasos principales:

1. Búsqueda de Pruebas Mínimas: Dado un ejercicio de entrada, el sistema construye tablas de expansión iterativamente ($T_1, T_2, \dots$) hasta encontrar las pruebas mínimas (aquellas con el menor tamaño deductivo posible).
2. Búsqueda de Conjuntos Isomórficos: El sistema busca otros conjuntos de fórmulas firmadas que posean una prueba mínima deductivamente isomorfa a la del ejercicio original.
   • Para ello, utiliza el concepto de símbolos de coincidencia deductiva: identifica qué símbolos (predicados o funciones) en una fórmula pueden ser reemplazados por otros símbolos de la misma teoría sin alterar la estructura de la prueba.
   • Esto permite generar nuevas variantes de ejercicios (ej. cambiar $\cap$ por $\cup$ o $\setminus$) que mantienen la misma dificultad estructural.

3. Contribuciones Clave

• Marco de Complejidad Basado en la Estructura de la Prueba: Propone una métrica de dificultad objetiva y explicativa basada en la isomorfía de las pruebas mínimas, superando las limitaciones de los enfoques puramente sintácticos o estadísticos.
• Método de Extracción de Reglas Específicas de la Teoría: Introduce un procedimiento mecanizable para convertir axiomas de teorías matemáticas (como Teoría de Conjuntos o Teoría de Números) en reglas de tabla sin símbolos lógicos, facilitando el análisis estructural.
• Algoritmo de Generación de Ejercicios: Desarrolla un procedimiento computacional que, dado un ejercicio de ejemplo, genera automáticamente un conjunto de ejercicios nuevos con complejidad de prueba garantizada como comparable.
• Herramienta Prototipo: Se ha implementado un prototipo disponible públicamente (GePECC) que demuestra la viabilidad del enfoque.

4. Resultados y Validación

• Ejemplo de Teoría de Conjuntos: El método se aplicó exitosamente a un fragmento de la Teoría de Conjuntos. Se demostró que ejercicios como "Probar que $x \in y \cap (w \cup z) \implies x \in (y \cap w) \cup z$" y "Probar que $x \in y \setminus (w \triangle z) \implies x \in (y \setminus w) \cup z$" tienen la misma complejidad de prueba, a pesar de usar operadores diferentes.
• Reducción del Espacio de Búsqueda: El uso de "símbolos de coincidencia deductiva" reduce drásticamente el espacio de búsqueda de candidatos. En el ejemplo presentado, la búsqueda se redujo en un factor de ~40 veces al restringir los reemplazos válidos.
• Generación de Ejercicios: El sistema generó múltiples variantes de ejercicios que son estructuralmente equivalentes en términos de esfuerzo de resolución, validando la capacidad del método para producir materiales educativos consistentes.

5. Significado e Impacto

• Pedagogía en Matemáticas y Lógica: Ofrece a los educadores una herramienta para crear bancos de ejercicios personalizados y adaptativos. Permite asignar problemas de dificultad controlada a estudiantes con diferentes niveles de dominio, evitando la injusticia de asignar ejercicios más fáciles a algunos y más difíciles a otros sin criterio.
• Evaluación Adaptativa Computarizada: Facilita el desarrollo de sistemas de evaluación que seleccionan preguntas basándose en el rendimiento previo del estudiante, asegurando que los saltos de dificultad sean manejables y medibles.
• Explicabilidad: A diferencia de las "cajas negras" del aprendizaje automático, este método ofrece una justificación formal de por qué dos ejercicios tienen la misma dificultad (isomorfía de sus pruebas mínimas), lo cual es crucial para la confianza en sistemas educativos automatizados.
• Futuro: El trabajo abre la puerta a investigar cómo ciertas características estructurales (como el uso de reglas de múltiples premisas) afectan la percepción de dificultad por parte de los estudiantes, refinando aún más el modelo de complejidad.

En resumen, el artículo presenta un avance significativo en la automatización educativa al vincular la dificultad de los ejercicios matemáticos con la estructura formal de sus soluciones, proporcionando un método riguroso y automatizable para la generación de material didáctico de calidad.