فيتاليك بوتيرين يقترح لغة جديدة لتحسين قابلية قراءة إثبات الذكاء الاصطناعي

المؤسس المشارك لإيثيريوم فيتاليك بوترين اقترح لغة برمجة جديدة. ستُترجم مباشرة إلى Lean أو HOL، وهو مساعد إثبات رسمي آخر.

يستهدف هذا المفهوم فجوة محددة في كيفية قراءة الناس لمخرجات الذكاء الاصطناعي. ينتج الذكاء الاصطناعي بشكل متزايد كتل كبيرة من الإثباتات الآلية، غالبًا بأسرع من أي فريق بشري يمكنه كتابتها يدويًا. قلة من القراء يمكنهم التحقق بسرعة مما تُثبت هذه الإثباتات فعليًا.

Lean هو مساعد إثبات، وهو برنامج يستخدمه الرياضيون والمهندسون لكتابة إثباتات يمكن للحاسوب التحقق منها سطرًا بسطر. يستخدم باحثو إيثريوم بالفعل هذا البرنامج للتحقق من الشيفرة التشفيرية ومنطق التوافق. لقد existed مساعدو الإثبات منذ حوالي 60 عامًا، لكن المجال ظل ممارسة متخصصة.

في منشوره post، جادل بوتيرين أن الخطوات الداخلية لإثبات ما تمتلكه من متطلب واحد فقط. هذا المتطلب هو الصيغة الرياضية الصحيحة، ولا شيء أكثر. لا يفحص القراء هذه الآلية مباشرة. تعمل التعريفات والنظريات بشكل مختلف، لأن البشر يقرأون هذه الأجزاء ليفهموا ما الذي تضمنه قطعة البرنامج فعليًا.

استكشف بوتيرين انقسامًا ذا صلة في مدونة blog في مايو. هناك، يُظهر إثبات رياضي أن الكود منخفض المستوى الفعال يتوافق مع مواصفات منفصلة وسهلة القراءة، لذا فإن مراجعة واحدة تغطي كلا النسختين معًا.

يتوافق توقيته أيضًا مع جهود إعادة بناء إيثريوم الخاصة، التي تحمل لقبًا منفصلًا، وهو خريطة طريق إيثريوم الرشيقة. وفي الوقت نفسه، يبني الباحثون ZK-EVM مُتحقق رسميًا، وهو نسخة قابلة لإثبات Zero-Knowledge من الآلة الافتراضية لإيثريوم (EVM)، باستخدام أساليب مماثلة.

يمكن لنماذج اللغة الكبيرة بالفعل كتابة إثباتات Lean قابلة للاستخدام. وقد سمى بيترين Claude وDeepseek 4 Pro كأدوات قادرة، إلى جانب Leanstral، وهو نموذج أصغر تم ضبطه خصيصًا لـ Lean. أحد أمثلة المشاريع هو evm-asm، وهو تنفيذ لـ EVM مُحقق مقابل مرجع قابل للقراءة. هذه القدرة تعكس مهارات الاستدلال التي أظهرها المطورون في تحدي الذكاء الاصطناعي الأخير لبيترين challenge. وقد حَلَّ المختبرون هذا التحدي خلال ساعات.

لكن المخاطر تتجاوز الراحة. فقد رصد باحثو الأمن زيادة في محاولات الاستغلال المدعومة بالذكاء الاصطناعي exploit attempts هذا العام. إن الكود المُثبت صحته رسمياً يُعد وسيلة واحدة للدفاع ضد هذا الاتجاه. فلغة مواصفات أكثر سهولة ستسمح للمطورين بمراجعة الادعاءات دون الغوص في الأدلة المحيطة.

لكنيرين يواصل اختبار هذه الأفكار علنًا، حيث قام مؤخرًا بعرض لوحة إعلانية مجهولة مبنية باستخدام إثباتات الصفرية المعرفة. أظهر العرض كيف يمكن نقل المطالبات القابلة للتحقق من مخازن الأبحاث إلى منتجات قابلة للتطبيق. كما بدأ الباحثون أيضًا في التحقق رسميًا من عملاء التوافق باستخدام لغة Lean لاكتشاف الأخطاء مبكرًا.

ومع ذلك، فإن الاتجاه يعكس نمطًا مألوفًا: فصل الكود السريع عن الادعاءات القابلة للقراءة، ثم إثبات تطابق الاثنين.

لا يوجد أي نموذج أولي للغة الجديدة بعد، وترك بوتيرين البنية الدقيقة مفتوحة. قد يتفق المطورون على معيار مشترك واحد، أو يقبلوا بعدة لهجات غير متوافقة. يمكن أن يحدد هذا الاختيار مدى سرعة وصول الكود المُتحقق من قبل الذكاء الاصطناعي إلى أنظمة الإنتاج.