Последний прорыв OpenAI в области математики может приблизить автоматизированное доказательство теорем к рабочим процессам безопасности смарт-контрактов.
8 сентября компания OpenAI заявила, что примерно 10 000 одновременных ИИ-агентов нашли решение проблемы движения жидкостей Навье-Стокса примерно за 88 часов. Формализация и проверка в Lean, программном ассистенте для доказательств, потребовали еще 17 часов с использованием GPT-6 Astra.
Система сгенерировала аналитическое доказательство, показывающее, что изначально гладкая жидкость может развить сингулярность за конечное время, сохраняя при этом конечную энергию, что соответствует случаям C и D формулировки задачи из «Математической премии тысячелетия». OpenAI опубликовала как само доказательство, так и его формализацию в Lean для независимой проверки.
Для крипторазработчиков более непосредственное значение заключается в самом процессе. Формальная верификация использует математические спецификации и доказательство теорем для установления того, соответствует ли код смарт-контракта заданным намерениям, — область, где человеческое руководство может сделать проверку дорогостоящей и трудоемкой.
ИИ может сместить «узкое место» безопасности вверх по цепочке
Масштаб эксперимента OpenAI тесно перекликается со сценарием, описанным математиком Теренсом Тао за пять дней до объявления.
Тао предупредил, что автономные ИИ-системы, поддерживаемые огромными вычислительными ресурсами, в конечном итоге смогут генерировать сложные решения для задачи Навье-Стокса и формально проверять их в таких системах, как Lean, при этом большая часть итеративного процесса открытия останется вне поля зрения общественности.
Его обеспокоенность была сосредоточена на том, что исследователи могут упустить в процессе. Неудачные подходы и промежуточные открытия часто дают идеи, которые переживают окончательное доказательство, в то время как в значительной степени автономная система может выдать правильный результат, не передавая той же глубины понимания людям.
Эта обеспокоенность переносится и на безопасность смарт-контрактов по мере автоматизации доказательства теорем.
В документации Ethereum говорится, что формальная верификация устанавливает, удовлетворяет ли контракт свойствам, заранее определенным разработчиками. Плохо написанные или неполные спецификации могут привести к тому, что уязвимости останутся необнаруженными, даже если проверка пройдет успешно.
Более мощные ИИ-системы, следовательно, могли бы сократить объем работы, необходимой для построения доказательств, одновременно повышая важность определения того, что эти доказательства должны охватывать. Контроль доступа, условия вывода средств, инварианты учета и привилегированные функции по-прежнему должны быть точно выражены, прежде чем верификатор сможет их протестировать.
Это могло бы изменить экономику формальной верификации для DeFi-протоколов, мостов и платформ токенизированных активов, где ручной труд ограничивал широкое применение этой техники.
Следующим испытанием станет адаптация систем, способных обрабатывать исследовательскую математику, к производственному программному обеспечению и получение доказательств, которые разработчики и аудиторы смогут осмысленно проверить.
Компании, которые смогут сочетать автоматизированное доказательство теорем с строгим дизайном спецификаций, смогут проверять больше контрактов перед развертыванием, концентрируя человеческий опыт на определении сбоев, которые никогда не должны происходить.
Всегда имейте в виду, что редакции могут придерживаться предвзятых взглядов в освещении новостей.
Автор – Oluwapelumi Adejumo
