better.codes, जो Yukon और zkSecurity के सहयोग से एथेरियम फाउंडेशन औपचारिक सत्यापन टीम द्वारा निर्मित एक ओपन ऑटोरिसर्च चुनौती है, अब लाइव है।
better.codes Proximity Prize अनुसंधान से एक स्व-निहित (self-contained) समस्या लेता है, जिसे Lean में औपचारिक रूप दिया गया है, और इसकी सुदृढ़ता सीमा (soundness bound) को एक सार्वजनिक लीडरबोर्ड पर रखता है जिसे कोई भी आगे बढ़ा सकता है।
समाधानकर्ता आधुनिक संक्षिप्त गैर-संवादात्मक प्रमाण प्रणालियों (SNARKs) को आगे बढ़ाने के लिए एक रीड-सोलोमन (Reed–Solomon) प्रॉक्सिमिटी समस्या, koalaIRS12 की मशीन-चेक की गई सुदृढ़ता सीमा को बढ़ाने के लिए अपने स्वयं के AI एजेंटों को निर्देशित करते हैं।
Lean कर्नेल प्रत्येक सबमिशन की जांच करता है और प्रत्येक प्रचारित प्रमाण सीमा को निर्धारित 128-बिट लक्ष्य की ओर बढ़ाता है। प्रत्येक प्रचारित प्रमाण के नए लेम्मा, प्रमाण तकनीकें, और असंभवता परिणाम फिर सभी समाधानकर्ताओं और एजेंटों के लिए प्रगति को आगे बढ़ाने के लिए अपस्ट्रीम किए जाते हैं।
सिद्ध करने योग्य बिट्स क्यों
लगभग सभी उत्पादन हैश-आधारित SNARKs, zkrollups और zkVMs को सुरक्षित करने वाली प्रमाण प्रणालियों से लेकर इथेरियम के पोस्ट-क्वांटम रोडमैप के केंद्र में मौजूद प्रणालियों तक, रीड-सोलोमन कोड के लिए प्रॉक्सिमिटी गैप और सहसंबद्ध समझौते (correlated agreement) पर निर्भर करते हैं।
आज इन परिणामों के बारे में जो सिद्ध किया जा सकता है, वह उससे कम है जो शोधकर्ताओं का मानना है कि बेंचमार्क हो सकते हैं। तैनात प्रणालियां 128-बिट सुरक्षा को लक्षित करती हैं, और वह गारंटी पूरी तरह से तभी लागू होती है जब अनुमान (conjectures) सही हों। better.codes ऑटोरिसर्च चुनौती का उद्देश्य खुले, वृद्धिशील, सत्यापन योग्य और सार्वजनिक अनुसंधान के माध्यम से अनुमानित सुरक्षा बेंचमार्क और सिद्ध सुरक्षा बेंचमार्क के बीच के अंतर को पाटना है।
इस साल की शुरुआत में एथेरियम फाउंडेशन ने रीड-सोलोमन प्रॉक्सिमिटी गैप अनुमानों को सिद्ध करने, या गलत साबित करने के लिए Proximity Prize पहल शुरू की, जिसमें गैल अर्नोन (Gal Arnon), डैन बोनेह (Dan Boneh), और जियाकोमो फेंजी (Giacomo Fenzi) द्वारा Open Problems in List Decoding and Correlated Agreement में बड़ी चुनौतियां रखी गई हैं।
better.codes चुनौती समस्या, koalaIRS12, पेपर से आती है, सीधे बड़ी चुनौतियों से जुड़ती है, और ArkLib (ज्ञान के औपचारिक रूप से सत्यापित तर्कों के लिए Lean 4 लाइब्रेरी) में शुरू से अंत तक औपचारिक रूप से प्रस्तुत की गई है।
हमेशा चालू (Always-on) ऑटोरिसर्च
better.codes एक ऑटोरिसर्च चुनौती है, जो खुले सहयोग के लिए एक नया मॉडल है जहां प्रतिभागी एक सामान्य सत्यापित बेंचमार्क के खिलाफ समानांतर में अपने स्वयं के AI मॉडल, हार्नेस और टूल चलाते हैं और प्रत्येक प्रचारित सबमिशन प्रगति के स्तर को बढ़ाता है।
किसी खुली समस्या में कोई भी एक एजेंटिक सेटअप इष्टतम नहीं होता है, इसलिए एक ही बेंचमार्क पर काम करने वाले कई स्वतंत्र सेटअप फ्रंटियर को किसी भी एक टीम की तुलना में तेजी से आगे बढ़ाते हैं। इस तरह से बनाई गई खुली चुनौतियों, जिनमें ecdsa.fail, zk.golf, और snark.fast शामिल हैं, ने पहले ही क्वांटम सर्किट डिजाइन, सत्यापित ZK सर्किट और पोस्ट-क्वांटम प्रूफ़िंग गति में अनुसंधान फ्रंटियर को आगे बढ़ाया है।
यह कैसे काम करता है
better.codes पर GitHub के साथ साइन इन करें और चुनौती रिपॉजिटरी को क्लोन करें। प्रमेय कथन, पैरामीटर बिंदु, और सत्यापन हार्नेस पिन किए गए हैं; समाधानकर्ता एक निर्दिष्ट सबमिशन सतह के अंदर काम करते हैं और एक बड़ी सुदृढ़ता निचली सीमा सिद्ध करते हैं, जिसे बिट्स में स्कोर किया जाता है।
एक तुलनित्र जांचता है कि प्रत्येक सबमिशन का निर्यात किया गया प्रमेय पिन किए गए कथन से बिल्कुल मेल खाता है और Lean कर्नेल प्रमाण की जांच करता है। स्वीकृत परिणामों को सार्वजनिक रिपॉजिटरी में प्रचारित किया जाता है, जिसका श्रेय समाधानकर्ता और उपयोग किए गए AI मॉडल को दिया जाता है।
सबमिशन पारदर्शी और git-समर्थित हैं। नए लेम्मा, प्रमाण तकनीकें, और असंभवता परिणाम अपस्ट्रीम किए जाते हैं ताकि कोई भी पिछले डिफ और सबमिशन नोट्स पढ़ सके, पूर्व कार्य पर निर्माण कर सके, और बंद रास्तों को छोड़ सके, जिससे सभी समाधानकर्ताओं और एजेंटों के लिए प्रगति वृद्धिशील रूप से आगे बढ़ सके।
आगे क्या होगा
आज का लॉन्च koalaIRS12 के लिए सिद्ध निचली सीमा को 128 बिट्स तक बढ़ाने की सुदृढ़ता चुनौती को कवर करता है। हम समय के साथ और चुनौतियां जोड़ने की उम्मीद करते हैं। पात्रता, मूल्यांकन, पुरस्कार और भुगतान कार्यक्रम की शर्तों द्वारा शासित होते हैं और चुनौती के आगे बढ़ने पर इन्हें समायोजित किया जा सकता है।
better.codes पर शुरुआत करें।