Ethereum отправляет AI-агентов доказывать недоказанное крипто-допущение

Команда Formal Verification при Ethereum Foundation вместе с Yukon и zkSecurity запустила в среду better.codes, объявила команда, публичный челлендж, платящий за то, чтобы AI-агенты любого желающего отгрызали кусок допущения безопасности, на которое сейчас полагается большая часть zero-knowledge инфраструктуры Ethereum, не имея формального доказательства.

Хеш-SNARK-и, системы доказательств за zk-роллапами, zkVM и частью постквантового плана Ethereum, опираются на нечто под названием proximity gaps и correlated agreement для кодов Рида-Соломона. Развёрнутые системы рассчитаны на 128-битную безопасность, но эта гарантия работает в полном объёме, только если лежащие в основе математические гипотезы об этих кодах окажутся верны, а прямо сейчас то, что исследователи могут формально доказать, отстаёт от того, во что они верят. Better.codes нацелен на конкретный кусок этого разрыва: задачу близости Рида-Соломона под названием koalaIRS12, взятую из более ранней инициативы Foundation Proximity Prize и открытых проблем, которые Гал Арнон, Дэн Бонэ и Джакомо Фенци сформулировали в статье о декодировании списков и согласованном соответствии.

• Целевой уровень безопасности koalaIRS12: 128 бит, пока не доказан на этой прочности
• Источник задачи: инициатива Foundation Proximity Prize и статья Арнона, Бонэ и Фенци
• Инструмент формализации: Lean 4, через библиотеку ArkLib для верифицированных аргументов знания
• Способ участия: вход через GitHub на better.codes и отправка решения внутри закреплённой формулировки задачи
• Прежние челленджи в этом формате: ecdsa.fail, zk.golf, snark.fast

Механика построена на коде, а не на комитете рецензентов. Формулировка теоремы, точка параметров и верификационная обвязка остаются фиксированными, и каждый участник отправляет доказательство внутри этой закреплённой площадки. Компаратор проверяет, что отправленная теорема точно совпадает с закреплённой формулировкой, затем само ядро Lean проверяет доказательство, без участия человека-судьи на обоих этапах. Принятые решения попадают в публичный лидерборд с указанием и участника, и конкретной AI-модели, создавшей доказательство, а их новые леммы и техники встраиваются обратно в общую кодовую базу, чтобы следующий участник стартовал с того места, где остановился предыдущий.

SNARK позволяет одной стороне доказать, что вычисление прошло верно, не заставляя вторую сторону переделывать работу или видеть все входные данные, и именно это позволяет роллапу публиковать в Ethereum одно доказательство вместо каждой обработанной транзакции. Надёжность (soundness) — это свойство, не позволяющее подделать доказательство для вычисления, которого никогда не было, и это то самое свойство, от которого реально зависит пользователь роллапа: если надёжность откажет, злоумышленник сможет убедить сеть, что ложный переход состояния корректен. Сейчас индустрия опирается на веру в то, что надёжность держится на уровне 128 бит для кодов, которые используют эти системы, подкреплённую годами криптоанализа, а не формально проверенным машиной доказательством. Закрытие этого разрыва не изменит поведение ни одного действующего роллапа сегодня, но изменит то, что исследователь безопасности сможет утверждать с уверенностью, а не с доверием.

Foundation называет этот формат автоисследованием: вместо одной команды, в одиночку работающей над сложной задачей, множество независимых групп одновременно запускают собственных AI-агентов против одного и того же зафиксированного бенчмарка, и любое принятое доказательство поднимает планку для всех, кто ещё работает над задачей. Это та же готовность отдавать AI-агентам открытые, проверяемые задачи, на которую делает ставку Generalist AI со своими роботами, обучающимися по одной демонстрации, только здесь задача, это формальное доказательство, которое машина может проверить построчно, а не физическое движение, которое должна оценить камера. Сегодняшний челлендж охватывает только границу надёжности для koalaIRS12, и Foundation говорит, что дальше могут появиться новые челленджи, а критерии участия, оценка и любые награды регулируются условиями программы, которые ещё могут измениться по ходу развития.

Это не финансовый совет — только информация к размышлению.