أصبح تحدي البحث التلقائي المفتوح better.codes، الذي صممه فريق التحقق الشكلي في مؤسسة إيثيريوم بالتعاون مع Yukon وzkSecurity، متاحًا الآن.
يأخذ better.codes مشكلة قائمة بذاتها من بحث جائزة التقارب (Proximity Prize)، تمت صياغتها شكليًا في Lean، ويضع حد الموثوقية الخاص بها في لوحة صدارة عامة يمكن لأي شخص المساهمة في تحسينها.
يوجه المُحِلّون وكلاء الذكاء الاصطناعي الخاصين بهم نحو رفع حد الموثوقية المدقق آليًا لـ koalaIRS12، وهي مشكلة تقارب Reed–Solomon لتعزيز أنظمة الإثبات الحديثة الموجزة وغير التفاعلية (SNARKs).
تتحقق نواة Lean من كل إرسال، وكل إثبات يتم ترقيته يرفع الحد نحو الهدف الثابت البالغ 128-bit. بعد ذلك، يتم رفع المبرهنات الجديدة وتقنيات الإثبات ونتائج الاستحالة لكل إثبات تمت ترقيته لتعزيز التقدم لجميع المُحِلّين والوكلاء.
لماذا البتات القابلة للإثبات
تعتمد جميع تقنيات SNARKs القائمة على التجزئة في بيئات الإنتاج تقريبًا، بدءًا من أنظمة الإثبات التي تؤمن zkrollups وzkVMs إلى تلك المركزية في خارطة طريق إيثيريوم لما بعد الكم، على فجوات التقارب والاتفاق المترابط لرموز Reed–Solomon.
ما يمكن إثباته حول هذه النتائج اليوم يقف دون ما يعتقد الباحثون أن المعايير قد تكون عليه. تستهدف الأنظمة المنشورة أمانًا بمقدار 128-bit، وهذا الضمان يظل ساريًا بالكامل فقط إذا كانت التخمينات صحيحة. يهدف تحدي البحث التلقائي better.codes إلى سد الفجوة بين معايير الأمان المخمنة ومعايير الأمان المثبتة من خلال بحث مفتوح وتدريجي وقابل للتحقق وعام.
في وقت سابق من هذا العام، أطلقت مؤسسة إيثيريوم مبادرة جائزة التقارب (Proximity Prize) لإثبات، أو دحض، تخمينات فجوات تقارب Reed–Solomon، مع تحديات كبرى تم طرحها في المشكلات المفتوحة في فك تشفير القوائم والاتفاق المترابط بواسطة Gal Arnon وDan Boneh وGiacomo Fenzi.
تأتي مشكلة تحدي better.codes، وهي koalaIRS12، من الورقة البحثية، وترتبط مباشرة بالتحديات الكبرى، وتمت صياغتها شكليًا من البداية إلى النهاية في ArkLib (مكتبة Lean 4 لحجج المعرفة التي تم التحقق منها شكليًا).
بحث تلقائي دائم التشغيل
يُعد better.codes تحديًا للبحث التلقائي، وهو نموذج جديد للتعاون المفتوح حيث يقوم المشاركون بتشغيل نماذج الذكاء الاصطناعي وأدوات الاختبار والأدوات الخاصة بهم بالتوازي مقابل معيار مشترك تم التحقق منه، وكل إرسال يتم ترقيته يرفع الحد الأدنى للتقدم.
لا يوجد إعداد وكيل واحد مثالي عبر مشكلة مفتوحة، لذا فإن العديد من الإعدادات المستقلة التي تعمل على نفس المعيار تحرك الحدود بشكل أسرع مما يمكن لأي فريق واحد القيام به. التحديات المفتوحة المبنية بهذه الطريقة، بما في ذلك ecdsa.fail وzk.golf وsnark.fast، قد حركت بالفعل حدود البحث في تصميم الدوائر الكمومية، ودوائر المعرفة الصفرية (ZK) التي تم التحقق منها، وسرعة الإثبات لما بعد الكم.
كيف يعمل
قم بتسجيل الدخول باستخدام GitHub في better.codes واستنسخ مستودع التحدي. يتم تثبيت بيان المبرهنة ونقطة المعلمة وأداة التحقق؛ يعمل المُحِلّون داخل مساحة إرسال مخصصة ويثبتون حدًا أدنى أكبر للموثوقية، ويتم تسجيل النقاط بالبتات.
تتحقق أداة المقارنة من أن المبرهنة المُصدَّرة لكل إرسال تتطابق تمامًا مع البيان المثبت، وتتحقق نواة Lean من الإثبات. يتم ترقية النتائج المقبولة إلى المستودع العام، وتُنسب إلى المُحِلّ ونموذج الذكاء الاصطناعي المستخدم.
عمليات الإرسال شفافة ومدعومة بـ git. يتم رفع المبرهنات الجديدة وتقنيات الإثبات ونتائج الاستحالة بحيث يمكن لأي شخص قراءة الفروق السابقة وملاحظات الإرسال، والبناء على العمل السابق، وتخطي الطرق المسدودة، مما يعزز التقدم تدريجيًا لجميع المُحِلّين والوكلاء.
ماذا بعد
يغطي إطلاق اليوم تحدي الموثوقية لرفع الحد الأدنى المثبت لـ koalaIRS12 إلى 128 bits. نأمل في إضافة المزيد من التحديات بمرور الوقت. تخضع الأهلية والتقييم والجوائز والمدفوعات لشروط البرنامج وقد يتم تعديلها مع تقدم التحدي.
ابدأ في better.codes.