Bend: لغة تمنع أخطاء الذكاء الاصطناعي بالبرهان

يقدَّم Bend في سطر واحد: لغة سريعة تمنع أخطاء الذكاء الاصطناعي بالبرهان، وتجمع سرعة C وتوازي CUDA وبراهين Lean وصياغة Python. ومنطق المشروع أن الناس في اقتصاد ما بعد الذكاء العام سيقلعون في النهاية عن كتابة الكود وقراءته، لكنهم سيحتاجون رغم ذلك طريقًا لا لبس فيه لإبلاغ الآلات بما يجب بناؤه. فالقوانين، كما يقول الموقع، تعبّر عن القصد بدقة أكبر من اللغة الطبيعية، والبراهين تتحقق من أن النموذج نفّذ القصد تنفيذًا صحيحًا، والمترجم السريع يشغّل النتيجة بسرعة.

سريعة في التنفيذ والفحص

يُصرَّف Bend إلى كود أصلي. وعلى نواة واحدة تقترب الأداءات من C، بينما يتوزع الملف التنفيذي نفسه على ست عشرة نواة أو على وحدة رسوميات ليعمل أسرع بما يصل إلى مئة ضعف من نواة واحدة. وللسرعة معنى في جهة الفحص أيضًا: فمدقّق الأنواع في Bend مدقّق براهين على طريقة Lean وRocq، حيث قد يستغرق فحص قاعدة كود متوسطة دقائق. أما Bend فيستغرق ثانية واحدة على الأكثر، وهذا ما يتيح للوكيل التحقق من عمله بعد كل تغيير.

توازٍ بلا خيوط ولا نوى

لا خيوط هنا ولا أقفال ولا نوى رسوميات تُكتب يدويًا. يقسم المبرمج العمل نصفين، فتوزع اللغة النداءات على كل نواة تجدها ثم تجمع النتائج. وفي العرض تُشغَّل عملية حساب قوة الاثنين على 4,096 نواة رسوميات.

القوانين بوصفها AGENTS.md مدعومًا بالبرهان

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

كيف تبدأ

التثبيت أمر shell واحد، وبعد ذلك تتوجه التعليمات إلى وكلاء البرمجة: يُضاف إلى AGENTS.md مقطع قصير يطلب تشغيل bend guide، وحفظ القواعد المهمة في LAWS.bend، وتشغيل bend PROOF.bend قبل كل commit، وتوزيع الكود كلما أمكن. ويوصي الموقع بطلب قوانين لكل ما يجب ألا ينكسر أبدًا، والبدء من الواجهة الخلفية على Linux أو macOS. وBend لغة شابة، كما يُحذَّر، لذا يُتوقع ظهور أخطاء وتُبلَّغ؛ والتفاصيل في دليل اللغة على GitHub وفي ورقتين، إحداهما عن نظرية الأنماط التابعة الأفينية التي تشكّل نواة Bend، والأخرى عن بيئة تشغيل متوازية للمعالجات وأجهزة الرسوميات.