LLM2Cert verifica 81 de 105 certificados de estabilidad y seguridad

Los modelos de lenguaje han aprendido a escribir código y a demostrar teoremas. Ahora se los prueba en una tarea de ingeniería donde un error sale caro: confirmar que un sistema dinámico se mantiene estable y seguro. Los autores del preprint LLM2Cert (arXiv 2610.30524) han construido un framework en el que un LLM propone certificados y verificadores formales los comprueban. En el nuevo benchmark DynaCertBench, de 105 tareas, el sistema verifica 81, es decir, el 77,1%. Son 17,1 puntos porcentuales más que la generación única sin retroalimentación (alrededor del 60%).

Por qué los certificados siguen siendo un cuello de botella

Las funciones de Lyapunov y los certificados de barrera ofrecen garantías en el espacio de estados. Las primeras muestran que el sistema es estable; los segundos demuestran que no entrará en una región peligrosa. La dificultad es que primero hay que encontrar estas funciones y después comprobarlas con rigor. Para los sistemas no lineales multidimensionales, esto sigue siendo un problema abierto.

Los pipelines actuales verifican a los candidatos de tres maneras: con solvers numéricos (programas de sum-of-squares), con métodos de intervalos y con solvers SMT. Los tres comparten problemas: requieren relajaciones, son conservadores o escalan mal a medida que crecen la dimensión y la no linealidad del modelo.

Los autores señalan además un efecto secundario. Los conjuntos de prueba estándar se componen sobre todo de sistemas polinomiales de baja dimensión, elegidos según lo que pueden resolver los solvers y no según las necesidades de la ingeniería. Los benchmarks reflejan lo que saben hacer las herramientas, no lo que hace falta en la práctica.

DynaCertBench y el enrutamiento de obligaciones

La primera parte del trabajo se centra en el conjunto de prueba. DynaCertBench contiene 105 tareas:

• 80 sistemas no redundantes seleccionados de la literatura;
• ampliaciones de esos sistemas con variantes multidimensionales y con restricciones de control;
• nuevos sistemas con acoplamiento no lineal;
• cuatro clases de tareas: estabilidad, región de atracción (region of attraction), invariancia hacia adelante (forward invariance) y seguridad.

La segunda parte es el propio LLM2Cert. El modelo genera un certificado candidato y el framework lo descompone en obligaciones de prueba. Cada obligación sigue una de dos vías: va a un solver SMT o directamente al agente Lean Proof-Repair. Lean actúa aquí como verificador formal estricto, y el agente repara la demostración cuando no converge. La retroalimentación de los verificadores aporta la mayor parte de la mejora: sin ella, el modelo que produce un solo candidato cierra bastantes menos tareas.

Las cifras que conviene tener presentes

• DynaCertBench: 105 tareas, 80 de ellas de la literatura.
• LLM2Cert verifica 81 de las 105 tareas, el 77,1%.
• Mejora sobre la propuesta one-shot sin retroalimentación: 17,1 p. p.
• De los 81 certificados encontrados, 22 se verifican en casos en los que el enfoque All-SMT, que envía todo al solver SMT, deja la cuestión abierta.

La última cifra es quizá la más reveladora. Se trata de casi una cuarta parte de los certificados del conjunto, fuera del alcance del SMT puro. El enrutamiento híbrido cierra parte de las tareas que el SMT por sí solo no resuelve.

El artículo lo han elaborado Zhipeng Cao, Peiyang Song, Nikolaus Vertovec, Weiru Cui, Zhihao Yang, Mingkang Liu, Luxia Lin, Bai Xue y Alessandro Abate. El código y los datos están publicados en el repositorio FormalCert-AI/llm2cert.

A quién le servirá primero

El efecto práctico se espera donde el control de sistemas no lineales exige garantías formales: robótica, transporte autónomo, redes eléctricas y aviónica. Hoy, un ingeniero tiene que elegir el certificado a mano o mediante programas SOS, que chocan con el límite de la dimensión. El esquema «el LLM propone, el solver y Lean verifican» traslada la parte creativa al modelo y deja la confianza en manos de la verificación formal. Aunque el modelo se equivoque, un certificado incorrecto no pasará la verificación.

Para los investigadores, lo útil es el propio DynaCertBench: permite comparar nuevos métodos de síntesis en tareas más cercanas a los sistemas reales que los habituales polinomios de baja dimensión. El código abierto permite reproducir los resultados y conectar otro modelo. Quedan 24 tareas de las 105 que LLM2Cert no ha cerrado, y ellas muestran dónde están los límites del método.