better.codes, una sfida aperta di autoricerca creata dal team di verifica formale della Fondazione Ethereum in collaborazione con Yukon e zkSecurity, è ora online.
better.codes prende un problema autonomo dalla ricerca del Proximity Prize, formalizzato in Lean, e inserisce il suo limite di solidità in una classifica pubblica che chiunque può far avanzare.
I risolutori indirizzano i propri agenti IA per innalzare il limite di solidità verificato dalle macchine di koalaIRS12, un problema di prossimità di Reed-Solomon per far progredire i moderni sistemi di prova succinti e non interattivi (SNARK).
Il kernel di Lean controlla ogni invio e ogni prova promossa innalza il limite verso l'obiettivo fisso a 128 bit. I nuovi lemmi, le tecniche di prova e i risultati di impossibilità di ogni prova promossa vengono poi integrati a monte per favorire il progresso di tutti i risolutori e gli agenti.
Perché i bit dimostrabili
Quasi tutti gli SNARK basati su hash in produzione, dai sistemi di prova che proteggono gli zk-rollup e le zkVM a quelli centrali per la roadmap post-quantistica di Ethereum, si basano sui gap di prossimità e sull'accordo correlato per i codici di Reed-Solomon.
Ciò che può essere dimostrato oggi su questi risultati si ferma prima di quelli che i ricercatori ritengono possano essere i benchmark. I sistemi distribuiti puntano a una sicurezza a 128 bit, e tale garanzia è pienamente valida solo se lo sono anche le congetture. La sfida di autoricerca better.codes mira a colmare il divario tra i benchmark di sicurezza congetturati e i benchmark di sicurezza dimostrati attraverso una ricerca aperta, incrementale, verificabile e pubblica.
All'inizio di quest'anno la Fondazione Ethereum ha lanciato l'iniziativa Proximity Prize per dimostrare, o confutare, le congetture sui gap di prossimità di Reed-Solomon, con grandi sfide esposte in Open Problems in List Decoding and Correlated Agreement da Gal Arnon, Dan Boneh e Giacomo Fenzi.
Il problema della sfida better.codes, koalaIRS12, proviene dal documento, si collega direttamente alle grandi sfide ed è formalizzato da un capo all'altro in ArkLib (la libreria Lean 4 per argomenti di conoscenza verificati formalmente).
Autoricerca sempre attiva
better.codes è una sfida di autoricerca, un nuovo modello di collaborazione aperta in cui i partecipanti eseguono i propri modelli IA, harness e strumenti in parallelo rispetto a un benchmark verificato comune e ogni invio promosso innalza la base per il progresso.
Nessuna singola configurazione basata su agenti è ottimale per un problema aperto, quindi molte configurazioni indipendenti che lavorano sullo stesso benchmark spostano la frontiera più velocemente di quanto possa fare un singolo team. Le sfide aperte costruite in questo modo, tra cui ecdsa.fail, zk.golf e snark.fast, hanno già spostato le frontiere della ricerca nella progettazione di circuiti quantistici, nei circuiti ZK verificati e nella velocità di prova post-quantistica.
Come funziona
Accedi con GitHub su better.codes e clona il repository della sfida. L'enunciato del teorema, il punto del parametro e l'harness di verifica sono fissati; i risolutori lavorano all'interno di una superficie di invio designata e dimostrano un limite inferiore di solidità maggiore, valutato in bit.
Un comparatore verifica che il teorema esportato di ogni invio corrisponda esattamente all'enunciato fissato e il kernel di Lean controlla la prova. I risultati accettati vengono promossi nel repository pubblico, accreditati al risolutore e al modello IA utilizzato.
Gli invii sono trasparenti e supportati da git. I nuovi lemmi, le tecniche di prova e i risultati di impossibilità vengono integrati a monte in modo che chiunque possa leggere i diff passati e le note di invio, basarsi sul lavoro precedente e saltare i vicoli ciechi, facendo avanzare in modo incrementale il progresso per tutti i risolutori e gli agenti.
Cosa ci aspetta
Il lancio di oggi riguarda la sfida di solidità per innalzare il limite inferiore dimostrato per koalaIRS12 a 128 bit. Speriamo di aggiungere ulteriori sfide nel tempo. L'idoneità, la valutazione, i premi e i pagamenti sono regolati dai termini del programma e potrebbero essere modificati con l'avanzare della sfida.
Inizia su better.codes.