نئی تحقیق کے مطابق چین کے مصنوعی ذہانت کے نظام نے امریکی ریاضی دان کے ایک دہائی قبل پیش کردہ مسئلے کو حل کر لیا ہے۔
یہ الجبرا کا مفروضہ (Algebra Conjecture) پہلی بار 2014 میں یونیورسٹی آف آئیووا کے پروفیسر ڈین اینڈرسن نے پیش کیا تھا، جن کا 2022 میں انتقال ہو گیا۔
پیکنگ یونیورسٹی کی ٹیم کے تیار کردہ اس اے آئی سسٹم نے اینڈرسن کے مسئلے کو حل کرنے اور اپنے نتائج کی تصدیق کے لیے دہائیوں پر محیط ریاضیاتی لٹریچر کو بغیر کسی انسانی مداخلت کے پروسیس کیا۔
ٹیم نے arXiv ریپوزٹری پر پوسٹ کی گئی اور ابھی تک پیئر ریویو نہ ہونے والی تحقیق میں کہا ’اس فریم ورک کا استعمال کرتے ہوئے ہم نے کمیوٹیٹو الجبرا میں ایک اوپن پرابلم کو کامیابی کے ساتھ حل کیا اور بغیر کسی انسانی مداخلت کے اس کے ثبوت کو خودکار طریقے سے فارملائز کیا۔‘
سائنس دانوں نے مشاہدہ کیا کہ یہ اے آئی سسٹم ریاضی کے کام کسی بھی انسان سے زیادہ تیزی سے انجام دے سکتا ہے۔
بشمول وہ کام آزادانہ طور پر کرنا جن کے لیے عام طور پر مختلف شعبوں کے ماہرین کے درمیان تعاون کی ضرورت ہوتی ہے۔
پیکنگ یونیورسٹی کے ریاضی دان ڈونگ بن کی قیادت میں محققین نے کہا ’یہ کام ٹھوس مثال فراہم کرتا ہے کہ کس طرح اے آئی کا استعمال کرتے ہوئے ریاضی کی تحقیق کو کافی حد تک خودکار بنایا جا سکتا ہے۔‘
ریاضی کے مسائل حل کرنے کے لیے دنیا بھر میں اے آئی سسٹمز کو تربیت دی جا رہی ہے لیکن انہیں ریاضی کے مسائل کو حل کرنے کے لیے اب بھی بڑی مقدار میں انسانی نگرانی کی ضرورت ہوتی ہے۔
چینی سائنس دانوں نے اپنی حالیہ تحقیق میں لکھا ’ریاضی کے ثبوت مکمل درستی کے متقاضی ہوتے ہیں، تاہم ماہرین کے لکھے ہوئے ثبوتوں میں بھی معمولی نقائص ہو سکتے ہیں۔
’بڑے لینگوئج ماڈلز (LLMs) کے ذریعے تیار کردہ ثبوت، جن میں غلط فہمی (hallucination) کا امکان زیادہ ہوتا ہے، بہت کم قابل اعتماد ہوتے ہیں۔‘
’اس سے متاثر ہو کر ہم تحقیق کی سطح کے ریاضی کو خود مختار طریقے سے حل کرنے اور تصدیق کرنے کے لیے ایک فریم ورک تجویز کرتے ہیں جو ایک قدرتی زبان کے استدلال کرنے والے ایجنٹ کو ایک فارملائزیشن ایجنٹ کے ساتھ مربوط کرتا ہے۔‘
مزید پڑھ
اس سیکشن میں متعلقہ حوالہ پوائنٹس شامل ہیں (Related Nodes field)
نیا اے آئی ’ریتھلاس‘ (Rethlas) نامی ایک استدلالی نظام کا اطلاق کرتا ہے، جو ریاضی کے تھیورم سرچ انجن، یا ’میٹلاس‘ (Matlas) سے استفادہ کرتے ہوئے مسئلے کو حل کرنے کی حکمت عملی تلاش کرتا ہے، جس کا طریقہ کار بالکل ویسا ہی ہے جیسا کہ ریاضی دان استعمال کرتے ہیں۔
جب ریتھلاس ایک ممکنہ ثبوت لے کر آتا ہے تو ’آرکن‘ (Archon) نامی دوسرا نظام ’لین سرچ‘ (LeanSearch) نامی ایک اور سرچ انجن کا استعمال کرتے ہوئے اس ثبوت کو ایک انٹرایکٹو تھیورم پروور کے پروجیکٹ میں تبدیل کر دیتا ہے۔
یہ تھیورم پروور ’لین 4‘ ایک پروگرامنگ لینگویج بھی ہے جس میں کمیونٹی کی دیکھ بھال میں ایک لائبریری موجود ہے جس میں لاکھوں تھیورمز اور تعریفیں موجود ہیں۔
محققین نے اینڈرسن کے الجبرا کے مفروضے کو حل کرنے کے لیے اس نئے اے آئی سسٹم کا استعمال کیا، جس میں 80 گھنٹے کا رن ٹائم لگا۔
انہوں نے لکھا ’انسانی آپریٹر کی طرف سے ریاضیاتی فیصلے کی کوئی ضرورت نہیں تھی۔‘
تاہم، محققین نے پایا کہ اگر کوئی ریاضی دان آرکن کی رہنمائی کرے تو وہ اس عمل کو تیز کر سکتے ہیں۔
انہوں نے نوٹ کیا ’ہمارا کام ریاضیاتی تحقیق کے لیے ایک امید افزا نمونہ پیش کرتا ہے جس میں غیر رسمی اور رسمی استدلالی نظام، تھیورم تلاش کرنے والے ٹولز سے لیس ہو کر، قابل تصدیق نتائج پیدا کرنے اور انسانی کوششوں کو کافی حد تک کم کرنے کے لیے مل کر کام کرتے ہیں۔‘
© The Independent
