شركة Axiom Math تتحقق من 16 مليون سطر من شيفرة Lean بواسطة الوكلاء وتسد ثغرة في الرياضيات الصورية

حين «يحل» الذكاء الاصطناعي مسألة رياضية جديدة كل أسبوع، يبرز سؤال وجيه: من يتحقق من كل ذلك؟ في الشهر الماضي وحده نشرت OpenAI نحو 719 مخطوطة تدّعي حل مسائل معقدة. ومن المستحيل قراءتها كلها يدويًا، كما أن الأخطاء تفلت حتى من الفحوص الآلية. تقترح الشركة الناشئة Axiom Math، المقدّرة قيمتها بـ1.6 مليار دولار، طريقًا مختلفًا: ليس التباطؤ، بل الاستناد إلى أساس موثّق.

ما الذي أُنجز بالضبط

أعلنت الشركة يوم الأربعاء أنها تحققت صوريًا من مشروع Stacks Project، أحد أكبر المجموعات في تاريخ الرياضيات البشرية. بدأه عام 2005 يوهان دي يونغ من جامعة كولومبيا كمرجع مفتوح. ويضم اليوم نحو 7654 صفحة: من الجبر الجامعي إلى أحدث أفكار الهندسة الجبرية ونظرية الأعداد.

أعاد وكلاء Axiom كتابة ذلك كله في صورة نحو 16 مليون سطر من الشيفرة بلغة Lean. ثم فحص برنامج يُسمّى proof assistant الشيفرة سطرًا بسطر. وإذا نجح الفحص، فالبرهان سليم منطقيًا، ولا حاجة إلى تصديق المؤلف بمجرد كلامه.

لماذا الأمر أصعب مما يبدو

التحقق من كل مبرهنة على حدة لا يمثل سوى نصف العمل. فنتائج Stacks مترابطة كشجرة العائلة: كل نتيجة تستند إلى سابقاتها. وإذا «انزاح» تعريف في مكان ما، ينهار كل ما فوقه. لذلك كان على الفريق الحفاظ على جميع الروابط عبر 16 مليون سطر. وتعترف الرئيسة التنفيذية كارينا هونغ نفسها بأنها لم تكن واثقة من النجاح في البداية: فالكبير والهش لا يجتمعان بسهولة.

كانت البنية كالتالي: في الأعلى تسلسل هرمي مرن، ولكن دون توزيع صارم للمهام. كان الوكلاء يجدون بأنفسهم ما يعملون عليه ويعملون بالتوازي. كما درّبت Axiom نماذجها الخاصة للرياضيات، وهو ما لا يفعله، بحسب هونغ، معظم المنافسين في مجال التحقق. في البداية كان خبير Lean في الشركة يغرس في الوكلاء «الذوق»، أي فهم الشكل الذي ينبغي أن تبدو عليه الشيفرة الجيدة. ومع الوقت، تقول هونغ، صاروا يتدبرون أمرهم بأنفسهم.

لماذا يهم هذا المطورين

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

رهان Axiom: الرياضيات ميدان تدريب تُصقل فيه هذه المهارة ثم تُنقل إلى البرمجيات. يمكن للوكلاء قراءة مكتبة Lean جاهزة والبناء عليها دون البدء من الصفر. ويصوغ تيرينس تاو المبدأ العام هكذا: كلما زادت البراهين الصورية، زاد ما يمكن إنجازه من جديد.

القيود

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

ماذا تفعل عمليًا

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