Ethereum Foundation: startuje better.codes, wyścig agentów AI o bezpieczeństwo SNARK-ów

Ethereum Foundation wraz z Yukon i zkSecurity uruchomiła better.codes – otwarte wyzwanie typu autoresearch, w którym agenci AI rywalizują o podniesienie zweryfikowanego maszynowo limitu bezpieczeństwa dla problemu koalaIRS12. Problem ten dotyczy luk w dowodach bliskości dla kodów Reeda-Solomona i leży u podstaw nowoczesnych systemów dowodów zwięzłych (SNARK), w tym tych zabezpieczających rollupy i przyszłą postkwantową ścieżkę Ethereum.

Problem: 128-bitowe bezpieczeństwo opiera się na nieudowodnionych założeniach

Współczesne hash-based SNARK-i – od systemów dowodowych stojących za zk-rollupami i zkVM, po te kluczowe dla postkwantowej mapy drogowej Ethereum – polegają na własnościach matematycznych zwanych lukami bliskości (proximity gaps) i skorelowaną zgodnością dla kodów Reeda-Solomona. Wdrożone systemy celują w 128-bitowy poziom bezpieczeństwa, jednak gwarancja ta jest w pełni ważna tylko wtedy, gdy prawdziwe są matematyczne przypuszczenia, których dotąd nie udowodniono.

Luka między zakładanym a udowodnionym poziomem bezpieczeństwa stała się na tyle istotna, że na początku roku EF ogłosiła inicjatywę Proximity Prize, zachęcającą do udowodnienia – lub obalenia – tych przypuszczeń. Fundamenty badawcze opisano w pracy Open Problems in List Decoding and Correlated Agreement autorstwa Gala Arnona, Dana Boneha i Giacomo Fenziego.

Jak działa better.codes: Lean, agenci i wspólny benchmark

better.codes to wyzwanie typu autoresearch – model otwartej współpracy, w którym uczestnicy uruchamiają własne modele AI równolegle wobec wspólnego, zweryfikowanego benchmarku. Każde zaakceptowane zgłoszenie podnosi poprzeczkę dla wszystkich. Problem koalaIRS12 został w całości sformalizowany w Lean 4 przy użyciu biblioteki ArkLib.

Mechanika jest przejrzysta: po zalogowaniu przez GitHub uczestnik klonuje repozytorium wyzwania. Twierdzenie, punkt parametryczny i harness weryfikacyjny są stałe. Solverzy pracują w wydzielonej przestrzeni zgłoszeniowej, udowadniając większe dolne ograniczenie bezpieczeństwa (soundness bound), punktowane w bitach. Komparator sprawdza zgodność wyeksportowanego twierdzenia ze wzorcem, a kernel Lean weryfikuje dowód. Zaakceptowane wyniki trafiają do publicznego repozytorium z przypisaniem do solvera i użytego modelu AI.

„Żadna pojedyncza konfiguracja agenta nie jest optymalna dla otwartego problemu, więc wiele niezależnych konfiguracji pracujących nad tym samym benchmarkiem przesuwa granicę szybciej niż jakikolwiek pojedynczy zespół.” – Ethereum Foundation

Nowe lematy, techniki dowodowe i wyniki niemożliwości są natychmiast upubliczniane (upstreamowane), dzięki czemu każdy może analizować wcześniejsze diffy, budować na istniejących rezultatach i omijać ślepe zaułki. Podobne otwarte wyzwania – ecdsa.fail, zk.golf czy snark.fast – już wcześniej przesunęły granice w projektowaniu obwodów kwantowych, weryfikowalnych obwodów ZK i szybkości dowodów postkwantowych.

Co dalej: 128 bitów i kolejne wyzwania

Dzisiejszy start obejmuje wyzwanie soundness, którego celem jest podniesienie udowodnionego dolnego ograniczenia dla koalaIRS12 do 128 bitów. EF zapowiada, że z czasem mogą pojawić się kolejne problemy. Zasady kwalifikowalności, oceny, nagród i płatności regulują warunki programu – mogą one ulegać zmianom w miarę postępu wyzwania. Start następuje natychmiast pod adresem better.codes.