Amazon сделала крупнейшее пожертвование команде Lean — языка для доказательства корректности программ

Amazon будет долгосрочно финансировать Lean Focused Research Organization (Lean FRO) — независимую команду, которая разрабатывает язык программирования Lean. Об этом компания сообщила в блоге Amazon Science. Сумму не назвали, но уточнили, что это крупнейшее пожертвование за всю историю организации. Цель, по словам Amazon, — сделать математическое доказательство корректности кода доступным каждому разработчику.

Логика Amazon такая. ИИ-агенты всё чаще сами переводят деньги, одобряют страховые выплаты и управляют критической инфраструктурой. Обычного тестирования для такой работы уже мало: тест проверяет только те ситуации, которые кто-то заранее придумал. Формальное доказательство устроено иначе. Оно показывает, что система не может повести себя неправильно ни при каких входных данных. Lean позволяет записать такое доказательство, а компьютер проверяет его до последнего шага.

Сама Amazon уже использует Lean в нескольких продуктах. В Bedrock AgentCore (это платформа для запуска ИИ-агентов) на Lean доказана корректность языка политик — правил, которые не дают агенту выходить за разрешённые рамки. В Amazon утверждают, что больше никто таких математических гарантий не даёт. Кроме того, на Lean опираются SampCert, который подтверждает, что защита дифференциальной приватности в AWS Clean Rooms действительно работает, и компилятор AWS Neuron для собственных ИИ-чипов Amazon. Ещё один пример: сотрудник компании вместе с языковой моделью доказал на Lean корректность протокола восстановления сегментов в базе данных Amazon Aurora. Amazon называет этот протокол самым критичным для сохранности данных. По словам компании, на это ушла малая доля времени, которое потребовалось бы на ручное доказательство.

Вокруг Lean давно сложилось большое сообщество математиков, программистов и физиков. На нём построена Mathlib — обширная библиотека формализованной математики. Язык стал важен и для обучения ИИ: модели учатся писать формальные доказательства на Lean, а проверку пройдёт только верное доказательство. Такие модели ошибаются реже и, как пишет Amazon, уже решают задачи исследовательского уровня. Так, в сентябре OpenAI опубликовала доказательство на Lean к своему решению задачи Навье — Стокса.

Почему Amazon не развивает Lean у себя, а финансирует внешнюю организацию? Компания объясняет это доверием. Доказательству проще верить, если инструменты, на которых оно построено, может проверить кто угодно. Клиенты, аудиторы и регуляторы могут сами изучить инструмент, которым управляет сообщество. Есть и практическая причина: чем больше у Lean разработчиков, в том числе из Amazon, тем больше библиотек, инструментов и готовых доказательств получают все.

Для отрасли это заметный сигнал: крупный облачный провайдер делает ставку на нейросимвольный ИИ, в котором генеративные модели проверяются строгой математикой, и считает формальную проверку частью безопасности агентов. Каким будет размер финансирования, сколько оно продлится и на какие направления пойдут деньги, Amazon не сообщила.