Learning to Disprove: Formal Counterexample Generation with Large Language Models

Este artículo presenta un enfoque que utiliza modelos de lenguaje grandes (LLM) ajustados mediante una estrategia de mutación simbólica y un marco de iteración de expertos para generar contraejemplos matemáticos formalmente verificables en Lean 4, abordando así la brecha actual en la investigación sobre razonamiento matemático que se centra casi exclusivamente en la demostración de teoremas.

Lo esencial

Imagina que las matemáticas son como un inmenso juego de construcción de castillos de naipes. Durante años, los mejores "arquitectos" de Inteligencia Artificial (IA) se han dedicado exclusivamente a construir castillos perfectos, demostrando que sus estructuras son sólidas y que las reglas se cumplen.

Pero, ¿qué pasa si alguien intenta construir un castillo que no debería estar de pie? ¿Cómo sabemos que una regla matemática es falsa? Aquí es donde entra el verdadero héroe de esta historia: el destructor de castillos, o en términos matemáticos, el contraejemplo.

Este artículo presenta una nueva IA entrenada no para construir, sino para derribar afirmaciones falsas. Aquí te explico cómo funciona, usando analogías sencillas:

1. El Problema: Solo sabemos construir, no destruir

Hasta ahora, las IAs matemáticas eran como estudiantes que solo sabían aprobar exámenes demostrando que algo es verdad. Si les decías: "Demuestra que todos los cisnes son blancos", la IA intentaba buscar miles de cisnes blancos. Pero si le decías: "Demuestra que la afirmación 'todos los números primos son impares' es falsa", la IA se quedaba atascada. No estaba entrenada para buscar el único cisne negro (el contraejemplo) que destruye la teoría.

Además, había dos grandes obstáculos:

• Falta de libros de texto: No había suficientes ejemplos de "cisnes negros" para enseñarles a la IA.
• Premios invisibles: Si la IA intentaba buscar un contraejemplo y fallaba, no recibía ninguna señal de "correcto" o "incorrecto". Era como jugar a un videojuego donde si pierdes, el juego se apaga y no sabes por qué.

2. La Solución: El "Mutador" de Realidad

Para solucionar la falta de datos, los autores crearon un mutador simbólico. Imagina que tienes una receta de cocina infalible (un teorema probado) que dice: "Si usas harina, huevos Y leche, obtendrás un pastel perfecto".

El mutador toma esa receta y borra un ingrediente (por ejemplo, la leche). Ahora la receta dice: "Si usas harina y huevos, obtendrás un pastel perfecto".

• La magia: Como sabemos que sin leche el pastel no sale bien, la nueva receta es falsa.
• El resultado: La IA ahora tiene un problema nuevo: "Encuentra una mezcla de harina y huevos que no sea un pastel". ¡Esto es un contraejemplo!

Al hacer esto miles de veces con miles de recetas matemáticas, generaron 575,000 nuevos problemas para entrenar a la IA. Es como tener un laboratorio donde crean millones de "trampas" matemáticas para que la IA aprenda a detectarlas.

3. El Entrenamiento: El Sistema de "Doble Premio"

Aquí está la parte más inteligente. Cuando la IA intenta resolver uno de estos problemas (encontrar el cisne negro), a veces se pierde. En el entrenamiento tradicional, si fallaba, recibía cero puntos y se desanimaba.

Los autores crearon un sistema de doble premio:

1. Premio A (El intento): Si la IA encuentra una mezcla que no es un pastel (aunque no sea la perfecta), recibe un pequeño punto. Esto la motiva a seguir intentando.
2. Premio B (La prueba): Si además de encontrar la mezcla, puede escribir la "receta formal" (el código en Lean 4) que demuestra matemáticamente por qué falla, recibe un punto extra.

Es como si en un examen de conducir, si fallas al estacionar pero logras explicar por qué fallaste, el profesor te da medio punto en lugar de cero. Esto mantiene a la IA motivada incluso cuando los problemas son muy difíciles.

4. El Proceso: Dos Pasos (Pensar y Probar)

La IA funciona en dos fases, como un detective:

1. Fase de "Adivinanza" (Informal): El detective piensa en voz alta: "Oye, si quito la leche, el pastel se cae. Probemos con harina y huevos". Propone un ejemplo concreto.
2. Fase de "Prueba" (Formal): El detective escribe un informe legal (código en Lean 4) que demuestra ante un juez (el verificador matemático) que su ejemplo es, de hecho, un cisne negro real.

5. Los Resultados: ¡La IA aprende a dudar!

Al entrenar a la IA con este método, lograron algo increíble:

• La IA ahora es mucho mejor encontrando errores en afirmaciones matemáticas.
• En pruebas contra las mejores IAs actuales, la suya resolvió entre un 47% y un 74% más de problemas de este tipo.
• No solo encuentra el error, sino que puede explicar por qué es un error con una prueba formal impecable.

En resumen

Esta investigación es como enseñar a un estudiante de matemáticas no solo a demostrar que 2+2=4, sino a encontrar rápidamente cuándo alguien dice que 2+2=5 y explicar por qué está equivocado.

Al crear un "laboratorio de errores" (mutación de datos) y un sistema de recompensas inteligente, han creado una IA que no solo cree ciegamente en las reglas, sino que tiene la capacidad crítica de ponerlas a prueba, encontrar sus grietas y derribarlas si es necesario. Es un paso gigante hacia una inteligencia artificial que piensa de verdad, no solo que repite lo que ya sabe.

Resumen técnico

Aquí tienes un resumen técnico detallado del artículo "Learning to Disprove: Formal Counterexample Generation with Large Language Models" en español.

Resumen Técnico: Aprendizaje para Refutar – Generación Formal de Contraejemplos con Modelos de Lenguaje Grandes

1. El Problema

El razonamiento matemático requiere dos habilidades complementarias: construir pruebas rigurosas para afirmaciones verdaderas y descubrir contraejemplos para refutar afirmaciones falsas. Sin embargo, los esfuerzos actuales de la IA en matemáticas se centran casi exclusivamente en la construcción de pruebas, descuidando la tarea crítica de encontrar contraejemplos.

Existen dos desafíos principales que impiden el avance en este campo:

1. Escasez de datos de entrenamiento: No existen conjuntos de datos suficientes para entrenar modelos de lenguaje grandes (LLMs) en la generación de contraejemplos. El único conjunto existente, CounterMath, contiene solo 1,216 problemas en lenguaje natural, insuficientes para el ajuste fino (fine-tuning) de LLMs modernos.
2. Señales de recompensa dispersas: En el aprendizaje por refuerzo, cuando un modelo falla al generar un contraejemplo correcto para un problema complejo, la recompensa desaparece (es cero), lo que estanca el aprendizaje y limita la mejora del modelo.

Además, la generación de contraejemplos difiere de la demostración de teoremas: requiere un paradigma de "adivinar y verificar" (proponer un caso específico y luego verificarlo), en lugar de una deducción lógica lineal.

2. Metodología Propuesta

Los autores proponen un marco integrado que consta de dos etapas principales: Síntesis de Problemas de Contraejemplos y Entrenamiento Guiado por Recompensas Múltiples.

A. Síntesis de Datos mediante Mutación Simbólica
Para abordar la escasez de datos, los autores diseñan una estrategia de mutación simbólica que genera automáticamente miles de problemas de contraejemplos a partir de teoremas existentes:

1. Selección de Semillas: Se recopilan teoremas formalmente demostrables en formato universal ($\forall x, H_1(x) \land H_2(x) \to C(x)$) de bibliotecas formales (Mathlib, LeanWorkbook) y pruebas generadas por LLMs.
2. Mutación: Se elimina una hipótesis necesaria (por ejemplo, $H_1$) del teorema original. Si $H_1$ era esencial, la versión mutada ($H_2(x) \to C(x)$) se vuelve falsa, lo que implica la existencia de un contraejemplo.
3. Formalización del Problema: El problema se reestructura como una búsqueda de un existencial: $\exists x, H_2(x) \land \neg H_1(x)$.
4. Validación: Se utiliza el probador de teoremas Lean 4 para verificar que la hipótesis eliminada es realmente necesaria y que el nuevo problema es sintácticamente correcto.
   • Resultado: Esta estrategia generó 575,000 instancias de contraejemplos a partir de 321,929 teoremas semilla.

B. Entrenamiento con Recompensas Múltiples (Multi-Reward)
Para superar el problema de las recompensas dispersas, se introduce un esquema de recompensa dual basado en la iteración de expertos:

1. Generación: El LLM propone un contraejemplo concreto ($x^*$) y genera dos pruebas formales en Lean 4:
   • Una prueba para la versión mutada (demostrando que $x^*$ satisface las condiciones restantes).
   • Una prueba para la hipótesis descartada (demostrando que $x^*$ viola la hipótesis eliminada, es decir, $\neg H_1(x^*)$).
2. Recompensas: Se calculan dos recompensas binarias basadas en la verificación del probador de teoremas:
   • $r_M$: Recompensa si la prueba de la versión mutada es correcta.
   • $r_H$: Recompensa si la prueba de la hipótesis descartada es correcta.
3. Estrategia: Dado que probar la violación de la hipótesis ($r_H$) es a menudo más fácil que probar la versión mutada completa, esta recompensa secundaria asegura que el modelo reciba señal de aprendizaje incluso cuando falla en la parte más difícil del problema. La recompensa final es una combinación ponderada: $r = \alpha r_M + (1-\alpha)r_H$.

3. Contribuciones Clave

• Nuevo Marco de Entrenamiento: El primer enfoque sistemático para entrenar LLMs específicamente para la generación de contraejemplos formales en Lean 4.
• Estrategia de Mutación Simbólica: Un método automatizado y riguroso para sintetizar datos de entrenamiento masivos y diversos, garantizando la validez lógica de los problemas generados.
• Mecanismo de Recompensa Doble: Una solución innovadora al problema de la dispersión de recompensas en el aprendizaje por refuerzo para tareas matemáticas complejas, permitiendo un entrenamiento más estable y eficiente.
• Benchmarks Nuevos: La creación de tres nuevos conjuntos de pruebas (FOR-COUNTER, VERI-FORMALIZE, VERI-REASON) para evaluar la búsqueda de contraejemplos y la verificación de pasos de razonamiento.

4. Resultados Experimentales

Los experimentos se realizaron en un servidor con 8 GPUs de alto rendimiento, utilizando Qwen3 8B para el razonamiento informal y DeepSeek-Prover-v2 7B para la generación de pruebas formales.

• Eficiencia de Mutación: La estrategia de mutación logró una tasa de mutación entre 1.65 y 2.48 por teorema semilla, con un tiempo de ejecución promedio de 0.3 a 0.71 segundos por teorema.
• Rendimiento de Entrenamiento: El enfoque de recompensas múltiples convergió más rápido y alcanzó un rendimiento superior en comparación con el entrenamiento de recompensa única.
  • En el conjunto de validación, el modelo con recompensas múltiples alcanzó una tasa de éxito Pass@1 del 49.8%, superando a la línea base de recompensa única (43.0%).
• Comparación con el Estado del Arte (SOTA): El modelo ajustado finamente superó significativamente a los modelos de razonamiento propietarios (como GPT-4.1, Gemini-2.5, DeepSeek-R1) y a los probadores de teoremas de código abierto existentes (Leanabell, STP, Goedel).
  • En la tarea de identificación de contraejemplos (FOR-COUNTER), el modelo propuesto resolvió 95 problemas más que la mejor línea base en Pass@1, representando una mejora relativa del 74%.
  • El modelo demostró una capacidad superior tanto en la búsqueda de contraejemplos como en la verificación de resultados autoformalizados y pasos de razonamiento.

5. Significado e Impacto

Este trabajo es fundamental porque:

1. Equilibra el Razonamiento Matemático: Reconoce que la capacidad de refutar (disprovar) es tan crucial como la de probar, llenando un vacío crítico en las capacidades de razonamiento de la IA.
2. Mejora la Fiabilidad del Razonamiento: Entrenar a los LLMs para generar contraejemplos fomenta la auto-verificación y la reflexión sobre los pasos intermedios, reduciendo la confianza en deducciones incorrectas.
3. Herramienta para Matemáticos: Proporciona un "copiloto" práctico para validar conjeturas matemáticas, acelerando la investigación al identificar rápidamente casos límite y excepciones.
4. Escalabilidad: Demuestra que la síntesis de datos simbólica combinada con estrategias de entrenamiento avanzadas puede superar las limitaciones de datos en dominios de alto rigor lógico como las matemáticas formales.

En conclusión, el artículo establece un nuevo estándar para la generación de contraejemplos formales, demostrando que los LLMs pueden aprender a "disprobar" de manera efectiva mediante la combinación de síntesis de datos masiva y esquemas de recompensa inteligentes.