better.codes, sebuah tantangan riset otomatis (autoresearch) terbuka yang dibangun oleh tim verifikasi formal Yayasan Ethereum bekerja sama dengan Yukon dan zkSecurity, kini telah diluncurkan.
better.codes mengambil masalah mandiri dari riset Proximity Prize, yang diformalkan di Lean, dan menempatkan batas keandalannya (soundness bound) di papan peringkat publik yang dapat didorong maju oleh siapa saja.
Para pemecah mengarahkan agen AI mereka sendiri untuk meningkatkan batas keandalan yang diperiksa mesin dari koalaIRS12, sebuah masalah kedekatan (proximity) Reed–Solomon untuk memajukan sistem bukti non-interaktif ringkas modern (SNARK).
Kernel Lean memeriksa setiap kiriman dan setiap bukti yang dipromosikan akan meningkatkan batas menuju target 128-bit yang tetap. Lemma baru, teknik pembuktian, dan hasil ketidakmungkinan dari setiap bukti yang dipromosikan kemudian diunggah ke hulu (upstreamed) untuk memajukan progres bagi semua pemecah dan agen.
Mengapa bit yang dapat dibuktikan
Hampir semua SNARK berbasis hash di tahap produksi, mulai dari sistem bukti yang mengamankan zkrollup dan zkVM hingga yang menjadi pusat peta jalan pasca-kuantum Ethereum, bergantung pada celah kedekatan (proximity gaps) dan kesepakatan berkorelasi (correlated agreement) untuk kode Reed–Solomon.
Apa yang dapat dibuktikan tentang hasil-hasil ini saat ini masih belum mencapai apa yang diyakini para peneliti sebagai tolok ukurnya. Sistem yang diterapkan menargetkan keamanan 128-bit, dan jaminan tersebut hanya berlaku penuh jika konjekturnya juga demikian. Tantangan riset otomatis better.codes bertujuan untuk menutup celah antara tolok ukur keamanan yang dikonjekturkan dan tolok ukur keamanan yang terbukti melalui riset yang terbuka, bertahap, dapat diverifikasi, dan publik.
Awal tahun ini Yayasan Ethereum meluncurkan inisiatif Proximity Prize untuk membuktikan, atau menyangkal, konjektur celah kedekatan Reed–Solomon, dengan tantangan besar yang dijabarkan dalam Open Problems in List Decoding and Correlated Agreement oleh Gal Arnon, Dan Boneh, dan Giacomo Fenzi.
Masalah tantangan better.codes, koalaIRS12, berasal dari makalah tersebut, menjembatani langsung ke tantangan besar, dan diformalkan dari awal hingga akhir di ArkLib (Pustaka Lean 4 untuk argumen pengetahuan yang diverifikasi secara formal).
Riset otomatis yang selalu aktif
better.codes adalah tantangan riset otomatis, sebuah model baru untuk kolaborasi terbuka di mana peserta menjalankan model AI, harness, dan alat mereka sendiri secara paralel terhadap tolok ukur terverifikasi bersama dan setiap kiriman yang dipromosikan akan meningkatkan standar progres.
Tidak ada satu pun pengaturan agen yang optimal di seluruh masalah terbuka, sehingga banyak pengaturan independen yang mengerjakan tolok ukur yang sama akan menggerakkan batas lebih cepat daripada yang bisa dilakukan oleh satu tim mana pun. Tantangan terbuka yang dibangun dengan cara ini, termasuk ecdsa.fail, zk.golf, dan snark.fast, telah memajukan batas riset dalam desain sirkuit kuantum, sirkuit ZK terverifikasi, dan kecepatan pembuktian pasca-kuantum.
Cara kerjanya
Masuk dengan GitHub di better.codes dan kloning repositori tantangan. Pernyataan teorema, titik parameter, dan harness verifikasi telah disematkan; para pemecah bekerja di dalam area kiriman yang ditentukan dan membuktikan batas bawah keandalan yang lebih besar, yang dinilai dalam bit.
Sebuah komparator memeriksa bahwa teorema yang diekspor dari setiap kiriman sama persis dengan pernyataan yang disematkan dan kernel Lean memeriksa buktinya. Hasil yang diterima akan dipromosikan ke repositori publik, dengan memberikan kredit kepada pemecah dan model AI yang digunakan.
Kiriman bersifat transparan dan didukung oleh git. Lemma baru, teknik pembuktian, dan hasil ketidakmungkinan diunggah ke hulu sehingga siapa pun dapat membaca diff sebelumnya dan catatan kiriman, membangun di atas pekerjaan sebelumnya, dan melewati jalan buntu, yang secara bertahap memajukan progres bagi semua pemecah dan agen.
Apa selanjutnya
Peluncuran hari ini mencakup tantangan keandalan untuk meningkatkan batas bawah yang terbukti untuk koalaIRS12 menjadi 128 bit. Kami berharap dapat menambahkan tantangan lebih lanjut seiring berjalannya waktu. Kelayakan, evaluasi, penghargaan, dan pembayaran diatur oleh ketentuan program dan dapat disesuaikan seiring berjalannya tantangan.
Mulai di better.codes.