Google DeepMind представи AlphaProof Code, система, която използва AI агенти за създаване на математически доказателства за софтуер. Изследователите я приложиха към зададени свойства на сигурността в кода зад протокола Signal.
Експерти проверяват математическите спецификации, преди агентите да генерират доказателства на езика Lean. Отделна проверка потвърждава валидността им. При тест с две стари, вече поправени грешки, върнати в изолирано копие на кода, системата установява получената уязвимост.
Формалната проверка установява дали кодът изпълнява точно зададена спецификация. Заключенията зависят от включените свойства и предположения. Сигурността зависи също от приложението, операционната система и устройството.
Разработката показва възможен път за по-широко използване на математически проверки в реален софтуер. DeepMind планира да разшири подхода към процесите за разработване.
