better.codes, otwarte wyzwanie typu autoresearch stworzone przez zespół weryfikacji formalnej Fundacji Ethereum we współpracy z Yukon i zkSecurity, jest już dostępne.
better.codes bierze samodzielny problem z badań Proximity Prize, sformalizowany w języku Lean, i umieszcza jego granicę poprawności (soundness bound) w publicznym rankingu, który każdy może poprawiać.
Solwery kierują swoich własnych agentów AI na podniesienie weryfikowanej maszynowo granicy poprawności koalaIRS12, problemu bliskości Reeda-Solomona, aby rozwijać nowoczesne zwięzłe nieinteraktywne systemy dowodów (SNARK-i).
Jądro Lean sprawdza każde zgłoszenie, a każdy promowany dowód podnosi granicę w kierunku ustalonego celu 128 bitów. Nowe lematy, techniki dowodzenia i wyniki niemożności z każdego promowanego dowodu są następnie włączane do głównego nurtu (upstreamed), aby przyspieszyć postęp dla wszystkich solwerów i agentów.
Dlaczego udowadnialne bity
Prawie wszystkie produkcyjne SNARK-i oparte na hashach, od systemów dowodów zabezpieczających zk-rollupy i zkVM, po te kluczowe dla postkwantowej mapy drogowej Ethereum, opierają się na lukach bliskości (proximity gaps) i skorelowanej zgodności (correlated agreement) dla kodów Reeda-Solomona.
To, co można dziś udowodnić na temat tych wyników, nie dorównuje temu, czym zdaniem badaczy mogą być te benchmarki. Wdrożone systemy celują w 128-bitowe bezpieczeństwo, a ta gwarancja jest w pełni utrzymana tylko wtedy, gdy prawdziwe są te hipotezy. Wyzwanie autoresearch better.codes ma na celu zniwelowanie luki między hipotetycznymi a udowodnionymi benchmarkami bezpieczeństwa poprzez otwarte, przyrostowe, weryfikowalne i publiczne badania.
Na początku tego roku Fundacja Ethereum uruchomiła inicjatywę Proximity Prize, aby udowodnić lub obalić hipotezy dotyczące luk bliskości Reeda-Solomona, z wielkimi wyzwaniami przedstawionymi w Open Problems in List Decoding and Correlated Agreement autorstwa Gala Arnona, Dana Boneha i Giacomo Fenziego.
Problem wyzwania better.codes, koalaIRS12, pochodzi z tego artykułu, łączy się bezpośrednio z wielkimi wyzwaniami i jest sformalizowany od początku do końca w ArkLib (bibliotece Lean 4 dla formalnie zweryfikowanych argumentów wiedzy).
Ciągłe autoresearch
better.codes to wyzwanie typu autoresearch, nowy model otwartej współpracy, w którym uczestnicy równolegle uruchamiają własne modele AI, środowiska testowe (harnesses) i narzędzia w odniesieniu do wspólnego, zweryfikowanego benchmarku, a każde promowane zgłoszenie podnosi poprzeczkę postępu.
Żadna pojedyncza konfiguracja agentowa nie jest optymalna dla całego otwartego problemu, więc wiele niezależnych konfiguracji pracujących nad tym samym benchmarkiem przesuwa Frontier szybciej, niż mógłby to zrobić jakikolwiek pojedynczy zespół. Otwarte wyzwania zbudowane w ten sposób, w tym ecdsa.fail, zk.golf i snark.fast, przesunęły już badawczy Frontier w projektowaniu obwodów kwantowych, zweryfikowanych obwodach ZK i szybkości dowodzenia postkwantowego.
Jak to działa
Zaloguj się przez GitHub na better.codes i sklonuj repozytorium wyzwania. Teza twierdzenia, punkt parametru i środowisko weryfikacyjne są przypięte; solwery pracują wewnątrz wyznaczonego obszaru zgłoszeń i dowodzą większej dolnej granicy poprawności, ocenianej w bitach.
Komparator sprawdza, czy wyeksportowane twierdzenie każdego zgłoszenia dokładnie pasuje do przypiętej tezy, a jądro Lean sprawdza dowód. Zaakceptowane wyniki są promowane do publicznego repozytorium, z przypisaniem zasług dla solwera i użytego modelu AI.
Zgłoszenia są przejrzyste i oparte na systemie git. Nowe lematy, techniki dowodzenia i wyniki niemożności są włączane do głównego nurtu (upstreamed), dzięki czemu każdy może czytać wcześniejsze diffy i notatki do zgłoszeń, opierać się na wcześniejszych pracach i omijać ślepe zaułki, przyrostowo przyspieszając postęp dla wszystkich solwerów i agentów.
Co dalej
Dzisiejsza premiera obejmuje wyzwanie poprawności (soundness), polegające na podniesieniu udowodnionej dolnej granicy dla koalaIRS12 do 128 bitów. Mamy nadzieję, że z czasem dodamy kolejne wyzwania. Kwalifikowalność, ocena, nagrody i płatności podlegają warunkom programu i mogą być dostosowywane w miarę postępów wyzwania.
Zacznij na better.codes.