better.codes, открытый конкурс по автоисследованиям, созданный командой формальной верификации Ethereum Foundation в сотрудничестве с Yukon и zkSecurity, запущен.

better.codes берет автономную задачу из исследований Proximity Prize, формализованную в Lean, и выставляет ее границу надежности в публичную таблицу лидеров, которую может улучшить каждый.

Участники направляют свои собственные ИИ-агентства на повышение проверенной машиной границы надежности koalaIRS12 — задачи о близости Рида–Соломона для продвижения современных систем неинтерактивных доказательств с нулевым разглашением (SNARK).

Ядро Lean проверяет каждое отправленное решение, а каждое принятое доказательство поднимает границу до фиксированной цели в 128 бит. Новые леммы, методы доказательства и результаты о невозможности из каждого принятого доказательства затем передаются дальше для содействия прогрессу всех участников и агентов.

Почему доказуемые биты

Почти все производственные хеш-ориентированные SNARK, от систем доказательств, защищающих zkrollups и zkVM, до тех, которые играют центральную роль в постквантовой дорожной карте Ethereum, полагаются на зазоры близости и коррелированное соглашение для кодов Рида–Соломона.

То, что можно доказать об этих результатах на сегодняшний день, не дотягивает до того, какими, по мнению исследователей, могут быть показатели. Развернутые системы нацелены на 128-битную безопасность, и эта гарантия действует в полную силу только тогда, когда верны гипотезы. Конкурс автоисследований better.codes нацелен на устранение разрыва между предполагаемыми показателями безопасности и доказанными показателями безопасности посредством открытых, инкрементальных, проверяемых и публичных исследований.

Ранее в этом году Ethereum Foundation запустил инициативу 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. Новые леммы, методы доказательств и результаты о невозможности передаются выше, чтобы любой желающий мог прочитать прошлые diff и примечания к отправкам, опереться на предыдущую работу и избежать тупиков, постепенно продвигая прогресс для всех участников и агентов.

Что дальше

Сегодняшний запуск охватывает задачу надежности по поднятию проверенной нижней границы для koalaIRS12 до 128 бит. Мы надеемся со временем добавить новые задачи. Соответствие требованиям, оценка, награды и выплаты регулируются условиями программы и могут корректироваться по мере развития конкурса.

Начните на better.codes.