Ya tenemos pruebas de automatización
La verificación formal de software, durante mucho tiempo vista como demasiado costosa y especializada, está siendo remodelada por los grandes modelos de lenguaje, que ahora pueden generar y automatizar muchas pruebas dentro de sistemas como Lean. Los comentaristas sostienen que esto podría hacer práctico el software de alta garantía e incluso el ensamblador verificado para más dominios, especialmente los críticos para la seguridad, pero enfatizan que escribir buenas especificaciones y abstracciones sigue siendo la parte difícil y que los métodos formales aún pueden demostrar correcto el comportamiento “equivocado” si la especificación es defectuosa. Hay un debate activo sobre cómo escalan los tipos dependientes y las funciones totales en el mantenimiento del mundo real y sobre si la verificación impulsada por LLMs cambiará de forma significativa las prácticas de ingeniería de software convencionales o seguirá centrada en casos límite críticos.
LLMs + Automatización de pruebas
- Muchos ven los LLMs + demostradores de teoremas (Lean, sistemas al estilo HOL, etc.) como un cambio de escala: ahora pueden descargar grandes partes de pruebas que antes llevaban días o semanas.
- La irrelevancia de las pruebas, junto con la automatización, puede hacer que los sistemas de tipos dependientes ricos sean más prácticos, reduciendo el esfuerzo de “ingeniería de pruebas”, aunque la buena descomposición de problemas y las abstracciones siguen siendo críticas.
- Algunos describen experimentos exitosos en los que los LLMs recrearon pruebas formales de varios días en minutos, lo que sugiere que proyectos de verificación antes “insanos” (núcleos, grandes teoremas) se vuelven plausibles como esfuerzos en solitario.
Las especificaciones como cuello de botella
- Varios sostienen que lo más difícil no es demostrar la corrección, sino definirla: el software del mundo real a menudo carece de un comportamiento preciso para casos extremos (fallos de red, copias de seguridad, serializadores, etc.).
- Escribir especificaciones formales puede superar en longitud y complejidad al código; los errores en las especificaciones se traducen directamente en sistemas “verificados” pero incorrectos.
- Las especificaciones parciales (por ejemplo, round-tripping, comprimir/descomprimir como inversos, “nunca ejecuta código arbitrario”) siguen considerándose muy valiosas.
Tipos dependientes, mantenimiento y diseño del lenguaje
- Un bando afirma que los tipos dependientes y las funciones totales no escalan para sistemas grandes: añadir una nueva propiedad puede requerir pasar nuevos invariantes por muchos tipos y pruebas.
- Contraargumento: esto es análogo a mantener la corrección en cualquier sistema grande; una buena estructuración (separar preocupaciones, usar tipos opacos, núcleos pequeños y confiables) mitiga el dolor.
- Los lenguajes futuros que integren la verificación en el sistema de tipos se consideran prometedores, pero muchos esperan que la mayoría de los programas solo verifiquen partes críticas, no sistemas completos.
Seguridad, criptografía y ensamblador verificado
- Las blockchains y la criptografía se destacan como candidatas principales: adversarios fuertes, historia de métodos formales e interés en ensamblador y compiladores verificados.
- A medida que encontrar exploits se vuelve más barato (incluido mediante IA), algunos argumentan que la verificación formal se vuelve económicamente más atractiva; otros creen que las organizaciones se detendrán en la búsqueda automatizada de errores “suficientemente buena”.
Comportamiento, alineación y límites de los LLMs
- Los LLMs a menudo evitan el trabajo pesado de demostración salvo que se los impulse con fuerza, prefieren soluciones superficiales y pueden ignorar bibliotecas potentes a menos que se les coaccione.
- También pueden implementar una función incorrectamente y luego generar pruebas/especificaciones que “demuestran” el comportamiento equivocado, por lo que la revisión humana de las especificaciones sigue siendo esencial.
- Los entusiastas ven los métodos formales + LLMs como transformadores; los escépticos advierten que esto principalmente traslada la dificultad a la especificación de nivel superior y no reemplazará las pruebas ni el juicio humano.