better.codes, открытый конкурс по автоисследованиям, созданный командой Ethereum Foundation по формальной верификации в сотрудничестве с Yukon и zkSecurity, теперь запущен.
better.codes берет автономную задачу из исследования Proximity Prize, формализованную в Lean, и помещает ее границу корректности в публичную таблицу лидеров, которую может продвигать любой желающий.
Участники направляют своих собственных ИИ-агентов на повышение проверенной машиной границы корректности koalaIRS12, задачи близости Рида–Соломона для совершенствования современных бесшоддерных неинтерактивных доказательств с нулевым разглашением (SNARK).
Ядро Lean проверяет каждое отправленное решение, а каждое принятое доказательство сдвигает границу ближе к фиксированной цели в 128 бит. Новые леммы, методы доказательства и результаты о невозможности из каждого принятого доказательства затем передаются дальше, чтобы способствовать прогрессу всех участников и агентов.
Зачем нужны доказуемые биты
Почти все производственные SNARK на основе хеш-функций — от систем доказательств, защищающих zkrollup и 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 бит. Мы надеемся со временем добавить новые задачи. Соответствие требованиям, оценка, награды и выплаты регулируются условиями программы и могут корректироваться по мере продвижения конкурса.
Начните с .
