اقترح الشريك المؤسس لعملة إيثيريوم فيتاليك بوتيرين لغة برمجة جديدة ستكون مترجمة مباشرة إلى Lean أو HOL، وهو مساعد إثبات رسمي آخر.
يستهدف هذا الاقتراح فجوة محددة في كيفية قراءة الأشخاص لمخرجات الذكاء الاصطناعي. ينتج الذكاء الاصطناعي بشكل متزايد كتلًا ضخمة من الإثباتات الآلية، وغالبًا أسرع مما يمكن لأي فريق بشري كتابتها يدويًا. لا يستطيع سوى عدد قليل من القراء التأكد بسرعة مما تثبته هذه الإثباتات بالفعل.
لغة تم بناؤها فقط لمدققي الإثباتات بالذكاء الاصطناعي
اعتمد على Lean كمساعد إثبات، وهو برنامج يستخدمه الرياضيون والمهندسون لكتابة إثباتات يمكن للكمبيوتر التحقق منها سطرًا بسطر. يعتمد باحثو عملة إيثيريوم عليه بالفعل للتحقق من التعليمات البرمجية التشفيرية ومنطق التوافق. ورغم أن مساعدي الإثبات موجودون منذ نحو 60 عامًا، إلا أن هذا المجال ظل تخصصًا ضيقًا.
في تدوينته نشر بوتيرين أن خطوات الإثبات الداخلية تحمل مطلبًا واحدًا فقط، وهو الصواب الرياضي ولا شيء غير ذلك. لا يقوم القراء أبدًا بفحص تلك الآلية بشكل مباشر. تعمل التعريفات والنظريات بشكل مختلف، لأن البشر يقرأون هذه الأجزاء لمعرفة ما الذي يضمنه البرنامج فعليًا.
تناول بوتيرين انقسامًا مشابهًا في تدوينة في مايو. في هذا المثال، يوضح إثبات رياضي أن الشيفرة منخفضة المستوى الفعّالة تتطابق مع مواصفات منفصلة وقابلة للقراءة، بحيث يغطي تدقيق واحد كلتا النسختين في وقت واحد.
واكبت توقيته أيضًا جهود إعادة بناء عملة إيثيريوم، التي تحمل لقبًا منفصلًا وهو خارطة طريق Lean لعملة إيثيريوم. في نفس الوقت، يعمل الباحثون على بناء ZK-EVM مُثبت رسميًا، وهو إصدار قابل للإثبات بالمعرفة الصفرية من آلة إيثيريوم الافتراضية (EVM)، باستخدام طرق مماثلة.
يكتب الذكاء الاصطناعي الإثباتات ويدقق البشر الادعاءات
تستطيع النماذج اللغوية الكبيرة بالفعل كتابة إثباتات Lean قابلة للاستخدام. ذكر بوتيرين أن كلود و Deepseek 4 Pro أدوات قادرة على ذلك، بجانب Leanstral، وهو نموذج أصغر مُعدل خصيصًا لبرنامج Lean. أحد المشاريع المثالية هو evm-asm، وهو تطبيق EVM تم التحقق منه مقابل مرجع قابل للقراءة. تعكس هذه القدرة مهارات التفكير المنطقي التي عرضها المطورون في تحدي الذكاء الاصطناعي الأخير لبوتيرين. حل المختبرون هذا التحدي خلال ساعات.
تتجاوز المخاطر حدود الراحة فقط، فقد راقب الباحثون الأمنيون ارتفاعًا في محاولات الاستغلال بمساعدة الذكاء الاصطناعي هذا العام. يوفر الكود المثبت رسميًا وسيلة دفاع ضد هذا الاتجاه. ستتيح لغة المواصفات الأكثر وُدية للمطورين تدقيق الادعاءات دون الخوض في الإثبات المحيط بها.
خارج دوائر بحث عملة إيثيريوم
يواصل بوتيرين اختبار هذه الأفكار علنًا حيث قام مؤخرًا بعرض لوحة إعلانات مجهولة الهوية تم إنشاؤها باستخدام براهين المعرفة الصفرية. أظهر العرض كيف يمكن نقل الادعاءات القابلة للتحقق من مستودعات البحث إلى المنتجات العملية. بدأ الباحثون أيضًا بالتحقق الرسمي من عملاء الإجماع في Lean لاكتشاف الأخطاء في وقت مبكر.
مع ذلك، تعكس الاتجاه نمطًا مألوفًا: فصل الشيفرة السريعة عن الادعاءات القابلة للقراءة، ثم إثبات أن الاثنين متطابقان.
لا يوجد بعد نموذج أولي للغة الجديدة، وترك بوتيرين صياغتها الدقيقة مفتوحة. قد يتوافق المطورون على معيار واحد مشترك، أو يكتفون بعدة لهجات غير متوافقة. يمكن أن يحدد هذا الخيار مدى سرعة وصول الشيفرة التي تم التحقق منها بالذكاء الاصطناعي إلى أنظمة الإنتاج.
