الذكاء الاصطناعي يُعزز الاكتشافات الرياضية: منحة جديدة لباحثين من معهد ماساتشوستس للتكنولوجيا
مقدمة
حصل باحثون من قسم الرياضيات في معهد ماساتشوستس للتكنولوجيا (MIT) على منحة بحثية مميزة ضمن مبادرة “الذكاء الاصطناعي من أجل الرياضيات” التي أطلقتها مؤسستا “Renaissance Philanthropy” و “XTX Markets”. وقد شملت هذه المنح الرائدة 29 مشروعًا بحثيًا، وتهدف إلى تطوير أنظمة ذكاء اصطناعي تُساعد على تعزيز الاكتشافات والبحوث الرياضية.
مشروع الباحثين ديفيد رو وأندرو سثرلاند
حصل الباحثان ديفيد رو (MIT ’06) وأندرو سثرلاند (MIT ’90، PhD ’07) مع الباحث كريس بيركبيك من جامعة إيست أنجليا، على منحة لدعم إثبات النظريات تلقائيًا من خلال ربط قاعدة بيانات الدوال L والأشكال النمطية (LMFDB) بمكتبة Lean4 الرياضية (mathlib).
يُعاني تطوير برامج إثبات النظريات التلقائية من نقص الموارد، إلا أن تقنيات الذكاء الاصطناعي، مثل نماذج اللغات الكبيرة (LLMs)، تُسهم في تقليل هذه العقبة، مما يجعل أطر التحقق الرسمي متاحة للباحثين الرياضيين.
تُعتبر مكتبة Mathlib مكتبة رياضية ضخمة تعتمد على جهود جماعية، وهي مصممة لمنظومة Lean لإثبات النظريات، التي تتحقق من صحة كل خطوة في الإثبات. تحتوي Mathlib على ما يقارب 105 نتيجة رياضية (مثل اللمّات، والفرضيات، والنظريات). أما قاعدة بيانات LMFDB، فهي مورد تعاوني ضخم على الإنترنت تُشبه “موسوعة” لنظرية الأعداد الحديثة، وتحتوي على أكثر من 109 بيان ملموس. يُشرف الباحثان سثرلاند ورو على تحرير LMFDB.
يهدف مشروع الباحثين إلى تعزيز كلا النظامين، بجعل نتائج LMFDB متاحة ضمن Mathlib كبيانات لم تُثبت رسميًا بعد، وتوفير تعريفات رسمية دقيقة للبيانات العددية المخزنة في LMFDB. سيفيد هذا الربط كلًا من الباحثين الرياضيين ووكلاء الذكاء الاصطناعي، وسيوفر إطارًا لربط قواعد بيانات رياضية أخرى بأنظمة إثبات النظريات الرسمية.
التحديات والفرص
تتمثل العقبات الرئيسية أمام أتمتة الاكتشاف الرياضي والإثبات في:
- محدودية المعرفة الرياضية المُدوّنة رسميًا.
- التكلفة العالية لتدوين النتائج المعقدة رسميًا.
- الفجوة بين ما هو مُتاح حاسوبيًا وما هو عملي تدوينه رسميًا.
يستخدم الباحثون التمويل لبناء أدوات للوصول إلى LMFDB من Mathlib، مما يجعل قاعدة بيانات ضخمة من المعارف الرياضية غير المُدوّنة رسميًا متاحة لنظام إثبات رسمي. يُمكن هذا النهج مساعدي الإثبات من تحديد أهداف محددة للتدوين الرسمي دون الحاجة إلى تدوين كامل بيانات LMFDB مسبقًا.
يُلاحظ الباحثون أن إثبات نظريات جديدة على حدود المعرفة الرياضية غالبًا ما يتضمن خطوات تعتمد على حسابات غير تافهة. فعلى سبيل المثال، يعتمد إثبات أندرو وايلز لنظرية فيرما الأخيرة على ما يُعرف بـ “خدعة 3-5” في نقطة حاسمة من الإثبات.
الاستفادة من الحسابات السابقة وقواعد البيانات
يُتيح استخدام النتائج المخزنة الاستفادة من آلاف سنوات المعالجة المركزية التي تم إنفاقها بالفعل في إنشاء LMFDB، مما يُوفر المال الذي كان سيلزم لإعادة هذه الحسابات. كما أن توفر المعلومات المحسوبة مسبقًا يجعل من الممكن البحث عن أمثلة أو أمثلة مضادة دون معرفة مدى اتساع البحث مسبقًا. بالإضافة إلى ذلك، فإن قواعد البيانات الرياضية عبارة عن مستودعات مُنسّقة، وليست مجرد مجموعة عشوائية من الحقائق.
الخطوات القادمة
يتمثل الهدف التالي للباحثين في بناء فريق، والتواصل مع مجتمعي LMFDB و Mathlib، والبدء في تدوين التعريفات التي تُشكل أساس أقسام المنحنيات الإهليلجية، وحقول الأعداد، والأشكال النمطية من LMFDB، وجعل من الممكن تشغيل عمليات بحث LMFDB من داخل Mathlib.
خاتمة
يمثل هذا المشروع خطوة هامة نحو تعزيز الاكتشافات الرياضية من خلال الاستفادة من تقنيات الذكاء الاصطناعي، ويمثل نموذجًا يحتذى به في التعاون بين الباحثين وتكامل مختلف الموارد الحاسوبية والرياضية.
اترك تعليقاً