Ethereum Vakfı Biçimsel Doğrulama ekibi tarafından Yukon ve zkSecurity iş birliğiyle oluşturulan açık bir otomatik araştırma yarışması olan better.codes yayında.
better.codes, Proximity Prize araştırmasından Lean'de biçimselleştirilmiş bağımsız bir problemi ele alıyor ve bunun sağlamlık sınırını herkesin ileriye taşıyabileceği, herkese açık bir liderlik tablosuna yerleştiriyor.
Çözücüler, modern kısa ve öz etkileşimsiz ispat sistemlerini (SNARK'lar) ilerletmek için bir Reed-Solomon yakınlık problemi olan koalaIRS12'nin makine onaylı sağlamlık sınırını yükseltmek üzere kendi yapay zeka ajanlarını yönlendiriyor.
Lean çekirdeği her gönderimi kontrol eder ve onaylanan her ispat, sınırı sabit 128 bitlik hedefe doğru yükseltir. Onaylanan her ispatın yeni lemmaları, ispat teknikleri ve imkansızlık sonuçları daha sonra tüm çözücüler ve ajanlar için ilerlemeyi hızlandırmak amacıyla ana kaynağa aktarılır.
Neden kanıtlanabilir bitler
zk-rollup'ları ve zkVM'leri güvence altına alan ispat sistemlerinden Ethereum'un kuantum sonrası yol haritasının merkezinde yer alanlara kadar, üretim ortamındaki hash tabanlı SNARK'ların neredeyse tamamı, Reed-Solomon kodları için yakınlık boşluklarına ve ilişkili mutabakata dayanır.
Bugün bu sonuçlar hakkında kanıtlanabilenler, araştırmacıların kriterlerin olabileceğine inandığı seviyenin gerisinde kalıyor. Dağıtılan sistemler 128 bit güvenliği hedefler ve bu garanti ancak varsayımlar doğruysa tam olarak geçerlidir. better.codes otomatik araştırma yarışması; açık, artımlı, doğrulanabilir ve herkese açık araştırmalar yoluyla varsayılan güvenlik kriterleri ile kanıtlanmış güvenlik kriterleri arasındaki boşluğu kapatmayı amaçlamaktadır.
Bu yılın başlarında Ethereum Vakfı, Gal Arnon, Dan Boneh ve Giacomo Fenzi tarafından Open Problems in List Decoding and Correlated Agreement adlı eserde ortaya konan büyük zorluklarla birlikte, Reed-Solomon yakınlık boşlukları varsayımlarını kanıtlamak veya çürütmek için Proximity Prize girişimini başlattı.
better.codes yarışma problemi koalaIRS12, makaleden gelmektedir, doğrudan büyük zorluklarla bağlantı kurar ve ArkLib'de (biçimsel olarak doğrulanmış bilgi argümanları için Lean 4 kütüphanesi) uçtan uca biçimselleştirilmiştir.
Her zaman aktif otomatik araştırma
better.codes, katılımcıların kendi yapay zeka modellerini, test ortamlarını ve araçlarını ortak ve doğrulanmış bir kritere karşı paralel olarak çalıştırdığı ve onaylanan her gönderimin ilerleme için tabanı yükselttiği, açık iş birliğine yönelik yeni bir model olan bir otomatik araştırma yarışmasıdır.
Açık bir problemde hiçbir tekil ajan kurulumu optimal değildir, bu nedenle aynı kriter üzerinde çalışan birçok bağımsız kurulum, sınırı herhangi bir ekibin yapabileceğinden daha hızlı ileri taşır. ecdsa.fail, zk.golf ve snark.fast dahil olmak üzere bu şekilde oluşturulan açık yarışmalar; kuantum devre tasarımı, doğrulanmış ZK devreleri ve kuantum sonrası ispat hızındaki araştırma sınırlarını halihazırda ileri taşımıştır.
Nasıl çalışır
better.codes adresinde GitHub ile giriş yapın ve yarışma deposunu klonlayın. Teorem ifadesi, parametre noktası ve doğrulama test ortamı sabitlenmiştir; çözücüler belirlenmiş bir gönderim alanı içinde çalışır ve bit cinsinden puanlanan daha büyük bir sağlamlık alt sınırını kanıtlar.
Bir karşılaştırıcı, her gönderimin dışa aktarılan teoreminin sabitlenmiş ifadeyle tam olarak eşleştiğini kontrol eder ve Lean çekirdeği ispatı kontrol eder. Kabul edilen sonuçlar herkese açık depoya aktarılır, çözücüye ve kullanılan yapay zeka modeline atfedilir.
Gönderimler şeffaftır ve git desteklidir. Yeni lemmalar, ispat teknikleri ve imkansızlık sonuçları ana kaynağa aktarılır; böylece herkes geçmiş farkları (diffs) ve gönderim notlarını okuyabilir, önceki çalışmaların üzerine inşa edebilir ve çıkmaz sokakları atlayarak tüm çözücüler ve ajanlar için ilerlemeyi kademeli olarak artırabilir.
Sırada ne var
Bugünkü lansman, koalaIRS12 için kanıtlanmış alt sınırı 128 bite çıkarmaya yönelik sağlamlık yarışmasını kapsamaktadır. Zamanla daha fazla yarışma eklemeyi umuyoruz. Uygunluk, değerlendirme, ödüller ve ödemeler program şartlarına tabidir ve yarışma ilerledikçe ayarlanabilir.
better.codes adresinden başlayın.