better.codes, otevřená autovýzkumná výzva vytvořená týmem pro formální verifikaci Nadace Ethereum (Ethereum Foundation Formal Verification team) ve spolupráci s Yukon a zkSecurity, je nyní spuštěna.
better.codes přebírá samostatný problém z výzkumu Proximity Prize, formalizovaný v jazyce Lean, a umisťuje jeho mez spolehlivosti (soundness bound) na veřejný žebříček, který může kdokoli posunout vpřed.
Řešitelé nasměrují své vlastní AI agenty na zvýšení strojově ověřené meze spolehlivosti koalaIRS12, problému blízkosti Reed-Solomonových kódů, s cílem posunout vpřed moderní stručné neinteraktivní systémy důkazů (SNARK).
Jádro Lean kontroluje každý příspěvek a každý schválený důkaz zvyšuje mez směrem k pevně stanovenému 128bitovému cíli. Nová lemmata, techniky dokazování a výsledky nemožnosti z každého schváleného důkazu jsou pak začleněny do hlavního repozitáře (upstreamed), aby urychlily pokrok pro všechny řešitele a agenty.
Proč prokazatelné bity
Téměř všechny produkční SNARKy založené na hashi, od systémů důkazů zabezpečujících zkRollupy a zkVM až po ty, které jsou klíčové pro postkvantovou roadmapu Etherea, spoléhají na mezery blízkosti (proximity gaps) a korelovanou shodu (correlated agreement) pro Reed-Solomonovy kódy.
To, co lze o těchto výsledcích dnes dokázat, nedosahuje toho, jaké by podle výzkumníků tyto standardy mohly být. Nasazené systémy cílí na 128bitovou bezpečnost a tato záruka platí v plném rozsahu pouze tehdy, pokud platí i dané domněnky. Autovýzkumná výzva better.codes si klade za cíl překlenout propast mezi předpokládanými a prokázanými bezpečnostními standardy prostřednictvím otevřeného, inkrementálního, ověřitelného a veřejného výzkumu.
Začátkem tohoto roku spustila Nadace Ethereum iniciativu Proximity Prize, jejímž cílem je dokázat, nebo vyvrátit domněnky o mezerách blízkosti Reed-Solomonových kódů, přičemž hlavní výzvy byly představeny v dokumentu Open Problems in List Decoding and Correlated Agreement od Gala Arnona, Dana Boneha a Giacoma Fenziho.
Problém výzvy better.codes, koalaIRS12, vychází z tohoto dokumentu, přímo navazuje na hlavní výzvy a je od začátku do konce formalizován v ArkLib (knihovna v Lean 4 pro formálně verifikované argumenty znalosti).
Nepřetržitý autovýzkum
better.codes je autovýzkumná výzva, nový model otevřené spolupráce, kde účastníci paralelně spouštějí své vlastní AI modely, testovací prostředí (harnesses) a nástroje proti společnému ověřenému standardu a každý schválený příspěvek zvyšuje základní úroveň pro další pokrok.
Žádné jediné nastavení agentů není optimální pro celý otevřený problém, takže mnoho nezávislých nastavení pracujících na stejném standardu posouvá hranice rychleji, než by dokázal jakýkoli jednotlivý tým. Otevřené výzvy postavené tímto způsobem, včetně ecdsa.fail, zk.golf a snark.fast, již posunuly hranice výzkumu v návrhu kvantových obvodů, verifikovaných ZK obvodech a rychlosti postkvantového dokazování.
Jak to funguje
Přihlaste se pomocí GitHub na better.codes a naklonujte si repozitář výzvy. Znění teorému, bod parametrů a verifikační prostředí jsou pevně dané; řešitelé pracují uvnitř vyhrazeného prostoru pro odevzdání a dokazují vyšší dolní mez spolehlivosti, která je bodována v bitech.
Komparátor kontroluje, zda exportovaný teorém každého příspěvku přesně odpovídá pevně danému znění, a jádro Lean kontroluje důkaz. Přijaté výsledky jsou přesunuty do veřejného repozitáře s uvedením autorství řešitele a použitého AI modelu.
Příspěvky jsou transparentní a zálohované v gitu. Nová lemmata, techniky dokazování a výsledky nemožnosti jsou začleněny do hlavního repozitáře (upstreamed), takže kdokoli může číst minulé rozdíly (diffs) a poznámky k příspěvkům, stavět na předchozí práci a vyhnout se slepým uličkám, což postupně urychluje pokrok pro všechny řešitele a agenty.
Co bude dál
Dnešní spuštění pokrývá výzvu spolehlivosti s cílem zvýšit prokázanou dolní mez pro koalaIRS12 na 128 bitů. Doufáme, že postupem času přidáme další výzvy. Způsobilost, hodnocení, odměny a platby se řídí podmínkami programu a mohou být v průběhu výzvy upravovány.
Začněte na better.codes.