El equipo de la red Ethereum ha publicado una serie de posts invitados del desarrollador principal de Vyper bajo el seudónimo big_tech_sux, dedicada al papel de la verificación formal en la era del rápido desarrollo de la inteligencia artificial.
El autor sostiene que el progreso de los LLM está haciendo que la demostración matemática de la corrección de los programas sea más accesible, y que para los contratos inteligentes, que gestionan miles de millones de dólares, la verificación formal se está convirtiendo gradualmente en una necesidad.
La IA está cambiando el enfoque de verificación de software
En la serie de posts se explica que la verificación formal es un método matemático que permite demostrar el funcionamiento correcto de un programa para todos los escenarios de ejecución posibles, no solo para los cubiertos por las pruebas.
Como ejemplo, el autor citó la función f(x) = x/2, para la cual se puede demostrar matemáticamente que el resultado nunca superará el valor de entrada.
Según sus palabras, esta metodología es capaz de encontrar errores extremadamente raros que prácticamente es imposible detectar con pruebas ordinarias.
«La verificación formal puede detectar un caso entre un cuatrillón que nunca aparecerá durante las pruebas, pero que precisamente puede llevar a un fallo catastrófico», señaló el autor.
Al mismo tiempo, reconoció que hasta hace poco el uso de este enfoque requería el trabajo de grandes equipos de expertos que creaban modelos matemáticos de los programas y realizaban demostraciones complejas.
En opinión del desarrollador, los LLM modernos simplifican sustancialmente este proceso a medida que nos acercamos a la IAG.
Sin embargo, el autor subrayó que incluso con la ayuda de la IA, la verificación formal sigue siendo un proceso complejo y que requiere muchos recursos. En particular, la transformación del código de software en un modelo formal puede contener imprecisiones que afectan a la fiabilidad de los resultados.
El desarrollo de la IA cambia el equilibrio entre ataque y defensa
En el material se señala que el desarrollo de la inteligencia artificial aumenta simultáneamente la eficacia tanto de los defensores como de los atacantes malintencionados.
El autor recordó un caso en el que un modelo de OpenAI aún no lanzado fue capaz de encontrar vulnerabilidades de día cero que permitían eludir varios niveles de protección.
En este contexto, la verificación formal, según el autor, permite inclinar la ventaja a favor de los defensores.
«Mientras que a los atacantes les basta con encontrar solo una secuencia de datos de entrada para hackear el sistema, los defensores pueden utilizar la verificación formal para demostrar su resistencia a todos los datos de entrada posibles», subrayó.
Es por ello que para el software crítico, en particular los contratos inteligentes que gestionan miles de millones de dólares de fondos de los usuarios, la verificación formal se convierte en "no una opción, sino un requisito previo necesario".
Vale la pena señalar que esto continúa el debate iniciado anteriormente por el cofundador de Ethereum, Vitalik Buterin, sobre el uso de la IA para la verificación formal del código.
end-content
