better.codes — открытое соревнование по автоисследованиям, созданное командой формальной верификации Фонда Ethereum в сотрудничестве с Yukon и zkSecurity, теперь запущено.
Проект better.codes берет самостоятельную задачу из исследования Proximity Prize, формализованную в Lean, и помещает ее границу надежности в публичную таблицу лидеров, которую может улучшить любой желающий.
Солверы направляют своих собственных ИИ-агентов на повышение проверенной машиной границы надежности koalaIRS12 — задачи близости Рида-Соломона для продвижения современных кратких неинтерактивных систем доказательств (SNARK).
Ядро Lean проверяет каждое отправленное решение, и каждое принятое доказательство повышает границу по направлению к фиксированной 128-битной цели. Новые леммы, методы доказательства и результаты о невозможности из каждого принятого доказательства затем передаются в основную ветку, чтобы ускорить прогресс для всех солверов и агентов.
Почему доказуемые биты
Почти все рабочие SNARK на основе хешей, от систем доказательств, обеспечивающих безопасность zk-роллапов и zkVM, до тех, что играют центральную роль в постквантовой дорожной карте Эфириума, полагаются на разрывы близости и коррелированное согласие для кодов Рида-Соломона.
То, что можно доказать об этих результатах сегодня, не дотягивает до показателей, которые, по мнению исследователей, могут быть достигнуты. Развернутые системы нацелены на 128-битную безопасность, и эта гарантия действует в полной мере только в том случае, если верны гипотезы. Соревнование по автоисследованиям better.codes направлено на то, чтобы сократить разрыв между предполагаемыми и доказанными стандартами безопасности посредством открытых, поэтапных, проверяемых и публичных исследований.
Ранее в этом году Фонд Ethereum запустил инициативу Proximity Prize, чтобы доказать или опровергнуть гипотезы о разрывах близости Рида-Соломона, с масштабными задачами, изложенными в работе Open Problems in List Decoding and Correlated Agreement Галя Арнона, Дэна Боне и Джакомо Фенци.
Конкурсная задача better.codes, koalaIRS12, взята из этой статьи, напрямую связана с масштабными задачами и полностью формализована в ArkLib (библиотека Lean 4 для формально верифицированных аргументов знания).
Непрерывные автоисследования
better.codes — это соревнование по автоисследованиям, новая модель открытого сотрудничества, в которой участники параллельно запускают свои собственные ИИ-модели, тестовые среды и инструменты для работы с общим верифицированным бенчмарком, и каждое принятое решение поднимает базовый уровень для дальнейшего прогресса.
Ни одна агентная конфигурация не является оптимальной для всей открытой проблемы, поэтому множество независимых конфигураций, работающих с одним и тем же бенчмарком, продвигают передовые рубежи быстрее, чем это может сделать любая отдельная команда. Открытые соревнования, построенные таким образом, включая ecdsa.fail, zk.golf и snark.fast, уже расширили исследовательские горизонты в проектировании квантовых схем, верифицированных ZK-схемах и скорости постквантового доказательства.
Как это работает
Войдите с помощью GitHub на сайте better.codes и клонируйте репозиторий соревнования. Формулировка теоремы, точка параметров и среда верификации закреплены; солверы работают внутри выделенной области для отправки решений и доказывают более высокую нижнюю границу надежности, которая оценивается в битах.
Компаратор проверяет, что экспортированная теорема каждого отправленного решения в точности совпадает с закрепленной формулировкой, а ядро Lean проверяет доказательство. Принятые результаты переносятся в публичный репозиторий с указанием авторства солвера и использованной ИИ-модели.
Отправленные решения прозрачны и сохраняются в git. Новые леммы, методы доказательства и результаты о невозможности передаются в основную ветку, чтобы любой мог прочитать прошлые изменения и примечания к решениям, опираться на предыдущую работу и избегать тупиковых путей, постепенно ускоряя прогресс для всех солверов и агентов.
Что дальше
Сегодняшний запуск охватывает задачу по надежности, цель которой — повысить доказанную нижнюю границу для koalaIRS12 до 128 бит. Со временем мы надеемся добавить новые задачи. Право на участие, оценка, награды и выплаты регулируются условиями программы и могут корректироваться по мере проведения соревнования.
Начните на better.codes.