أكسيوم توثق مشروع ستاكس لمنع أخطاء الذكاء الاصطناعي
أعلنت إكسيوم ماتس، وهي شركة ناشئة تبلغ قيمتها ١٫٦ مليار دولار، أنها أتمت التحقق الشكلي من مشروع ستاكس، وهو مرجع رياضي ضخم بدأه عام ٢٠٠٥ عالم الرياضيات في جامعة كولومبيا يوهان دي يونغ بوصفه مشروعًا مفتوح المصدر، وشارك فيه باحثون على مدى سنوات لبناء نتائج تمتد من الجبر الأساسي إلى أفرع متقدمة في الجبر والهندسة ونظرية الأعداد. ونجحت الشركة، عبر وكلاء ذكاء اصطناعي، في ترجمة نحو ٧٦٥٤ صفحة إلى قرابة ١٦ مليون سطر من الشيفرة في لغة لين، حيث يفحص مساعد إثبات كل سطر للتأكد من سلامة البناء المنطقي. وتكتسب المبادرة أهميتها في ظل مخاوف من انتشار مخرجات رياضية توليدية غير موثوقة؛ فبعد أن أعلنت أوبن إيه آي الشهر الماضي عن ٧١٩ مخطوطة تدّعي تقديم حلول لمشكلات صعبة، أصبح احتمال وجود أخطاء في الفحوصات الآلية أمرًا مثيرًا للقلق. ويرى معنيون أن التحقق الشكلي يمكن أن يوفر أرضية أدق، إذ يعيد الرياضيون كتابة البراهين بلغة لين، ثم يتحقق برنامج مساعد من صحتها سطرًا بسطر، وهو نهج مستخدم في فحص تصميم الرقاقات والبرمجيات. ولم تكن المهمة سهلة لأن النتائج في مشروع ستاكس مترابطة، فكل نظرية تعتمد على ما سبقها، ما تطلب الحفاظ على كل الروابط عبر ملايين الأسطر. وقالت الشركة إن وكلائها عملوا بشكل متوازٍ وتلقائي ضمن هيكل عام، وإنها دربت نماذج خاصة لإكسابهم حسًا رياضيًا بشريًا مع مرور الوقت. ويُعد هذا الإنجاز فاصلًا، خصوصًا في الهندسة الجبرية، وهي من أكثر مجالات الرياضيات احتياجًا إلى قاعدة موثوقة من الإثباتات المؤكدة. وتسعى إكسيوم، التي أسستها في مارس ٢٠٢٥ كارينا هونغ بعد تركها برنامج الدكتوراه في جامعة ستانفورد، وجمعت جولة بقيمة ٢٠٠ مليون دولار من قيادة مينلو فنتشرز، إلى جعل الرياضيات المتحققة قاعدة يمكن أن يستند إليها البرمجون ووكلاء الذكاء الاصطناعي. وتقول إن كل نتيجة موثقة ستكون لبنة للبناء عليها في برهان جديد، بما يقلل احتمال إنتاج أعمال مشوبة بالأخطاء. ويرى علماء أن زيادة عدد البراهين المتحققة تتيح مزيدًا من البراهين المشابهة، وأن هذا الأساس الموثوق قد يكون ضروريًا كلما توسع استخدام الذكاء الاصطناعي في كتابة البرمجيات وأعمال العلم.
