ما مدى قرب أجهزة الكمبيوتر من البناء التلقائي للتفكير الرياضي؟

تحدد مجموعة أدوات الذكاء الاصطناعي شكل الجيل التالي من أدوات إثبات النظرية التلقائية ، ومعها العلاقة بين الرياضيات والآلات.

يقال أنه في عام 1970 ، قدم عالم الرياضيات المتوفى بول كوهين ، الفائز الوحيد بميدالية فيلدز عن عمله في المنطق الرياضي ، تنبؤًا لا أساس له من الصحة والذي لا يزال يسعد علماء الرياضيات أو يزعجهم: "في يوم من الأيام سيحل محل علماء الرياضيات في المستقبل. أجهزة الكمبيوتر ". تنبأ كوهين ، المعروف بأساليبه الجريئة في العمل بنظرية المجموعات ، بإمكانية أتمتة جميع الرياضيات ، بما في ذلك البراهين الكتابية.



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



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



محرمات النظرية المحوسبة تنقسم إلى فئتين. تستخدم محررات النظرية الآلية (ATPs) عادةً أساليب القوة الغاشمة لطحن أكوام ضخمة من الأرقام. تعمل مُثبتات النظرية التفاعلية (ITP) كمساعدين بشريين ، وقادرة على التحقق من دقة الحجج ، وكذلك البحث عن الأخطاء في البراهين الموجودة. ومع ذلك ، حتى إذا قمت بدمج هاتين الاستراتيجيتين (كما هو الحال مع المحفزات الأكثر حداثة) ، فلن يظهر نظام التفكير التلقائي منها.





ساعد العالم المعرفي سيمون ديديو من جامعة كارنيجي ميلون في إثبات أن البشر والآلات يصنعون برهانًا رياضيًا بطريقة مماثلة.



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



واحدة من المشاكل الصعبة المفتوحة في هذا المجال هي مسألة مقدار عملية إنشاء الإثبات التي يمكن أتمتها. هل سيكون النظام قادرًا على إنشاء فرضية مثيرة للاهتمام وإثباتها بطريقة مفهومة للناس؟ تقدم مجموعة من الإنجازات الأخيرة التي حققتها المختبرات حول العالم طرقًا للذكاء الاصطناعي (AI) للإجابة على هذا السؤال. يستكشف جوزيف أوربان من المعهد التشيكي للمعلوماتية والروبوتات وعلم التحكم الآلي في براغ ، الأساليب المختلفة التي تستخدم التعلم الآلي لزيادة فاعلية المحفزات الحالية. في يوليو ، مجموعتهعرض مجموعة من الفرضيات والأدلة الأصلية التي تم إنشاؤها والتحقق من صحتها بواسطة الآلات. في يونيو ، نشرت مجموعة في Google Research بقيادة Christian Szegedi نتائج محاولات استخدام نقاط القوة في أنظمة معالجة اللغة الطبيعية لجعل أدلة الكمبيوتر أكثر تشابهًا في التركيب والتفسير للأدلة البشرية.



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

آلات مفيدة

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



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





تستخدم إميلي رييل من جامعة جونز هوبكنز إثباتات النظرية لتدريب الطلاب ومساعدي الكمبيوتر.



قال شليبالا: "يمكنك أن تأخذ أي عبارة رياضية وترميزها بأداة واحدة ، ثم تجمع كل الحجج ، وتحصل على دليل على السلامة".



في الرياضيات ، ساعدت أدوات إثبات النظرية في إنتاج براهين معقدة وثقيلة حسابيًا كان يمكن لولا ذلك أن تستغرق آلاف السنين الرياضية البشرية. ومن الأمثلة الصارخة فرضية كبلرحول التعبئة الأكثر كثافة للكرات في الفضاء ثلاثي الأبعاد (تاريخياً ، كانت هذه الكرات برتقالية أو قذائف مدفعية). في عام 1998، توماس هيلز وتلميذه، وسام فيرغسون، أكمل هذا دليل على استخدام مجموعة متنوعة من التقنيات الرياضية المحوسبة. كانت النتيجة مرهقة للغاية - استغرق الدليل 3 جيجا بايت - حتى أن 12 عالم رياضيات حللها لعدة سنوات قبل الإعلان عن أنهم متأكدون بنسبة 99٪ من حقيقتها.



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

مشاعر مختلطة

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





يتساءل العديد من علماء الرياضيات ، جنبًا إلى جنب مع مايكل هاريس من جامعة كولومبيا ، عن الحاجة إلى إنشاء أدوات إثبات نظرية محوسبة - وأن هذا الأخير سيجعل علماء الرياضيات غير ضروريين.



هناك استياء آخر لعلماء الرياضيات مرتبط بحقيقة أنهم إذا أرادوا استخدام مبرهنات النظرية ، فعليهم أولاً تعلم كيفية البرمجة ، ثم معرفة كيفية التعبير عن مشكلتهم بلغة يمكن فهمها بواسطة الكمبيوتر - وكل هذا يصرف الانتباه عن ممارسة الرياضيات. قال هاريس: "بحلول الوقت الذي أعيد فيه صياغة السؤال بطريقة مناسبة لهذه التكنولوجيا ، سأحل هذه المشكلة بنفسي".



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



لكن Buzzard وآخرين يعتقدون أنهم ربما لا يزالون بحاجة إلى إلقاء نظرة فاحصة على التكنولوجيا. على سبيل المثال ، قال ديديو: "قد لا تكون أدلة الكمبيوتر غريبة كما نعتقد". مؤخرًا ، جنبًا إلى جنب مع سكوت فيتيري ، عالم الكمبيوتر في جامعة ستانفورد ، قام بعكس هندسة العديد من البراهين الكنسية الشهيرة (بما في ذلك بعض البدايات)Euclidean) وعشرات البراهين التي تم إنشاؤها بواسطة برنامج الكمبيوتر لإثبات نظريات Coq التي تبحث عن أوجه التشابه. ووجدوا أن الهيكل المتفرّع لبراهين الآلة كان مشابهًا بشكل ملحوظ لبنية البراهين التي صنعها البشر. وقال إن هذه الخاصية المشتركة يمكن أن تساعد الباحثين في إيجاد طريقة جعل البرامج المساعدة تشرح.



قال ديديو: "قد لا تكون البراهين الآلية غامضة كما تبدو".



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



يقول رييل أيضًا إنه يستخدم المبررات النظرية أكثر فأكثر في عمله مؤخرًا. قالت: "ليس من الضروري استخدامها طوال الوقت ، ولن تحل محل الخربشات على قطعة من الورق أبدًا ، ولكن استخدام مساعدي الكمبيوتر للحصول على أدلة قد غيّر فهمي لكيفية كتابة الأدلة".



تقدم Theorem Provers أيضًا طريقة للحفاظ على الرياضيات عادلة. في عام 1999 عالم رياضيات سوفييتي وروسي وأمريكيفلاديمير الكسندروفيتش Voevodsky ، اكتشفت خطأ في واحدة من البراهين له. منذ ذلك الحين وحتى وفاته في عام 2017 ، شجع بنشاط على استخدام أجهزة الكمبيوتر للتحقق من الأدلة. قال هالز إنه وجد وفيرغسون مئات الأخطاء في البراهين الأصلية عن طريق اختبارها باستخدام أجهزة الكمبيوتر. حتى النظريات الأولى في عناصر إقليدس ليست مثالية. إذا كانت الآلة قادرة على مساعدة علماء الرياضيات في تجنب مثل هذه الأخطاء ، فلماذا لا تستغلها؟ قدم هاريس اعتراضًا عمليًا على هذا الاقتراح ، ومع ذلك ، فمن غير المعروف مدى معقولية: إذا كان على علماء الرياضيات قضاء بعض الوقت في صياغة الرياضيات للكمبيوتر لفهمها ، فلن يتمكنوا من قضاء ذلك الوقت في الرياضيات الجديدة.



ومع ذلك ، Timati Gowers، عالم رياضيات وعالم رياضيات حائز على جائزة كامبريدج فيلدز ، يريد أن يذهب أبعد من ذلك: فهو يتصور كيف ستحل مبرهنات النظرية محل المراجعين البشريين في المجلات الرئيسية في المستقبل. "أرى كيف يمكن أن يصبح هذا ممارسة قياسية - إذا كنت تريد قبول عملك ، فعليك تشغيله من خلال مراجع آلي."

محادثة مع أجهزة الكمبيوتر

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



صُممت مبرهنات نظرية اليوم دون اعتبار لمدى الود في الرياضيات. النوع الأول ، ATP ، شائع الاستخدام لاختبار حقيقة البيان ، غالبًا عن طريق اختبار جميع الخيارات الممكنة. اسأل اتحاد لاعبي التنس المحترفين إذا كان من الممكن السفر من ميامي إلى سياتل ، ومن المحتمل أن يمر عبر جميع المدن التي تؤدي إليها الطرق من ميامي ، وفي النهاية سيجد المدينة التي تؤدي إلى سياتل.





يعتقد Timati Gowers من جامعة كامبريدج أن المبرّفات النظرية ستحل يومًا ما محل المراجعين البشريين



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



لكن هناك مشكلة: ATP لا تشرح عملها. تتم جميع العمليات الحسابية داخل آلة ، وتبدو بالنسبة لشخص ما مثل سلسلة طويلة من الأصفار والآحاد. قال هوانغ إنه كان من المستحيل النظر إلى الدليل واختبار المنطق ، لأنه يبدو وكأنه مجموعة من البيانات العشوائية. قال: "لا أحد يستطيع أن ينظر إلى مثل هذه الأدلة ويقول: كل شيء واضح".



تحتوي الفئة الثانية ، ITP ، على مجموعات بيانات ضخمة تحتوي على عشرات الآلاف من النظريات والأدلة التي يمكن من خلالها التحقق من دقة الإثبات. على عكس ATPs ، التي تعمل داخل الصندوق الأسود الذي يصدر ردودًا ببساطة ، تتطلب ITPs التفاعل وأحيانًا التوجيه من شخص ، لذا فهي ليست بعيدة المنال. قال هوانغ: "يمكن لأي شخص أن يجلس ويصف التقنيات المستخدمة لإثبات ذلك". تمت دراسة هذه الأدلة من قبل ديديو وفيتيري.



في السنوات الأخيرة ، أصبحت ITPs ذات شعبية متزايدة. في عام 2017 ، استخدم الثالوث الذي أثبت المشكلة المنطقية لثلاثيات فيثاغورس ITP يسمى Coq لإنشاء واختبار نسخة رسمية من برهانهم. في عام 2005 ، استخدم جورج غونتييه من Microsoft Research Cambridge Coq لإضفاء الطابع الرسمي على نظرية الألوان الأربعة. استخدم Hales أيضًا ITPs المسماة HOL Light و Isabelle لإثبات تخمين كيبلر رسميًا (HOL تعني منطق الترتيب الأعلى).



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

حدود التفكير

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



جزئيًا ، استوحى Urban من عمل Andrei Karpaty ، الذي درب منذ عدة سنوات شبكة عصبية لإنتاج هراء رياضي بدا مقنعًا لغير المتخصصين. لكن Urban لم يكن بحاجة إلى هذا الهراء - فقد طور هو والمجموعة أداتهم الخاصة للبحث عن البراهين ، بعد أن تدربوا على ملايين النظريات. استخدموا الشبكة لتوليد فرضيات جديدة واختبار صحتها باستخدام برنامج ATP يسمى E.



أصدرت الشبكة أكثر من 50000 صيغة جديدة ، على الرغم من تكرار عشرات الآلاف منها. قال أوربان: "يبدو أننا لا نستطيع حتى الآن إثبات فرضيات أكثر إثارة للاهتمام".



يرى Szegedi من Google Research مشكلة الاستدلال التلقائي في أدلة الكمبيوتر كجزء من مجال أوسع بكثير: معالجة اللغة الطبيعية ، والتي تتضمن التعرف على الأنماط في استخدام الكلمات والجمل. يعد التعرف على الأنماط أيضًا فكرة أساسية عن رؤية الكمبيوتر ، والتي عمل عليها Szegedi سابقًا في Google. مثل المجموعات الأخرى ، يريد فريقه إنشاء محرِّكات نظرية يمكنها البحث عن براهين مفيدة وشرحها.



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



وصفت مجموعته في Google Research مؤخرًا طريقة لاستخدام النماذج اللغوية - التي تستخدمها الشبكات العصبية غالبًا - لتوليد أدلة جديدة. بعد تدريب النموذج على التعرف على بنية الشجرة للنظريات المثبتة ، أطلقوا تجربة مجانية ، ببساطة يطلبون من الشبكات العصبية إنشاء وإثبات النظريات دون إشراف. من بين آلاف الفرضيات التي تم إنشاؤها ، تبين أن 13٪ قابلة للإثبات وجديدة (وليس تكرار النظريات الأخرى في قاعدة البيانات). قال إن مثل هذه التجربة تقول أن الشبكات العصبية يمكنها أن تتعلم ، بمعنى ما ، أن تفهم كيف يبدو الدليل.



قال سيجيدي: "الشبكات العصبية قادرة على تطوير مظهر مصطنع من الحدس".



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



بعد كل شيء ، إذا تطورت الآلات أكثر فأكثر ، وتمكنت من الوصول إلى كمية هائلة من البيانات ، فيجب أن تتعلم القيام بأشياء جيدة ومثيرة للاهتمام. قال جاورز: "سوف يتعلمون تقديم طلباتهم بأنفسهم".



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