لغة Bend تتحقق من شفرة الذكاء الاصطناعي بالإثبات الرياضي

Bend لغة برمجة جديدة تقوم على فكرة مختلفة: الشفرة التي يكتبها وكيل ذكاء اصطناعي (AI agent) لا تُقرأ بل يُطلب لها إثبات. مدقق الأنواع في اللغة هو نفسه مدقق إثباتات، على نحو ما نجده في Lean وRocq. الفارق الذي يبرزه الفريق هو السرعة: تلك الأدوات قد تستغرق دقائق على قاعدة شفرة متوسطة الحجم، بينما لا تستغرق Bend أكثر من ثانية واحدة، ما يسمح للوكيل بالتحقق بعد كل تعديل.

قوانين لا يمكن كسرها

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

نواة واحدة أو ست عشرة أو وحدة رسوميات

تُترجم Bend إلى شفرة أصلية. وعلى نواة واحدة تعمل بسرعة تقارب سرعة C، ويعمل الملف التنفيذي نفسه على ست عشرة نواة أو على وحدة معالجة الرسوميات (GPU) بسرعة تصل إلى مئة ضعف سرعة النواة الواحدة. لا حاجة لكتابة خيوط تنفيذ أو أقفال أو نوى: تقسم العمل إلى نصفين، فتوزع اللغة النداءات على كل نواة تجدها ثم تجمع النتائج. ويظهر أحد الأمثلة تشغيل الدالة pow2 على 4096 نواة رسوميات.

اللغة موثقة بالكامل في ملف GUIDE.md الذي يطبعه الأمر bend guide. وهناك ورقتان تشرحان البنية الداخلية: BendTT لنظرية الأنواع التابعة التقريبية، وBendRT لزمن التشغيل المتوازي. المشروع لا يزال حديثاً ويعمل على أفضل نحو في الواجهة الخلفية على Linux وmacOS، والفريق يطلب الإبلاغ عن الأخطاء. التفاصيل على موقع المشروع.