Comprovar que un programa és segur sol voler dir provar-lo i buscar-hi errors, però això no garanteix que no n'hi quedin. L'alternativa és la verificació formal: demostrar matemàticament, amb proves que un ordinador pot revisar, que el codi fa exactament el que ha de fer. És molt fiable, però tan lenta i cara que gairebé només es fa servir en peces petites i crítiques. Google DeepMind va presentar dimarts AlphaProof Code, un sistema d'agents d'IA pensat per fer aquesta feina a una escala molt més gran.
Com a primera prova, l'equip el va posar a verificar el codi compilat del protocol criptogràfic de Signal, el que xifra de punta a punta els missatges de l'aplicació Signal i també els de Google Messages. Els agents, que funcionen amb el model Gemini 4 Carbon, van escriure més de sis milions de línies de Lean, un llenguatge que serveix per formular demostracions matemàtiques que un ordinador pot comprovar. La feina va durar quatre setmanes i només en un 1% del codi els agents van demanar que ho revisés una persona. Per assegurar-se que el sistema no donava per bo qualsevol cosa, els investigadors hi van tornar a introduir dos errors que ja s'havien corregit en el passat, i AlphaProof Code va produir demostracions, comprovades per la màquina, que aquelles versions eren insegures.
Si el mètode es confirma, podria canviar com es protegeix el programari més delicat: biblioteques de xifratge, sistemes bancaris o el codi que fa funcionar infraestructures. Fins ara, verificar formalment un programa d'aquesta mida requeria anys de feina d'especialistes, i els agents d'IA ho podrien fer en setmanes. DeepMind diu que publica els resultats de la verificació perquè altres equips els puguin fer servir.
La feina té límits. Els resultats els explica la mateixa empresa en un informe tècnic que no consta que hagi passat una revisió externa, i una verificació formal només garanteix el que diu l'especificació: si la descripció del que ha de fer el programa és incompleta, la demostració també ho serà. A més, el blog no aclareix si l'eina mateixa s'obrirà a altres usuaris, i el cost de computació de quatre setmanes d'agents no s'ha fet públic.