Amazon с помощью ИИ доказала надёжность протокола базы данных Aurora

Исследователи Amazon математически доказали, что основная часть Grover, протокола хранения в облачной базе данных Aurora, не теряет уже надёжно записанное. Описание протокола и доказательство предлагала языковая модель, а каждый шаг проверяла программа Lean 4¹.

Почему это важно: модели здесь не нужно верить на слово. Доказательство, как решение судоку, можно проверить, не доверяя тому, кто его нашёл, поэтому математическую проверку систем, от которых зависит сохранность данных, можно поручать ИИ.

Детали: шанс отказа одной машины слишком высок, поэтому Grover по умолчанию держит шесть копий данных и обещает выдержать одновременный отказ любых двух машин. Сломавшиеся заменяют запасные, на которые данные копируются с исправных. Сложность в том, что связь между машинами ненадёжна: часть правок до машины иногда не доходит, одна машина может не узнать об обновлении другой, а о новой правке они узнают в разное время.

Доказательство показывает: данные, однажды надёжно сохранённые, остаются такими, сколько бы раз их копии потом ни восстанавливали после сбоев и ни переносили с машины на машину. Оно не привязано к числу машин, поэтому подходит для любой настройки Grover, а не только для шести копий.

Как это работает: вручную авторы написали шаблон на Lean 4, годный для любого распределённого протокола, то есть правил, по которым несколько машин согласуют данные. Заполняла его модель — по документации Grover. Затем она предлагала описание протокола и пыталась доказать его надёжность или найти контрпример — случай, когда протокол ломается.

Обычно находился контрпример. Тогда исследователи вносили в описание на Lean 4 минимальную правку, чтобы исключить этот случай, и держались как можно ближе к документации. Цикл повторялся, пока для очередного описания вместо контрпримера не нашлось доказательство. Затем они автоматически построили контрпримеры, показав, что без любой из этих правок соответствующие теоремы перестают выполняться. Какую модель использовали, Amazon не называет.

Интрига: перевод на язык Lean 4 вскрыл в документации Grover множество двусмысленностей и опечаток. Прочитанная буквально, она описывала протокол, способный терять данные. Об одном условии авторы документации знали, но забыли его записать: его нарушение иногда вело бы к потере данных, если поднять число копий выше стандартных шести. Теперь такие требования записаны для тех, кто будет поддерживать и менять Grover. О реальных потерях данных Amazon не сообщает.

Но: это пробная работа, и её итог — проверенный эталонный алгоритм для будущих реализаций. Математика ручается только за протокол, записанный в Lean 4, а совпадает ли он с задуманным, решают люди. Для них авторы свернули описание в компактную запись, которая помещается в один файл, и формально доказали, что обе версии равносильны. Специалисты команды Grover эту сверку ещё ведут.

Если шире: в июле Amazon объявила о долгосрочной денежной поддержке Lean FRO, организации, которая развивает Lean, — это крупнейшее пожертвование в её истории. Тогда же компания коротко упомянула, что один из её учёных с помощью языковой модели и Lean доказал корректность протокола восстановления сегментов Aurora гораздо быстрее, чем вручную.

Что дальше: авторы работы Сэмюэл Тенка (Samuel Tenka) и Канна Симидзу (Kanna Shimizu) надеются применить метод не только к Grover, но и к другим распределённым протоколам. Тогда, пишут они, разработчики смогут улучшать такие протоколы «со скоростью, которая зависит от их аппетита к улучшениям, а не от аппетита к риску».