AlphaProof Code مقابل MathForm-8B: مرحلتان من مسار Lean نفسه، لا متنافسان

إذا قرأت ورقة AlphaProof Code عن كثب، فسيلفت انتباهك رقم لا يبرزه الإعلان: فمن بين الأسابيع الأربعة التي قضاها باحثو DeepMind الخمسة في التحقق من Signal، كان الجزء الذي تعذّرت أتمتته هو الواجهة الأمامية. فقد جلس خبراء بشريون مع مزيج من النماذج لترجمة أهداف Signal الأمنية إلى مواصفات Lean صورية، وراجع خبير كل واحدة منها قبل البدء بأي عمل على البرهان. وهذا هو عنق الزجاجة. أما MathForm-8B، نموذج الأتمتة الصورية ذو الثمانية مليارات معامل من OpenBMB الذي أُطلق على Hugging Face في 14 أغسطس 2026، فهو محاولة مباشرة لأتمتة هذه الخطوة تحديدًا — أي أخذ عبارة رياضية باللغة الطبيعية وإخراج عبارة مبرهنة بصيغة Lean 4 جاهزة كي يبرهنها شخص آخر. ضعهما جنبًا إلى جنب، فلن تكون بصدد مقارنة منتجين. أنت تنظر إلى مرحلتين متتاليتين من خط أنابيب واحد، يفصل بينهما الفارق بين الرياضيات وأمن البروتوكولات.

مسار العمل، بالترتيب الذي يجري به العمل

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

MathForm-8B يؤدي المهمة الأولى، لفئة ضيقة من المدخلات: ادعاءات رياضية بأسلوب الكتب المدرسية. أعطِه "لكل عدد حقيقي x، فإن x² غير سالب" فيعيد الاستيرادات والأنواع وترويسة مبرهنة في Lean 4. لكنه لا يعيد برهانًا، ومؤلفوه صريحون في أن البحث عن البرهان مشكلة شخص آخر. أرقامه المعلنة، وكلها مبلَّغ عنها من المورّد وغير مُعاد إنتاجها، هي 88.06% في المتوسط لـ Pass@8 تحت فحص نحوي، و72.37% تحت فحص الاتساق الأكثر صرامة عبر ستة معايير تقييم — والفجوة بين هذين الرقمين هي المقياس الصادق لمدى تكرار أن تعني عبارة صحيحة نحويًا شيئًا مختلفًا عما طُلب.

يؤدي AlphaProof Code المهمتين الثانية والثالثة، إضافة إلى مرحلة مواصفات لم يكن بمقدور MathForm-8B الاقتراب منها. أهداف أمان Signal ليست ادعاءات رياضية بالمعنى الذي دُرّب عليه MathForm؛ بل هي عبارات عن بروتوكول — بأن تظل الرسائل محمية قبل تعرّض جهاز للاختراق مؤقتًا وبعده، وبأن المُبادر والمُستجيب هما بالفعل ما يدّعيان أنهما هما. تطلّب تحويلها إلى Lean خبرة بروتوكولات لا تملكها أي أداة أتمتة صياغة رسمية بحجم 8B. بمجرد أن أصبحت المواصفات موجودة، أُسندت أعمال البرهان بالكامل إلى وكلاء، وأُسند التحقق إلى نواة Lean وإلى وكيل حارس يستخدم المقارن مقابل نسخة مواصفات محتجزة.

كم يكلفك استخدام كل واحد منها فعليًا

• الأوزان — MathForm-8B: قابلة للتنزيل، Apache 2.0، أربع شرائح safetensors بصيغة BF16، تم ضبطها ضبطًا دقيقًا من Qwen3-8B. AlphaProof Code: لا يوجد. يتضمن الإصدار تطويرًا بـ Lean، ودلالات AArch64، وربطًا لـ libsignal على github.com/google-deepmind/code-verification.

• تشغيله — MathForm-8B: ‏Transformers أو vLLM أو SGLang، وكلها توفّر نقطة نهاية متوافقة مع OpenAI، على عتاد تملكه. AlphaProof Code: لا نقطة نهاية، ولا واجهة برمجة تطبيقات، ولا قائمة انتظار، ولا سعر؛ فهو إطار بحثي تقول DeepMind إنه يحتاج إلى «بحث مستمر» قبل أن يتوسّع.

• المدخل — MathForm-8B: عبارة رياضية باللغة الطبيعية. AlphaProof Code: مواصفة صورية بالإضافة إلى الملف الثنائي الذي تريد إثباته مقابلها.

• المخرجات — MathForm-8B: عبارة مبرهنة Lean 4، غير مُثبتة. AlphaProof Code: برهان تم التحقق منه آليًا، أو دحض عندما يكون الكود معطوبًا.

• مراجعة بشرية — MathForm-8B: أنت تراجع البيان الصادر، وبنسبة اتساق تبلغ 72.37% ستكون بصدد مراجعة الكثير منها. AlphaProof Code: يراجع الخبراء كل مواصفة قبل بدء عمل الإثبات، ثم تضع الوكلاء علامة على نحو 1% من قاعدة الشيفرة لإلقاء نظرة ثانية.

• حدود معروفة — MathForm-8B: العبارات الرياضية فقط، دون توليد براهين، وكان مستودع الشيفرة المُشار إليه في ملف README الخاص به لا يزال مجرّد عنصر نائب عند الإصدار. AlphaProof Code: لا ضمان ما بعد كمّي لـ SPQR healing، ولا خصوصية للحمولة، وجلسة واحدة لكل ترقية، وحدّ لتزوير MAC يصبح بلا معنى عند نحو 25,000 رسالة في الجلسة الواحدة.

الفجوة التي سيتعين على MathForm-8B سدّها

من المُغري القول إن أداة إضفاء الصيغة الرسمية الآلية كان يمكن أن تكتب مواصفات Signal وتوفّر على الباحثين أسابيع العمل المكثّف في البداية. لكن رواية الورقة نفسها تقول غير ذلك، والسبب محدد. فمواصفة بروتوكول ليست إعادة صياغة لادعاء؛ بل هي خيار بشأن نموذج الخصم. يتضمن عمل Signal مسارًا رمزيًا في إطار Dolev–Yao مع مهاجم كمّي يكسر Diffie–Hellman بعد المصافحة، ومسارًا حسابيًا مع خصوم كلاسيكيين وحدّ ملموس. يعبّر هذان المساران عن مبرهنات مختلفة حول الشيفرة نفسها، والاختيار بينهما قرار هندسي له تبعات أمنية. لن يقوم أي نموذج دُرّب على تحويل "أثبت أن x² ≥ 0" إلى Lean باتخاذ ذلك القرار.

ما يمكن أن يفعله مُصَرِّع آلي على نحو معقول هو الجزء الميكانيكي من ذلك العمل: فبإعطائه هدفًا أمنيًا مكتوبًا بالنثر ومكتبة من تعريفات Lean القائمة، يُنتج مسودة أولى للعبارة بأسلوب المشروع نفسه، ليقوم خبير بتصحيحها. هذا توفير حقيقي، لكنه أصغر بكثير مما يوحي به العنوان. تذكر الورقة كتالوجًا لانحرافات المواصفات يضم أكثر من 200 مدخل حسابي ونحو 35 مدخلًا رمزيًا — خمسة عشر منها فجوات أو أخطاء في تحليل Double Ratchet — وهو ما وجدته خطوة المراجعة البشرية. وأي نموذج يصوغ العبارات كمسودات سيتعين قياسه مقابل ذلك الكتالوج، لا مقابل نتيجة Pass@8 في معايير تقييم الرياضيات.

حيث لا يمكن مقارنة الرقمين على الإطلاق

تُقيس نسبة 88.06% لدى MathForm-8B و6.5 مليون سطر لدى AlphaProof Code أمرين مختلفين، ولا ينبغي أبدًا وضعهما في العمود نفسه. إحداهما معدل إصابة في مجموعة معايير بناها المؤلفون؛ والأخرى كمية من البرهان أُنتجت لهدف واحد. والمورّد صريح في أن نسبة 88.06% تستخدم فحصًا نحويًا، وهو معيار ضعيف — إذ يمكن لعبارة أن تُصرَّف وتظل مع ذلك تُصوغ الادعاء الخاطئ، ولهذا يكون رقم الاتساق أقل بـ16 نقطة.

المثال المماثل في AlphaProof Code هو عمل التحقق: أُعيد إدخال خللين سبق إصلاحهما في Signal، خلل الحالة الضعيفة وخلل الزمرة الفرعية الصغيرة، إلى نسخة معزولة، وفي كلتا الحالتين أنتج النظام برهانًا مُدقَّقًا آليًا على أن النسخة المعطوبة تفشل في نظرية الأمان. ذلك اختبار سلبي، والاختبار السلبي هو ما يفتقده معيار تقييم المُصيغ التلقائي تمامًا. لا يورد MathForm-8B أي نتيجة من قبيل «عند إعطاء عبارة خاطئة عمدًا، قال النموذج إنها كذلك».

كيف ستستخدمها معًا فعليًا

وعلى نحو ملموس، وهذا هو الجزء الوحيد من المقارنة الذي له مسار قريب المدى: استخدم مُصيغًا آليًا لإعداد المسودة، ونموذجًا عامًا قويًا لنقد المسودة، ووكيل إثبات لمحاولة إنجاز الإثبات. لكل مرحلة نمط فشل مختلف، وتوجيه الثلاث جميعًا عبر مفتاح واحد هو التسهيل العملي. على OrcaRouter، أكثر من 200 نموذج تقع خلف واجهة API واحدة بسعر قائمة المزوّد وبهامش ربح 0%، لذا فإن حلقة صياغة مواصفات ترسل العبارة نفسها إلى نموذجين وتحسب فروق Lean بينهما هي استدعاء routing-DSL بدلًا من ثلاثة عقود وثلاث مجموعات SDK. يغطي التجاوز التلقائي عند الفشل الحالة التي يمرّ فيها النموذج الذي اخترته بفترة سيئة.

ما لا يوفره أيٌّ من ذلك هو الضمان. يمنحك MathForm-8B بيانًا، وتمنحك النماذج نقدًا، ولا يزال هناك شيء عليه أن يثبته. في الوقت الحاضر، النظام المنشور الوحيد الذي يغلق تلك الحلقة على شيفرة حقيقية قيد التشغيل هو AlphaProof Code، وهو ليس للبيع.

السبب في قراءة كلتا الورقتين بدلًا من اختيار فائز

MathForm-8B أداة مفيدة ذات مهمة ضيقة وسقف دقة حقيقي ومقاس. أما AlphaProof Code فهو عرض توضيحي لسير العمل، والنتيجة الأكثر قابلية للنقل منه ليست حجم البرهان، بل التقسيم: فعمل المواصفات يحتاج إلى بشر ونموذج عام قوي، وعمل البرهان يحتاج إلى فرق من الوكلاء ونواة، والحد الفاصل بينهما هو حيث تكمن كل الصعوبة. وينبغي لأي شخص يبني خط أنابيب تحقق أن يأخذ هذا التقسيم على محمل الجد، وأن ينظر إلى الأتمتة الصورية باعتبارها الجزء الذي يقلل تكلفة المرحلة الأولى — لا الجزء الذي يحل محلها.

الخلاصة الصادقة لفريق يقرر ما ينبغي تنزيله هذا الشهر: MathForm-8B، نعم، إذا كنت تعمل مع Lean وتريد مساعدة في الصياغة. AlphaProof Code، اقرأ مستودع المصنوعات وكتالوج الانحرافات عن المواصفات، لأن الكتالوج يخبرك بما لا يزال التحقق الشكلي من كود الإنتاج عاجزًا عن الوصول إليه أكثر مما سيفعل أي إعلان.