better.codes, हे Yukon आणि zkSecurity यांच्या सहकार्याने इथेरियम फाउंडेशन औपचारिक पडताळणी टीमने तयार केलेले एक ओपन ऑटोरिसर्च चॅलेंज आता लाईव्ह आहे.
better.codes हे Proximity Prize संशोधनातील एक स्वयंपूर्ण समस्या घेते, जी Lean मध्ये औपचारिक केली गेली आहे, आणि तिची साऊंडनेस बाउंड एका सार्वजनिक लीडरबोर्डवर ठेवते ज्याला कोणीही पुढे नेऊ शकते.
आधुनिक संक्षिप्त नॉन-इंटरॅक्टिव्ह प्रूफ सिस्टीम्स (SNARKs) प्रगत करण्यासाठी रीड-सोलोमन प्रॉक्सिमिटी समस्या असलेल्या koalaIRS12 ची मशीन-चेक केलेली साऊंडनेस बाउंड वाढवण्यासाठी सॉल्व्हर त्यांचे स्वतःचे AI एजंट्स निर्देशित करतात.
Lean कर्नल प्रत्येक सबमिशन तपासते आणि प्रत्येक प्रमोट केलेला पुरावा निश्चित केलेल्या 128-बिट लक्ष्याकडे बाउंड वाढवतो. प्रत्येक प्रमोट केलेल्या पुराव्याचे नवीन लेमा, प्रूफ तंत्र आणि अशक्यता परिणाम (impossibility results) नंतर सर्व सॉल्व्हर आणि एजंट्सच्या प्रगतीसाठी अपस्ट्रीम केले जातात.
सिद्ध करण्यायोग्य बिट्स का
zkrollups आणि zkVMs सुरक्षित करणाऱ्या प्रूफ सिस्टीम्सपासून ते इथेरियमच्या पोस्ट-क्वांटम रोडमॅपसाठी मध्यवर्ती असलेल्या जवळपास सर्व प्रोडक्शन हॅश-आधारित SNARKs, रीड-सोलोमन कोड्ससाठी प्रॉक्सिमिटी गॅप्स आणि कोरिलेटेड ॲग्रीमेंटवर अवलंबून असतात.
आज या परिणामांबद्दल जे सिद्ध केले जाऊ शकते ते संशोधकांच्या मते बेंचमार्क्स काय असू शकतात यापेक्षा कमी पडते. डिप्लॉय केलेल्या सिस्टीम्स 128-बिट सुरक्षेचे लक्ष्य ठेवतात, आणि ती हमी तेव्हाच पूर्णपणे टिकते जेव्हा अनुमाने (conjectures) टिकतात. better.codes ऑटोरिसर्च चॅलेंजचे उद्दिष्ट ओपन, वाढीव (incremental), पडताळणी करण्यायोग्य आणि सार्वजनिक संशोधनाद्वारे अनुमानित सुरक्षा बेंचमार्क्स आणि सिद्ध झालेल्या सुरक्षा बेंचमार्क्समधील अंतर कमी करणे हे आहे.
या वर्षाच्या सुरुवातीला इथेरियम फाउंडेशनने रीड-सोलोमन प्रॉक्सिमिटी गॅप्स अनुमाने सिद्ध करण्यासाठी किंवा खोडून काढण्यासाठी Proximity Prize initiative सुरू केले, ज्यामध्ये Gal Arnon, Dan Boneh आणि Giacomo Fenzi यांच्या Open Problems in List Decoding and Correlated Agreement मध्ये मांडलेली मोठी आव्हाने आहेत.
better.codes चॅलेंज समस्या, koalaIRS12, या पेपरमधून येते, थेट मोठ्या आव्हानांशी जोडते आणि ArkLib (ज्ञानाच्या औपचारिक पडताळणी केलेल्या युक्तिवादांसाठी Lean 4 लायब्ररी) मध्ये एंड-टू-एंड औपचारिक केली गेली आहे.
नेहमी-सुरू असलेले ऑटोरिसर्च
better.codes हे एक ऑटोरिसर्च चॅलेंज आहे, ओपन कोलॅबोरेशनचे एक नवीन मॉडेल जिथे सहभागी त्यांचे स्वतःचे AI मॉडेल्स, हार्नेसेस आणि टूल्स एका सामान्य पडताळणी केलेल्या बेंचमार्कच्या विरूद्ध समांतरपणे चालवतात आणि प्रत्येक प्रमोट केलेले सबमिशन प्रगतीची पातळी उंचावते.
कोणत्याही ओपन समस्येवर एकच एजंटिक सेटअप इष्टतम (optimal) नसतो, त्यामुळे एकाच बेंचमार्कवर काम करणारे अनेक स्वतंत्र सेटअप्स कोणत्याही एका टीमपेक्षा फ्रंटियर्स अधिक वेगाने पुढे नेतात. अशा प्रकारे तयार केलेल्या ओपन चॅलेंजेसनी, ज्यामध्ये ecdsa.fail, zk.golf, आणि snark.fast यांचा समावेश आहे, क्वांटम सर्किट डिझाइन, पडताळणी केलेले ZK सर्किट्स आणि पोस्ट-क्वांटम प्रूव्हिंग स्पीडमधील संशोधन फ्रंटियर्स आधीच पुढे नेले आहेत.
हे कसे काम करते
better.codes वर GitHub सह साइन इन करा आणि चॅलेंज रिपॉझिटरी क्लोन करा. प्रमेय विधान (theorem statement), पॅरामीटर पॉईंट आणि व्हेरिफिकेशन हार्नेस पिन केलेले आहेत; सॉल्व्हर एका नियुक्त केलेल्या सबमिशन पृष्ठभागाच्या आत काम करतात आणि बिट्समध्ये स्कोअर केलेली मोठी साऊंडनेस लोअर बाउंड सिद्ध करतात.
एक कंपॅरेटर तपासतो की प्रत्येक सबमिशनचे एक्सपोर्ट केलेले प्रमेय पिन केलेल्या विधानाशी तंतोतंत जुळते आणि Lean कर्नल पुराव्याची तपासणी करते. स्वीकारलेले परिणाम सार्वजनिक रिपॉझिटरीमध्ये प्रमोट केले जातात, ज्याचे श्रेय सॉल्व्हर आणि वापरलेल्या AI मॉडेलला दिले जाते.
सबमिशन्स पारदर्शक आणि git-बॅक्ड आहेत. नवीन लेमा, प्रूफ तंत्र आणि अशक्यता परिणाम अपस्ट्रीम केले जातात जेणेकरून कोणीही मागील diffs आणि सबमिशन नोट्स वाचू शकेल, पूर्वीच्या कामावर आधारित पुढील काम करू शकेल आणि डेड एंड्स टाळू शकेल, ज्यामुळे सर्व सॉल्व्हर आणि एजंट्ससाठी प्रगती वाढीवपणे पुढे जाईल.
पुढे काय
आजच्या लाँचमध्ये koalaIRS12 साठी सिद्ध झालेली लोअर बाउंड 128 बिट्सपर्यंत वाढवण्याचे साऊंडनेस चॅलेंज समाविष्ट आहे. आम्हाला आशा आहे की कालांतराने आणखी आव्हाने जोडली जातील. पात्रता, मूल्यमापन, पुरस्कार आणि पेमेंट्स प्रोग्रामच्या अटींद्वारे नियंत्रित केले जातात आणि चॅलेंज जसजसे पुढे जाईल तसतसे त्यात बदल केले जाऊ शकतात.
better.codes वरून सुरुवात करा.