🤖 AI

ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction

El artículo presenta ALPS, un nuevo referente que mide rigurosamente la creatividad válida en los modelos de lenguaje de gran tamaño al encomendarles la generación de pruebas matemáticas o construcciones originales y verificables para leyes ecuacionales generadas aleatoriamente, revelando que los modelos actuales tienen dificultades significativas con el lado de la construcción y que la mayoría de las instancias permanecen sin resolver incluso por demostradores automáticos avanzados.

Autores originales: Eric Xie, Wenqian Ye, Aidong Zhang

Publicado 2026-08-18

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Eric Xie, Wenqian Ye, Aidong Zhang

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

En el panorama científico moderno, la inteligencia artificial ha comenzado a dar un paso más allá del papel de procesador de datos para entrar en el papel de descubridor. Estamos viendo máquinas que pueden proponer nuevos compuestos químicos, sugerir materiales novedosos e incluso formular conjeturas matemáticas que los humanos aún no han considerado. Este cambio plantea una pregunta profunda: cuando una máquina produce una respuesta que parece un avance, ¿cómo sabemos si es verdaderamente creativa y no solo una repetición ingeniosa de algo que memorizó durante su entrenamiento? La verdadera creatividad en la ciencia requiere dos cosas: la solución debe ser original, lo que significa que no se ha visto antes, y debe ser efectiva, lo que significa que realmente funciona y resuelve el problema en cuestión. La dificultad radica en verificar estas cualidades. En muchos campos, juzgar si una nueva idea es válida requiere que expertos humanos examinen el resultado y decidan si es bueno, un proceso que es lento y subjetivo. En las matemáticas, donde las respuestas pueden verificarse con absoluta certeza, el desafío es diferente: los problemas suelen ser tan complejos que una computadora no puede simplemente buscar a través de cada posibilidad para encontrar la respuesta, y los problemas en sí mismos son a menudo conjuntos fijos que la máquina podría haber estudiado ya.

Para resolver este dilema, investigadores de la Universidad de Virginia han desarrollado una nueva forma de probar la inteligencia artificial, un referente que llaman ALPS. Este sistema está diseñado para medir la "creatividad válida" presentándole a la máquina un tipo específico de acertijo matemático que no puede resolverse mediante la memoria o siguiendo una rutina estándar. Los acertijos se basan en reglas sobre cómo se pueden combinar un conjunto de elementos. Imagine una colección de objetos y una regla para mezclar cualquiera de ellos entre sí. Los investigadores generan una regla específica, o ley, que describe cómo deben comportarse estos objetos. La tarea de la máquina es decidir una de dos cosas: o bien la regla es tan restrictiva que obliga a que todos los objetos sean idénticos, o la regla permite una estructura compleja e infinita de objetos que satisfaga la condición. Si la máquina afirma que la estructura existe, debe construir una descripción de la misma. Si afirma que los objetos deben ser idénticos, debe demostrar que no existe otra posibilidad. La brillantez de esta configuración es que las respuestas pueden ser verificadas por una computadora con perfecta exactitud, sin necesidad de que ningún humano examine el resultado. Además, el sistema puede generar un suministro infinito de estos acertijos, asegurando que la máquina siempre se enfrente a un problema que no ha visto antes.

Los investigadores probaron este sistema utilizando una variedad de potentes herramientas de razonamiento automatizado, que son programas informáticos especializados diseñados para resolver problemas lógicos. Ejecutaron estas herramientas contra un grupo de más de cuatro mil de estas leyes generadas. Los resultados fueron contundentes. Incluso con un aumento masivo de la potencia de cómputo, las herramientas automatizadas solo pudieron resolver una fracción minúscula de los problemas. Específicamente, un portafolio de ocho configuraciones diferentes de los mejores probadores disponibles logró resolver solo alrededor del dos por ciento de las leyes. Cuando los investigadores aumentaron el presupuesto de computación veinte veces, encontraron solo un puñado de soluciones adicionales, y ninguna de ellas eran las estructuras complejas que buscaban; solo eran demostraciones de que los objetos tenían que ser idénticos. Esto sugiere que la barrera para resolver estos problemas no es la falta de potencia de cómputo, sino la falta de un método para inventar las estructuras específicas y personalizadas que cada ley única requiere. La máquina simplemente no sabe cómo construir la estructura infinita adecuada desde cero.

Los investigadores dirigieron entonces su atención hacia los modelos de lenguaje de gran tamaño, el tipo de inteligencia artificial que impulsa muchas de las herramientas conversacionales utilizadas hoy en día. Probaron los modelos de razonamiento más potentes disponibles, dándoles los mismos acertijos y la misma oportunidad de probar sus respuestas. En el lado de la tarea donde la máquina tenía que demostrar que todos los objetos eran idénticos, el mejor modelo tuvo éxito en aproximadamente el catorce por ciento de los casos, pero solo en los problemas más simples. En el lado donde la máquina tenía que construir una nueva estructura infinita, los resultados fueron aún más reveladores: ninguno de los modelos tuvo éxito. Cuando los modelos intentaban construir una estructura, fallaban consistentemente de una de dos maneras. O bien proponían una estructura demasiado rígida, colapsando todos los objetos en un solo punto y fallando así en mostrar una solución compleja, o proponían una estructura demasiado laxa, que no seguía las reglas de la ley que intentaban satisfacer. En cada instancia, la máquina no pudo equilibrar la necesidad de seguir las reglas con la necesidad de crear algo nuevo y complejo.

El estudio concluye que, si bien estos sistemas de inteligencia artificial están mejorando en su capacidad para seguir instrucciones y revisar su propio trabajo, todavía luchan con el acto central del descubrimiento científico: inventar una nueva estructura que se ajuste a un conjunto de restricciones. Los investigadores han hecho público todo su sistema, incluyendo el generador que crea los acertijos y el juez automatizado que verifica las respuestas. Esto permite que otros científicos continúen probando y mejorando estos modelos sin quedarse sin problemas frescos. Los hallazgos sugieren que el camino a seguir para la IA en la ciencia puede no consistir en darles a las máquinas más datos o más tiempo, sino en enseñarles cómo proponer y refinar sus propias ideas en un ciclo de creación y verificación. Hasta que las máquinas puedan construir de manera confiable estas soluciones personalizadas, su papel en el descubrimiento científico seguirá siendo limitado, incapaces de cruzar la brecha entre el procesamiento de información y la generación de conocimiento verdaderamente válido y original.

Resumen Técnico: ALPS – Midiendo la Creatividad Válida en Modelos de Lenguaje de Gran Escala mediante Construcción Matemática

1. Planteamiento del Problema

Las evaluaciones actuales de los Modelos de Lenguaje de Gran Escala (LLM) en dominios científicos (p. ej., demostración de teoremas, diseño de moléculas) tienen dificultades para distinguir entre la creatividad válida y la mera memorización o ejecución rutinaria. Una solución se considera "válidamente creativa" solo si satisface dos criterios conjuntos:

Originalidad: La solución no es una repetición de los datos de entrenamiento o de un procedimiento general conocido.
Efectividad: La solución es objetivamente correcta y aporta valor para la tarea específica.

Los benchmarks existentes no logran medir esta combinación de manera fiable porque carecen de al menos una de las tres propiedades necesarias:

Verificabilidad: Las soluciones deben ser objetivamente comprobables (no sujetas a juicio subjetivo).
Renovabilidad: Se deben poder generar nuevos casos de problemas sin límite para evitar la contaminación de los datos de entrenamiento.
Constructividad: La tarea debe requerir una solución adaptada al caso específico, evitando soluciones mediante memoria o algoritmos estándar.

Los corpora estáticos (p. ej., MATH, miniF2F) fallan en la renovabilidad; los acertijos sintéticos (p. ej., SAT aleatorios) suelen fallar en la constructividad, ya que pueden resolverse mediante procedimientos conocidos; y las tareas de descubrimiento abierto (p. ej., diseño de moléculas) suelen fallar en la verificabilidad debido al juicio humano subjetivo.

2. Metodología: El Benchmark ALPS

Los autores presentan ALPS (Austin-Law Proof-Synthesis), un benchmark diseñado para cumplir con las tres propiedades simultáneamente dentro del dominio de la teoría ecuacional.

Formulación del Problema:

Dominio: ALPS opera sobre magmas (conjuntos con una operación binaria única $\diamond$ ) y leyes ecuacionales (identidades cuantificadas universalmente).
Tarea: Cada instancia es una ley $L$ de la forma $x = T[x, y, z, \dots]$ , donde $T$ es un término de orden cinco o superior.
La Dicotomía: Para cualquier ley de este tipo, se cumple exactamente una de dos condiciones:
1. Trivial: La ley implica $x = y$ , colapsando todo modelo a un único elemento.
2. Austin: La ley tiene un modelo no trivial, el cual debe ser necesariamente infinito (ya que todos los modelos finitos no triviales son descartados por el proceso de certificación del benchmark).
El Desafío: El solver debe proporcionar una prueba deductiva de que $L \models x=y$ (lado Trivial) o construir un magma infinito que satisfaga $L$ (lado Austin).

Construcción del Corpus:

Generación: El corpus se expande mediante un motor de extensión. Partiendo de leyes Austin conocidas, las variables en el término $T$ se reemplazan recursivamente con nuevas operaciones (p. ej., $v \to v \diamond w$ ). Esto asegura que se puedan generar problemas nuevos e inéditos indefinidamente.
Filtrado y Admisibilidad: Los candidatos pasan por un riguroso proceso de filtrado:
1. Filtro de Modelo Finito: Descarta leyes con modelos finitos no triviales.
2. Probadore de Admisibilidad: Utiliza probadores automáticos para certificar que no existe un modelo finito no trivial. Esto se basa en una consecuencia lógica de la finitud: en un conjunto portador finito, una aplicación inyectiva es sobreyectiva. El probador intenta derivar una contradicción de la ley y la suryectividad de un subtérmino, certificando que cualquier modelo debe ser infinito.
3. Deduplicación: Las leyes equivalentes (mutuamente implicantes) se agrupan en clases de equivalencia para asegurar recuentos de problemas distintos.
Pool Resultante: A partir de una generación inicial de candidatos, los autores produjeron un grupo de 4,141 leyes no resueltas (el "nivel difícil") y un conjunto más pequeño de leyes "certificadas como fáciles".

Verificación de Respuestas (El Juez Automatizado):
El juez verifica las entregas a través de dos canales distintos, totalmente automatizados y sin intervención humana:

Lado Trivial: El LLM envía una cadena de igualdades. Un entorno de ejecución (harness) la formaliza automáticamente en una prueba de Lean (verificada por el núcleo de Lean) para comprobar que $L \implies \forall a, b: a=b$ .
Lado de Construcción: El LLM envía un conjunto finito de ecuaciones $E$ $E$ (una presentación). El juez verifica dos afirmaciones utilizando probadores de teoremas automatizados (p. ej., Vampire, E, Twee):
- Derivación: $E \vdash L$ (Cada modelo de $E$ satisface $L$ ).
- Satisfacibilidad: $E \cup \{a \neq b\}$ es satisfacible (Existe un modelo de $E$ con al menos dos elementos distintos).
- Si ambas se cumplen, el certificado de admisibilidad de la instancia garantiza que el modelo es infinito.

3. Contribuciones Clave

Una Tarea de Construcción de Dos Lados: Un benchmark donde cada instancia está certificada para tener una respuesta determinada (o bien trivial o bien infinita), aislando la necesidad de construcción creativa.
Corpus Renovable y Generador: Un generador público que crea instancias frescas sin límite, asegurando que la evaluación nunca sea contaminada por los datos de entrenamiento.
Juez Automatizado: Un sistema que certifica las entregas mediante canales independientes (Lean para la trivialidad, certificados de probadores automáticos para la construcción) sin jueces humanos.
Línea Base Automatizada Fuerte: Un portafolio de ocho configuraciones de los principales probadores (Vampire, E, Twee) que establece el límite "limitado por el método" de la automatización actual.

4. Resultados Experimentales

Rendimiento de los Probadores Automatizados:

Un portafolio de ocho configuraciones resolvió solo el 2.2% del pool de evaluación de 4,141 leyes.
Aumentar el presupuesto de cómputo por un factor de 20 añadió solo un 0.6% más de leyes resueltas (todas pruebas de trivialidad, ninguna nueva modelo).
El 97.2% del pool permanece sin resolver por cualquier configuración probada, lo que indica que el obstáculo es la ausencia de métodos para construir estructuras infinitas a medida, no la falta de cómputo.
Hallazgo secundario: Los autores resolvieron una ley de orden 5 que había quedado abierta por el Proyecto de Teorías Ecuacionales (ETP), confirmando la existencia de un modelo infinito mediante saturación.

Rendimiento de los LLM:

Lado Trivial: En un conjunto de 63 leyes "certificadas como fáciles", el modelo más fuerte probado (o3) alcanzó una tasa de éxito del 14% (9 soluciones) con waypoints (lemmas derivados por el probador) y un 9.5% sin ellos. GPT-4.1 y o4-mini obtuvieron un 0%.
- Modo de Fallo: Los LLM fallaron principalmente al enviar cadenas que contenían pasos inválidos (pasos no derivables de la ley), los cuales fueron rechazados por el entorno de ejecución.
Lado de Construcción: En una muestra de 25 leyes de "nivel difícil" (no resueltas por la automatización), ningún LLM produjo una solución verificada.
- Modo de Fallo: Las entregas eran demasiado fuertes (implicaban la ley pero colapsaban a un solo elemento, fallando la comprobación de distinción) o demasiado débiles (permitían elementos distintos pero no lograban implicar la ley). o3 superó exactamente uno de los dos controles en todas las 25 leyes. o4-mini y GPT-4.1 fallaron ambos controles en muchas leyes.

5. Significado y Reivindicaciones

El artículo afirma que ALPS logra aislar la creatividad válida al eliminar los factores de confusión de la memorización y la ejecución rutinaria.

Necesidad de Creatividad: La alta tasa de fallo tanto de los probadores automatizados como de los LLM en el "nivel difícil" demuestra que estos problemas no pueden resolverse mediante procedimientos generales existentes o búsqueda de fuerza bruta.
Naturaleza del Fallo: Los perfiles de fallo específicos (pasos inválidos en pruebas de trivialidad; presentaciones "demasiado fuertes/débiles" en la construcción) resaltan que los modelos actuales luchan con la generación creativa bajo restricciones. A menudo pueden redactar una estructura, pero fallan al equilibrar las especificaciones globales sin colapsar en soluciones degeneradas.
Paralelo Científico: El artículo traza un paralelo con el ciclo "especificar–construir–verificar" en el descubrimiento científico (p. ej., diseño de moléculas), señalando que ALPS hace que cada fase sea comprobable por máquina.
Dirección Futura: Los autores sugieren que el camino a seguir reside en los bucles de verificar-y-refinar (similares a la Síntesis Inductiva Guiada por Contraejemplos, CEGIS), donde los solvers redactan estructuras, reciben retroalimentación automatizada sobre su validez y las revisan.

Los autores mantienen la modestia, señalando que aunque los LLM más fuertes muestran cierta capacidad en instancias fáciles, actualmente fallan al construir estructuras infinitas válidas en instancias difíciles, y que el benchmark permanece mayoritariamente sin resolver por la tecnología actual.