Twitch: Learning Abstractions for Equational Theorem Proving

El artículo presenta Twitch, una herramienta que descubre automáticamente abstracciones (patrones de términos recurrentes) en demostraciones de teoremas para guiar al probador equacional Twee, logrando resolver problemas de igualdad unitaria previamente no resueltos y acelerando significativamente la demostración de otros.

Lo esencial

¡Claro que sí! Imagina que estás intentando resolver un rompecabezas matemático gigante, pero en lugar de piezas de cartón, tienes ecuaciones y símbolos extraños. Eso es lo que hace un proovedor de teoremas automático (como Twee, el protagonista de esta historia).

El problema es que hay tantas combinaciones posibles que el "cerebro" de la máquina se abruma. Es como si intentaras encontrar la salida de un laberinto gigante caminando al azar; podrías tardar años en salir.

Aquí es donde entra Twitch, la nueva herramienta creada por los autores de este artículo. Vamos a explicarlo con una analogía sencilla.

🧠 El Problema: El Laberinto Infinito

Imagina que Twee es un explorador muy rápido, pero un poco tonto. En el laberinto de las matemáticas, cada vez que toma una decisión, genera miles de caminos nuevos. La mayoría son callejones sin salida (ruido).

• Sin ayuda: Twee prueba todo lo que se le ocurre, como si estuviera probando cada puerta de un hotel de 1000 habitaciones sin saber cuál lleva a la salida.
• El resultado: Se gasta mucho tiempo y energía en cosas que no sirven.

💡 La Solución: Twitch y sus "Gafas Mágicas"

Los autores dicen: "¿Y si le enseñamos al explorador a reconocer patrones?".
En lugar de darle una lista de reglas estrictas, crearon Twitch, una herramienta que actúa como un detective de patrones.

Twitch tiene dos formas de aprender a usar sus "gafas mágicas" (que llaman abstracciones):

1. El Detective de Fracasos (Abstracciones de Prueba Parcial)

Imagina que Twee intenta resolver un problema muy difícil y falla después de 5 minutos. Aunque no resolvió el problema, dejó un rastro de "pistas" (ecuaciones intermedias) por el camino.

• Lo que hace Twitch: Revisa ese rastro de fracaso y dice: "¡Espera! En este camino fallido, la forma f(x, x) apareció una y otra vez. ¡Esa forma debe ser importante!".
• La analogía: Es como si un detective revisara un mapa de un viaje fallido y dijera: "Cada vez que intentamos cruzar el río por el norte, nos quedamos atascados en el mismo tipo de roca. Esa roca es clave".
• El resultado: Twitch crea una regla que dice: "Si ves esa forma de roca, ¡fíjate bien! Es probable que sea útil".

2. El Maestro de Escuela (Abstracciones de Dominio)

Esta es la parte más potente. Imagina que quieres aprender a resolver problemas de "Lógica de Grupos".

• Lo que hace Twitch: Primero, le pide a Twee que resuelva problemas fáciles de ese mismo tema. Luego, analiza todas las soluciones exitosas de esos problemas fáciles.
• La analogía: Es como un maestro que dice: "Antes de que intentes el examen final de matemáticas, resuelve estos 50 ejercicios fáciles. Fíjate que en casi todos usamos la misma fórmula para simplificar. ¡Aprende esa fórmula!".
• El resultado: Twitch crea un "resumen" o un atajo mental basado en lo que funcionó en los problemas fáciles, y se lo da al explorador para que lo use en el problema difícil.

⚙️ ¿Cómo funciona la magia? (La Compresión)

Para encontrar estos patrones, Twitch usa una herramienta llamada Stitch (que significa "coser").

• La analogía: Imagina que tienes un texto muy largo y repetitivo: "El gato come el pescado, el perro come el pescado, el pájaro come el pescado".
• Stitch dice: "¡Cosamos esto!". Crea una nueva palabra, digamos ComerPescado(x), y reescribe el texto como: "El gato ComerPescado, el perro ComerPescado, el pájaro ComerPescado".
• En matemáticas: Si el proovedor ve una ecuación gigante, Twitch le dice: "No mires la ecuación entera. Mira solo esta parte que se repite y llámala 'X'. Si ves 'X', es más probable que sea un buen camino".

Esto hace que el proovedor sea más inteligente sin tener que probar millones de caminos inútiles. Le da un "sentido común" matemático.

🏆 Los Resultados: ¿Funciona?

Los autores probaron esto en problemas reales y difíciles (llamados problemas de "calificación 1", que son como los niveles de jefe final en un videojuego).

• Sin Twitch: El proovedor se quedaba atascado o tardaba horas.
• Con Twitch: ¡Resolvió 12 problemas que antes no podía! Y en los que sí podía resolver, lo hizo dos veces más rápido.

🚀 En Resumen

Twitch es como un entrenador que le dice al proovedor de teoremas: "Oye, no intentes adivinar todo. He visto que cuando resuelves problemas similares, siempre usas este patrón específico. Úsalo como una brújula para navegar el laberinto".

En lugar de darle al explorador un mapa completo (que es demasiado grande), le da pistas inteligentes basadas en la experiencia previa, permitiéndole encontrar la salida mucho más rápido y resolver rompecabezas que antes parecían imposibles.

Es un paso gigante hacia que las máquinas no solo "calculen", sino que aprendan a pensar como los matemáticos humanos, buscando patrones y estructuras en lugar de solo fuerza bruta.

Resumen técnico

Resumen Técnico: Twitch - Aprendizaje de Abstracciones para la Demostración de Teoremas Equacionales

1. El Problema

Los demostradores de teoremas automatizados (ATP), especialmente los basados en saturación como Twee (un demostrador de teoremas equacionales), deben navegar por espacios de búsqueda masivos. En un intento de prueba típico, el sistema puede considerar cientos de millones de pares críticos, seleccionando solo unos pocos miles como reglas de reescritura activas y utilizando quizás solo cientos en la prueba final.

El desafío principal es identificar rápidamente qué pares críticos son "interesantes" o prometedores. Las heurísticas actuales de Twee son simplistas, basándose principalmente en el tamaño (peso) de los términos. Aunque estrategias como la de ponderación (weighting) o resonancia permiten a los humanos guiar la búsqueda especificando formas de términos interesantes, esto requiere intervención manual. El objetivo de este trabajo es automatizar el descubrimiento de estas formas de términos interesantes (llamadas abstracciones) para guiar la búsqueda sin intervención humana.

2. Metodología

El sistema propuesto, Twitch, automatiza el descubrimiento de abstracciones utilizando una herramienta llamada Stitch, originalmente diseñada para la síntesis de programas. La metodología se basa en dos enfoques principales para generar abstracciones:

A. Definición de Abstracción:
Una abstracción es un patrón de términos que aparece repetidamente en pruebas relevantes. Formalmente, se busca un conjunto de definiciones de funciones auxiliares que compriman maximamente un conjunto de términos (reduciendo su tamaño). Por ejemplo, si el término $f(x, x)$ aparece frecuentemente, Stitch puede proponer una abstracción $g(x) := f(x, x)$.

B. Dos Modos de Generación:

1. Abstracciones de Prueba Parcial (Partial Proof Abstractions):

   • Se ejecuta Twee en un problema difícil ($P_h$) durante un tiempo limitado. Si falla, se analizan los lemas derivados en el intento fallido.
   • Se seleccionan los lemas más "interesantes" basándose en una métrica heurística: $s(l=r) = \frac{|T(l=r)|}{|l=r|^2}$, donde $|T|$ es la suma de los pesos de todos los términos en la prueba del lema y $|l=r|$ es el peso de la ecuación misma. Esto favorece lemas simples que requieren pruebas largas.
   • Se extraen los términos de estos lemas y se ejecuta Stitch para encontrar patrones comunes.

2. Abstracciones de Dominio (Domain Abstractions):

   • Se utiliza un corpus de problemas "fáciles" (ya resueltos) dentro del mismo dominio teórico.
   • Se generan abstracciones locales para cada problema fácil.
   • Se filtran aquellas que proporcionan una aceleración significativa al re-probar el problema.
   • Finalmente, se ejecuta Stitch sobre el conjunto de abstracciones locales exitosas para encontrar patrones comunes de alto nivel (abstracciones de dominio) que sirvan para guiar la prueba de problemas difíciles en ese mismo dominio. Este enfoque se inspira en el aprendizaje curricular.

C. Integración en Twee:
A diferencia de añadir las abstracciones como nuevos axiomas (lo que expande el espacio de búsqueda y puede causar explosión combinatoria), Twitch integra las abstracciones directamente en la función heurística de Twee.

• Cuando un par crítico coincide con una abstracción, su peso calculado se reduce artificialmente.
• Esto aumenta la probabilidad de que el demostrador seleccione ese par crítico para la siguiente inferencia, sin alterar el espacio de búsqueda subyacente.
• Se permite al usuario ajustar el "peso" de la abstracción (constante o factor de peso) para controlar qué tan agresiva es la guía.

3. Contribuciones Clave

1. Método de Generación Automática: Un enfoque novedoso para extraer abstracciones de intentos de prueba fallidos o de corpus de pruebas exitosas, utilizando Stitch para la compresión de términos.
2. Extensión de Twee: Implementación nativa de soporte para abstracciones en el demostrador equacional Twee, inspirada en la estrategia de ponderación pero sin añadir axiomas definicionales que expandan el espacio de búsqueda.
3. Validación Empírica: Demostración de que estas abstracciones permiten resolver problemas previamente intratables y acelerar significativamente la resolución de problemas estándar.

4. Resultados Experimentales

Los autores evaluaron Twitch en un conjunto de 1041 problemas de igualdad unitaria (UEQ) no satisfacibles del repositorio TPTP v9.2.1, abarcando nueve dominios (Álgebra, Lógica, Teoría de Grupos, Retículos, etc.).

• Problemas Difíciles Resueltos: Twitch permitió a Twee resolver 12 problemas con calificación 1 (los más difíciles, donde el 90% de los demostradores fallan) y un total de 18 problemas difíciles adicionales (rating $\ge$ 0.9).
  • Ejemplo destacado: El problema LAT075-1 (axiomatización del operador NAND/Sheffer stroke), que antes requería ~250 segundos, se resolvió en ~10 segundos con abstracciones de dominio (o ~130s usando solo la heurística de abstracción sin axiomas).
• Mejoras de Rendimiento (Speed-up):
  • La combinación de abstracciones de dominio y la estrategia de aplanamiento de objetivos (goal flattening) redujo el tiempo de ejecución a la mitad para problemas que Twee ya podía resolver, y resolvió aproximadamente 25 problemas más dentro del límite de 300 segundos.
  • Las abstracciones de prueba parcial mostraron mejoras menores pero útiles, especialmente cuando no hay problemas relacionados previos.
• Comparación con Axiomas Definicionales:
  • Se comparó el uso de abstracciones como guías heurísticas frente a su adición como axiomas. El enfoque de abstracción (guía heurística) resultó más robusto: añadir muchos axiomas causó tiempos de espera (timeouts) frecuentes, mientras que el uso de abstracciones permitió incluir más patrones sin degradar el rendimiento.

5. Significado y Conclusión

El trabajo demuestra que el aprendizaje automático de patrones sintácticos (abstracciones) a partir de la estructura de las pruebas es una estrategia viable y potente para la demostración de teoremas equacionales.

• Interpretabilidad: A diferencia de los modelos de aprendizaje profundo que actúan como "cajas negras", las abstracciones descubiertas por Twitch son patrones sintácticos explícitos y comprensibles (ej. $f(x,x)$ representando la negación), lo que facilita la integración en sistemas formales.
• Eficiencia: Al evitar la expansión del espacio de búsqueda (no añadiendo axiomas), se logra una guía eficiente que acelera la búsqueda sin los riesgos de la saturación excesiva.
• Futuro: El sistema sugiere que la curación de dominios de problemas y la combinación de abstracciones parciales y de dominio son direcciones prometedoras. Además, se identifica la necesidad de mejorar la robustez de la implementación frente a la reescritura de términos que podrían destruir las abstracciones.

En resumen, Twitch cierra la brecha entre la intuición humana (saber qué formas de términos son importantes) y la automatización, permitiendo a los demostradores equacionales aprender de sus propios éxitos y fracasos para resolver problemas matemáticos complejos de manera más eficiente.