ИИ-агенты DeepMind проверили шифрование Signal

Подразделение искусственного интеллекта (ИИ) Google, DeepMind, заявляет, что математически доказало с помощью ИИ, что ядро кода шифрования, используемого в зашифрованном мессенджере Signal, безопасно. Это было сделано путём обучения ИИ-агентов преобразовывать код в около шести миллионов строк на Lean, языке программирования для формальной верификации, который гарантирует корректность программного обеспечения. Только примерно один процент этих строк был проверен вручную экспертами-людьми, а остальное было сделано автоматически. Этот процесс занял всего четыре недели, по сравнению с годами, которые потребовались бы команде экспертов для выполнения такой задачи. В качестве доказательства концепции исследователи внесли две реальные ошибки, которые ранее были удалены из кода одной из версий Signal, и ИИ-агенты смогли определить оба случая как небезопасные.

В прошлом формальная верификация была трудоёмкой и затратной, из-за чего большинству компаний было непрактично использовать её для реального, развёрнутого программного обеспечения. Однако если ИИ-агенты способны повторить годы работы всего за несколько недель, требуя при этом минимального участия человека, то эту технику, возможно, удастся применять и к другим важным участкам кода — например, к тем, что используются в медицинском оборудовании или энергосетях, где одна-единственная ошибка способна затронуть огромное количество людей.