أعلنت شركة الذكاء الاصطناعي الناشئة «أكسيوم ماث» (Axiom Math) نجاح منظومتها من الوكلاء المستقلين في التحقق رسمياً وبرمجياً (Formal Verification) من كامل محتوى «مشروع ستاكس» (Stacks Project)، الذي يُعد واحداً من أضخم المراجع الرياضية المفتوحة التي ألفها علماء الرياضيات عبر التاريخ.
تحويل المعرفة الرياضية إلى شفرة قابلة للتدقيق
يضم مشروع Stacks، الذي بدأه أستاذ الرياضيات في جامعة كولومبيا يوهان دي يونغ (Johan de Jong) عام 2005، نحو 7,654 صفحة تغطي مبادئ الجبر والهندسة الجبرية وصولاً إلى نظريات متقدمة في نظرية الأعداد. وقد تمكنت أسراب وكلاء Axiom Math من ترجمة هذه النصوص المعقدة والمترابطة إلى نحو 16 مليون سطر برمجي بلغة «لين» (Lean)، وهي لغة برمجة متخصصة تسمح لبرمجيات التدقيق بمراجعة كل برهان رياضي سطراً بسطر للتأكد من سلامته المنطقية الصارمة.
وتستهدف الشركة، التي تبلغ قيمتها السوقية 1.6 مليار دولار بعد جمعها 200 مليون دولار في جولة تمويل أولى بقيادة «مينلو فينتشرز» (Menlo Ventures)، بناء قاعدة معرفية موثوقة ومثبتة برمجياً لتعتمد عليها أنظمة الذكاء الاصطناعي مستقبلاً في تطوير البرمجيات والبحث العلمي وتفادي إخراج استنتاجات مضللة أو غير دقيقة تُعرف باسم «النفايات التوليدية» (AI slop).
آلية عمل الوكلاء البرمجية وتحديات الترابط الهيكلي
أوضحت كارينا هونغ (Carina Hong)، المؤسسة والرئيسة التنفيذية للشركة البالغة من العمر 25 عاماً والتي تركت برنامج الدكتوراه في الرياضيات بجامعة ستانفورد لتأسيس Axiom في مارس 2025، أن التحدي الأكبر تمثل في الحفاظ على ترابط آلاف النظريات وتفادي أي تناقض مفاهيمي. ومن جانبه، أشار آشفين سواميناثان (Ashvin Swaminathan)، عضو الفريق التقني في الشركة، إلى أن وكلاء الذكاء الاصطناعي لم يعملوا بتوجيه مباشر لكل خطوة، بل وُضعت لهم بنية هرمية مرنة سمحت لهم بتوزيع المهام بالتوازي، والاستفادة من نماذج مخصصة دُرّبت على التفكير الرياضي السليم بدلاً من الاعتماد على نماذج توليد الشفرة العامة.
ما الذي يعنيه هذا الإنجاز لقطاع التقنية؟
يمثل هذا التطور خطوة عملية لسد فجوة كبرى في إثبات الرياضيات حاسوبياً، خاصة في مجالات مثل الهندسة الجبرية. ولا تنحصر فائدة التحقق الشكلي في أوساط الأكاديميين؛ إذ يتيح توثيق البراهين عبر الشفرات الحاسوبية بيئة تأسيسية قابلة لإعادة الاستخدام. وتراهن الشركة على أن المطورين ومطوري البرمجيات الحساسة—كتصميم الرقائق وحسابات الأنظمة الحرجة—سيحتاجون إلى هذه القواعد المحققة لمنع الثغرات الأمنية والأخطاء الخفية الناتجة عن الاعتماد المتزايد على الوكلاء في كتابة البرمجيات.
كيف أعددنا هذا الخبر؟
اعتمد الخبر على المصدر الأصلي الموضح أعلاه. قد نستخدم أدوات آلية للمساعدة في الاستخراج والتصنيف والصياغة،
لكن النشر يخضع لقواعد تمنع المحتوى المكرر والقصير أو الروتيني منخفض القيمة.
اقرأ سياستنا التحريرية.