🤖 AI

From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates

Este artículo presenta NSPI, un marco neuro-simbólico que aprovecha los modelos de lenguaje grandes para proponer conjeturas aproximadas de suma de cuadrados y el cálculo simbólico para refinarlas en pruebas exactas verificadas por máquina en Lean, logrando así una demostración automatizada escalable de desigualdades polinómicas con hasta 10 variables.

Autores originales: Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

Publicado 2026-05-18

📖 4 min de lectura☕ Lectura para el café

CC BY 4.0

Autores originales: Ruobing Zuo, Hanrui Zhao, Gaolei He, Zhengfeng Yang, Jianlin Wang

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

Imagina que intentas demostrar que un pastel complejo, de múltiples capas, siempre es "suficientemente dulce" (matemáticamente, no negativo) sin importar cómo lo cortes o cambies los ingredientes. En el mundo de las matemáticas, esto se llama demostrar una desigualdad polinómica.

Durante mucho tiempo, los matemáticos han tenido dos formas principales de hacer esto, pero ambas han tenido defectos importantes:

El Método de "Lógica Pura" (Simbólico): Esto es como intentar resolver el problema del pastel escribiendo cada reacción química individual de los ingredientes en una pizarra. Es perfectamente preciso, pero si el pastel tiene demasiados ingredientes (variables), la pizarra se llena instantáneamente y el método colapsa. Es demasiado lento y desordenado para problemas grandes.
El Método de "Adivinanzas de IA" (LLMs): Esto es como pedirle a un chef muy inteligente y creativo que adivine la receta. El chef es rápido y bueno con pasteles pequeños, pero cuando el pastel se vuelve enorme y complicado, el chef empieza a alucinar ingredientes que no existen o a cometer errores matemáticos. No pueden probar que su respuesta es 100% verdadera.

Este artículo introduce un nuevo equipo llamado NSPI (Demostración de Desigualdades Polinómicas Neuro-Simbólica). Piensa en NSPI como una asociación perfecta entre un chef creativo y un inspector de calidad riguroso.

Así es como funciona su "línea de montaje", paso a paso:

Paso 1: El Chef Creativo (El LLM)

Primero, el equipo le pide a un Modelo de Lenguaje Grande (el "Chef") que examine un problema matemático difícil. El Chef no intenta hacer las matemáticas difíciles de inmediato. En su lugar, usa su creatividad para adivinar una estructura.

La Analogía: Imagina que el Chef dice: "Apuesto a que este pastel está hecho de tres capas específicas de cubos de azúcar apilados juntos".
En términos matemáticos, el LLM adivina una descomposición Suma de Cuadrados (SOS). Sugiere: "Esta expresión complicada probablemente sea solo la suma de algunas cosas más simples elevadas al cuadrado".
Punto Crucial: La conjetura del Chef suele ser una aproximación. Está cerca, pero podría tener pequeños errores decimales (como decir que un cubo de azúcar pesa 1.0000001 gramos en lugar de exactamente 1).

Paso 2: El Inspector de Calidad (Corrección Simbólica)

La conjetura del Chef se pasa al "Inspector de Calidad", que es un potente sistema de álgebra computacional.

La Analogía: El Inspector toma el boceto aproximado del Chef y usa un microscopio para corregir los pequeños errores. Utiliza una técnica llamada Método de Newton (una forma matemática de hacer zoom en la respuesta exacta) y Recuperación Racional (convertir decimales desordenados en fracciones limpias y exactas).
Si el Chef adivinó que las capas eran "aproximadamente" 1.5, 2.3 y 0.7, el Inspector calcula los números exactos: 3/2, 23/10 y 7/10.
Ahora, la conjetura se ha convertido en un certificado matemático perfecto y exacto.

Paso 3: El Juez del Tribunal (Verificación Lean)

Finalmente, el equipo lleva este certificado exacto a un "Juez" llamado Lean.

La Analogía: Lean es un juez estricto e inmutable que verifica cada paso del trabajo del Inspector. No le importan las "sensaciones" ni las "adivinanzas". Solo acepta pruebas que sean lógicamente a prueba de fallos.
Debido a que el Inspector proporcionó un certificado exacto, el Juez puede verificar fácilmente: "Sí, si elevas al cuadrado estos números exactos y los sumas, obtienes el pastel original. Y como los cuadrados son siempre positivos, el pastel siempre es dulce".
El Juez luego emite una prueba verificada por máquina que está garantizada al 100% como correcta.

¿Por qué es esto un gran logro?

El artículo probó a este equipo en 522 problemas matemáticos muy difíciles, algunos con hasta 10 variables diferentes (ingredientes).

Los Métodos de Lógica Antiguos se rendían cuando los problemas se volvían demasiado grandes (demasiados ingredientes).
Los Métodos de IA Antiguos se confundían y cometían errores en los problemas grandes.
El Equipo NSPI tuvo éxito donde otros fallaron. Podían resolver problemas con 10 variables que ningún otro método podía tocar.

La Conclusión

El artículo afirma que al permitir que una IA adivine la forma de la solución y luego usar herramientas matemáticas para corregir los detalles y una computadora para verificar la verdad, han construido un sistema que puede resolver problemas complejos de desigualdades más rápido y de manera más confiable que nunca antes. No solo adivinaron; construyeron un puente desde una "buena conjetura" hasta un "hecho demostrado".

Lo que NO afirmaron:

No dijeron que esto curará enfermedades o predecirá el mercado de valores.
No afirmaron que esto funciona para cada tipo de problema matemático, solo para demostrar que ciertas expresiones polinómicas son siempre positivas.
No afirmaron que esto reemplace a los matemáticos humanos por completo, sino que automatiza un tipo de razonamiento muy específico y difícil.

Resumen Técnico: De Conjeturas Generadas por LLM a Formalizaciones en Lean

Enunciado del Problema

La demostración automatizada de desigualdades polinómicas es un desafío fundamental en el razonamiento matemático, particularmente para casos de alta dimensionalidad y multivariados. Los enfoques existentes enfrentan limitaciones significativas de escalabilidad:

Métodos Puramente Simbólicos: Aunque proporcionan garantías sólidas, los métodos basados en la descomposición de Suma de Cuadrados (SOS) y la Programación Semidefinida (SDP) sufren de explosión combinatoria y un crecimiento rápido en las expresiones intermedias a medida que aumenta el número de variables o el grado. A menudo fallan al producir pruebas estructuradas y legibles por humanos.
Métodos Puramente Basados en LLM: Los Modelos de Lenguaje Grande (LLM) integrados con asistentes de prueba (por ejemplo, Lean, Isabelle) han mostrado promesa, pero están limitados por la escasez de datos de entrenamiento formalizados de alta calidad. Tienen dificultades con desigualdades algebraicas complejas, particularmente aquellas que exceden 5 variables, y a menudo carecen de la capacidad de generar certificados rigurosos y verificables por máquina.

El desafío central es cerrar la brecha entre el descubrimiento heurístico y la verificación formal rigurosa, habilitando la demostración automatizada de desigualdades polinómicas sin restricciones en entornos de alta dimensionalidad (hasta 10 variables) con corrección verificada por máquina.

Metodología: Marco NSPI

Los autores proponen NSPI (Demostración de Desigualdades Polinómicas Basada en SOS Neuro-Simbólica), un marco que integra las fortalezas complementarias de los LLM y el cálculo simbólico en una tubería de extremo a extremo. El proceso consta de tres etapas principales:

1. Conjetura Neuronal (Generación de SOS Guiada por LLM)

En lugar de utilizar los LLM meramente para la guía de búsqueda, NSPI los eleva a generadores primarios de conjeturas.

Construcción de Datos: Los autores construyen un conjunto de datos a gran escala de pares polinomio-SOS no negativos utilizando dos estrategias novedosas:
- Impulsado por Cálculo: Generación de matrices de Gram mediante desplazamiento espectral u optimización LMI para garantizar la semidefinición positiva (PSD) con coeficientes controlados.
- Impulsado por Estructura: Explotación de estructuras algebraicas como matrices diagonalmente dominantes (dd) y escaladas diagonalmente dominantes (sdd), que garantizan propiedades PSD por diseño.
Entrenamiento: Se emplea un esquema de entrenamiento en dos etapas:
- Arranque en Frío: Ajuste Fino Supervisado (SFT) en más de un millón de pares sintéticos polinomio-SOS para establecer un razonamiento estructural fundamental.
- Refuerzo Progresivo: Se aplica la Optimización de Política Relativa Grupal (GRPO) basada en currículos a instancias desafiantes (aumentando la cantidad de variables de 3–5 a 9–10). La función de recompensa combina precisión (fidelidad numérica), adherencia al formato y penalizaciones de estructura algebraica para asegurar que el LLM genere estructuras SOS plausibles.
Salida: El LLM propone una descomposición SOS aproximada (una suma de términos al cuadrado) para un polinomio dado.

2. Corrección Simbólica (Recuperación Racional Exacta)

Para transformar la conjetura aproximada del LLM en una prueba rigurosa, un módulo de corrección simbólica refina la salida:

Refinamiento Gauss-Newton: La estructura SOS aproximada se refina utilizando métodos iterativos tipo Newton para minimizar el error hacia atrás entre la suma de cuadrados conjeturada y el polinomio objetivo. Esto produce una matriz de Gram numérica de alta precisión.
Recuperación Racional: La matriz numérica se convierte en una matriz PSD racional exacta. Dependiendo de si la solución se encuentra en el interior o en el borde del cono PSD, el sistema emplea proyección ortogonal o factorización LDL $^\top$ truncada combinada con aproximación diofántica simultánea. Este paso asegura que el certificado SOS resultante sea exacto y libre de errores de punto flotante.

3. Verificación Formal (Generación de Pruebas en Lean)

El certificado SOS racional exacto se convierte automáticamente en una prueba en Lean verificable por máquina.

Plantillas de Prueba: Las plantillas de Lean predefinidas se rellenan con los términos SOS exactos.
Verificación: El demostrador de Lean verifica dos condiciones:
1. Igualdad: El polinomio objetivo es igual a la expresión SOS expandida (verificado mediante linear_combination).
2. No negatividad: La expresión SOS es no negativa (verificada mediante la táctica positivity, que aplica recursivamente reglas como $x^2 \ge 0$ ).

Contribuciones Clave

Tubería Neuro-Simbólica: La propuesta de NSPI, un marco de extremo a extremo que automatiza la generación de pruebas formales completas para desigualdades polinómicas encadenando la conjetura neuronal, la corrección simbólica y la verificación formal.
Puente de Confiabilidad Principiado: Un método novedoso para integrar la generación heurística basada en LLM con la certificación simbólica exacta. Esto transforma las conjeturas neuronales en pruebas verificables por máquina, permitiendo la escalabilidad a casos multivariados de alta dimensionalidad (hasta 10 variables) sin depender de grandes cantidades de datos de entrenamiento formalizados preexistentes.
Punto de Referencia y Evaluación: La construcción de PolyIneqBench, un punto de referencia desafiante que contiene 522 problemas de desigualdad (de 3 a 10 variables), incluyendo problemas de competiciones reales e instancias sintéticas de alta dimensionalidad. Experimentos extensos demuestran que NSPI supera a los solucionadores simbólicos más avanzados (Maple, Z3), a los demostradores puros de LLM (DeepSeek-Prover-V2, Goedel-Prover) y a los sistemas híbridos existentes (LIPS), particularmente en escenarios de alta dimensionalidad.

Resultados Experimentales

Rendimiento: En PolyIneqBench, NSPI logró una tasa de aprobación del 11.7% para problemas de 10 variables, mientras que los métodos simbólicos (Maple, Z3) y los demostradores puros de LLM cayeron a cerca del 0% o dígitos simples.
Eficiencia: NSPI mantuvo el tiempo de ejecución promedio más bajo entre los solucionadores exitosos, demostrando una aceleración de más de 10x en comparación con varios demostradores basados en LLM.
Escalabilidad: La estrategia de aprendizaje por refuerzo progresivo desplazó con éxito el límite de capacidad del modelo hacia dimensiones más altas, observándose ganancias de rendimiento a medida que el currículo avanzaba de 3–5 variables a 9–10 variables.
Ablación: Los experimentos confirmaron que tanto el entrenamiento de arranque en frío sintético como el GRPO basado en currículos son críticos para el éxito del sistema.

Significado y Afirmaciones

El artículo afirma establecer un nuevo paradigma en la demostración de teoremas neuro-simbólica donde los LLM funcionan como motores centrales de conjeturas simbólicas en lugar de meras guías de búsqueda. Al tratar a los LLM como generadores de priores simbólicos (estructuras SOS) y confiar en el cálculo simbólico para la precisión y en la verificación formal para la corrección, el enfoque aborda el cuello de botella de la escasez de datos de los métodos neuronales puros y los límites de escalabilidad de los métodos simbólicos puros.

Los autores posicionan a NSPI como una extensión significativa de la frontera para la demostración automatizada de desigualdades polinómicas, manejando con éxito casos de alta dimensionalidad (hasta 10 variables) que previamente eran intratables para los sistemas automatizados existentes. El trabajo demuestra que combinar el descubrimiento heurístico con la certificación rigurosa puede ampliar sustancialmente el alcance práctico del razonamiento matemático automatizado.