Google DeepMind demuestra matemáticamente la seguridad del código de Signal con IA

Genial, qué gran caso de uso para la IA. Siento que Google ha sido el más limpio de los grandes jugadores en términos de contribuciones útiles y control de sus sistemas de IA. Sin embargo, este nuevo agente de demostración no parece desafiar la especificación, solo la implementación, si he entendido bien.

Me pregunto en qué se diferencia este agente de un agente de codificación clásico; al final parece funcionar igual, iterando sobre una base de código mientras escribe código Lean o Rocq y lo ejecuta.

Espero que muy pronto, quizás en los próximos dos o tres años, parezca una locura que alguna vez hayamos ejecutado _cualquier_ software no verificado en nuestros sistemas, como ahora parece una locura que usáramos Telnet o HTTP en texto plano.

A principios de este año estaba haciendo algunas refactorizaciones importantes de un proyecto antiguo. En ese momento los agentes de codificación estaban despegando realmente, hasta el punto de que cada vez se podía confiar más en ellos para trabajo más autónomo, así que estaba emocionado de probarlo.

Hizo la refactorización, ejecutándose durante varias horas, y además ofreció voluntariamente una extensa suite de pruebas. ¡Todas las pruebas en verde!

Quedé muy impresionado, hasta que entrecerré los ojos un poco. ¡Había implementado todo al revés, de una manera que no solo era inútil (no lograba ninguno de los objetivos declarados) sino que en realidad empeoraba las cosas en comparación con antes!

Hasta ese momento había sido bastante optimista sobre el potencial de la verificación formal en la era de la IA. Pero al ver ese desastre, me di cuenta de que bien podría haberme escrito una demostración matemática para el código que escribió, y la demostración habría pasado, ¡y el código seguiría estando mal!

Muy genial. Hace un par de años estaba jugueteando con la idea de desarrollar un modelo especializado para verificación formal usando algo como el enfoque AlphaZero. Dadas las noticias de los últimos meses, ahora me alegro de no haberlo hecho; realmente parece que los LLM de propósito general se están comiendo todo.

Es interesante que terminen con 26k líneas de especificaciones (incluyendo la semántica de Arm). Eso es una base de confianza bastante grande. Supongo que necesitan desarrollar los modelos simbólicos/computacionales desde cero. Será interesante ver si podemos desarrollar bibliotecas reutilizables de estos, al estilo de mathlib, y cómo funcionan los incentivos allí. Probablemente a los laboratorios de IA no les interese particularmente esto, y también es probable que sea un trabajo ingrato para los investigadores. Pero quizás si surgen empresas que hacen verificación o venden productos verificados, tal vez tengan un incentivo para compartir el trabajo y tener una TCB estandarizada. Eso podría, para bien o para mal, también poner fin práctico a las "guerras de demostradores de teoremas interactivos".

También es interesante cómo esto funcionará para el código en desarrollo. ChatGPT afirma que al día siguiente de que se publicara esto, libsignal cambió sustancialmente :D Quizás un modelo intermedio, no confiable, en Rust podría ayudar (donde la mayor parte de la demostración relaciona el modelo Rust con la especificación, y luego una demostración más mecánica relaciona el modelo Rust con el binario); seL4 hizo esto hace mucho tiempo. Pero no tengo idea de si esto es práctico, no he oído nada e […]

He estado experimentando con lo fácil que es para la IA escribir Lean (https://metamagic.substack.com/p/beyond-the-proof-dump-lean-...) y algunas lecciones:

1. La IA en Lean no es perfecta y la IA puede hacer trampa fácilmente dado que ella escribe el Lean. Para cualquiera que esté jugando con código Lean generado por IA, como mínimo necesitas otro prompt adversarial para revisar el Lean generado por la IA.

2. En el artículo, hurgando un poco, veo que reintrodujeron algunos errores para verificar que los detectaría, pero parece que no encontraron ningún error. Quizás Signal es simplemente increíble con muchos ojos revisándolo, pero la verdadera historia para el resto de nosotros es que si empiezas a convertir a Lean con IA, el valor estará en las suposiciones que encuentre. Incluso para cosas que pensé que eran realmente lógicamente estrictas, Lean encontró algunas cosas menores que tuve que corregir. Similar al fuzzing, donde nunca he dejado de encontrar errores cuando introduje fuzzing en una base de código; espero lo mismo para convertir especificaciones a Lean.

3. Tener la capacidad de generar Lean (de manera barata) mediante IA es un desbloqueo muy interesante para la codificación. Potencialmente poder ir de la especificación a Lean a código, usando Lean como portero lógico, tiene el potencial de ser una capacidad real que se use más a diario y no solo en investigación.

Pregunta de novato: Aparte de estos sistemas criptográficos, ¿sería útil construir estas demostraciones para piezas generales de software? Específicamente:

1. ¿Alguien lo ha aplicado a sistemas de software donde un agente de IA está en la ruta crítica en producción, es decir, donde puede ocurrir una acción no determinista (aunque con recuperación)?

2. ¿En qué escenarios tiene sentido tener una demostración en Lean desde el principio? Por ejemplo, imagino que si quisieras hacer un sistema de base de datos con algunas garantías en torno a ACID, entonces podría ser mejor tener esto desde el principio. Pero probablemente no sea tan útil para construir un servicio respaldado por una API.

Impresionante. Recuerdo haber pensado el año pasado que el software está a punto de volverse mucho más propenso a errores ahora que la gente está delegando más a la IA, pero herramientas como esta me dan esperanza de que quizás el futuro del software en realidad se vea mucho más seguro.