Axiom Math تتحقق رسميًا من Stacks Project للحد من فوضى الذكاء الاصطناعي

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

وكلاء يعملون بالتوازي

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

ويسد الإنجاز إحدى أكبر الفجوات في الرياضيات المصوغة رسميًا، وهي الهندسة الجبرية. ويقول سوامیناتان إن الباحثين الذين يريدون فحص أعمال جديدة باستخدام Lean باتت لديهم الآن قاعدة يبنون عليها.

لماذا يهم ذلك

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

وترى هونغ أن الوكلاء يحتاجون إلى مكتبة معرفية قابلة لإعادة الاستخدام كي لا ينتجوا محتوى رديئًا، وتتحدى شركات البرمجة أن تعمل على التوثيق الرسمي بهذا الحجم. تأسست Axiom في مارس 2025، وجمعت في مارس الماضي 200 مليون دولار في جولة Series A بقيادة Menlo Ventures.