نظام ذكاء اصطناعي بلا تدريب إضافي يثبت مسائل IMO 2026 الست جميعها في Lean

أظهر باحثون من Case Western Reserve University (أُنجز العمل خلال تدريب في Amazon Web Services) أن نموذجًا لغويًا كبيرًا جاهزًا، ودون أي تدريب إضافي، يستطيع إثبات نظريات معقدة وصحة برامج، إذا نُظّم العمل حوله تنظيمًا سليمًا. واستخدموا نموذج Anthropic Fable-5. تُكتب البراهين في نظام Lean، وهي لغة تفحص فيها «نواة» صغيرة كل خطوة استدلال، ولا يمكن خداعها.

وقد حلّ النظام جميع المسائل الست المصوَّغة شكليًا من الأولمبياد الدولي للرياضيات 2026. كما اجتاز جميع مسائل VERINA (مجموعة في البرمجة الموثَّقة)، وتعامل مع شروط التحقق من NTP4VC، وهي مجموعة صناعية للتحقق الشكلي من الشيفرة. وإضافة إلى ذلك، يحلّ مسائل من PutnamBench، وهي مجموعة مسائل مصوَّغة شكليًا من أولمبياد باتنام الجامعي.

وكل نتيجة محتسبة هي إما إثبات للعبارة وإما دحض لها، وقد فحصت نواة Lean الحالتين.

شجرة وكلاء بدلًا من سلسلة إعادات تشغيل

تكمن الصعوبة في أن Lean لا يجيب إلا عن سؤال محلي: هل تنجح هذه الخطوة المعينة أم لا. أما التقسيم السيئ للمسألة، أو غياب lemma (عبارة مساعدة)، فلا يتضحان إلا بعد عشرات الخطوات. يضاف إلى ذلك أن النموذج مقيَّد بنافذة السياق وبميزانية الحوسبة.

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

• لكل وكيل فرعي سياق نظيف خاص به ونسخته الخاصة من المشروع؛ • يستطيع الوكيل الفرعي أن يولّد بدوره وكلاء فرعيين، والأدوات متطابقة لدى الجميع؛ • قد ينفق الوكيل الفرعي عشرات الاستدعاءات على lemma واحدة، ثم لا يعيد إلى الأب إلا الـ lemma الجاهزة أو المثال المضاد أو النتائج الجزئية؛ • تصل النتائج إلى الأب في الدور التالي دون انتظار بقية الفروع، ولذلك قد يعيد اكتشاف مبكر توجيه البحث؛ • ينتهي البحث عندما يُقبل أول إثبات مناسب.

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

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

Lean كخدمة قابلة للتوسع

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

داخل كل نسخة مجموعة من العمليات العاملة التي حُمّلت فيها مكتبة Mathlib مسبقًا. يستغرق الاستيراد عشرات الثواني، لذلك تُعاد الاستفادة من العمليات، ويجري الفحص على عملية «دافئة» بسرعة أكبر بوضوح. تعمل النسخ على Kubernetes، ويتكيف عددها تلقائيًا مع الحمل.

ويحمي المؤلفون النظام من الغش بإجراء مستقل. فالوكيل الذي يحرّر ملف الإثبات قد يضعف صياغة النظرية، أو يترك الثغرة sorry، أو يضيف بديهية. لذلك جُمّد كل ما يسبق توقيع النظرية، ويجري الفحص النهائي عبر Lean Comparator: يجب أن يُترجم الملف دون ثغرات، وألا يستخدم سوى البديهيات المسموح بها. أما تقرير الوكيل نفسه عن نجاحه فلا يؤخذ في الحسبان.

امتحان جديد: الشيفرة الأولمبية في دور مسائل تحقق

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

• يكتب وكيل مبرمج حلولًا آمنة بلغة Rust لمسائل على غرار LeetCode، تتألف من دالة نقية واحدة على بيانات بسيطة (أعداد، قوائم، سلاسل نصية، أشجار، قوائم مترابطة)؛ • يجتاز الحل اختبارات مرجعية، ثم يُترجم إلى نموذج قابل للتنفيذ في Lean؛ • يُشغَّل Rust وLean على المدخلات نفسها، ولا تُقبل إلا البرامج التي تتطابق مخرجاتها تطابقًا كاملًا؛ • يكتب وكيل آخر المواصفة، أي الخاصية التي يجب أن تتحقق أو تُنتهك؛ • تُجمَّد الصياغة، ثم يثبتها المُثبِت أو يدحضها.

يختلف هذا عن المجموعات المكتوبة يدويًا في أن المسائل تحمل التزامات على مستوى التنفيذ: حساب بدقة ثابتة في عدد البتات، وأخطاء صريحة، وحلقات مولَّدة، وتحويلات أنواع، واستبدال وظيفي للحالة القابلة للتغيير. وتعطي حالات الدحض وسومًا سلبية لا توجد في خطوط الإنتاج التي تقتصر على البراهين. وتكتب المواصفة وكيلٌ آخر قبل أن يراها المُثبِت، ولا يستطيع المُثبِت اختيار صياغة أسهل.

وفي عيّنة من العبارات بحدّ زمني قدره 30 دقيقة لكل منها، لا يحلّ النظام سوى جزء منها. وبالنسبة إلى مُثبِت كاد يستنفد المعايير القديمة، تبقى هذه المسائل بعيدة عن التشبّع. ويمكن توسيعها بالحوسبة، واستخدامها لمقارنة مثبتات أخرى، ومكافآت في التعلم المعزَّز بمكافآت قابلة للتحقق (RLVR). فاختبار الشيفرة لا «يخمّن» شيئًا، بل يعطي حكمًا قابلًا للتحقق من نواة Lean. وتنتج طفرات البرامج (تعديلات صغيرة على شيفرة صحيحة) مسائل إضافية بوسوم سلبية، لكن المقالة لا تقيّمها.

ماذا يعني هذا للمهندسين

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