التدقيق بمساعدة الحاسوب
البرهان بمساعدة الحاسوب هو برهان رياضي تم إنشاؤه جزئياً على الأقل بواسطة الحاسوب .
معظم البراهين المدعومة بالحاسوب حتى الآن هي تطبيقات لبراهين مطولة تعتمد على استنفاد الحلول لنظرية رياضية . الفكرة هي استخدام برنامج حاسوبي لإجراء حسابات مطولة، وتقديم برهان يثبت أن نتيجة هذه الحسابات تستلزم النظرية المعطاة. في عام ١٩٧٦، كانت نظرية الألوان الأربعة أول نظرية رئيسية يتم التحقق منها باستخدام برنامج حاسوبي .
بُذلت محاولات في مجال أبحاث الذكاء الاصطناعي لإنشاء براهين جديدة أصغر وأكثر وضوحًا لنظريات رياضية، انطلاقًا من الأساسيات، باستخدام تقنيات الاستدلال الآلي ، مثل البحث الاستدلالي . وقد أثبتت هذه البرامج الآلية لإثبات النظريات عددًا من النتائج الجديدة، ووجدت براهين جديدة لنظريات معروفة. إضافةً إلى ذلك، تُمكّن برامج المساعدة التفاعلية في البراهين علماء الرياضيات من تطوير براهين سهلة القراءة، مع التحقق الرسمي من صحتها. ولأن هذه البراهين قابلة للمراجعة البشرية عمومًا (وإن كان ذلك بصعوبة، كما هو الحال مع برهان حدسية روبنز )، فإنها لا تنطوي على الآثار الجدلية المترتبة على البراهين الحاسوبية التي تعتمد على الاستنفاد.
طُرق
إحدى طرق استخدام الحواسيب في البراهين الرياضية هي ما يُعرف بالحسابات العددية المُدققة أو الحسابات العددية الدقيقة. وهذا يعني إجراء الحسابات عدديًا مع الحفاظ على الدقة الرياضية. يُستخدم في هذه الطريقة الحساب متعدد القيم ومبدأ الاحتواء لضمان احتواء ناتج البرنامج العددي متعدد القيم على حل المسألة الرياضية الأصلية. ويتم ذلك من خلال التحكم في أخطاء التقريب والاقتطاع، واحتواءها، ونشرها، باستخدام، على سبيل المثال، حساب الفترات . وبشكل أدق، يتم اختزال الحساب إلى سلسلة من العمليات الأساسية، على سبيل المثالفي الحاسوب، تُقرّب نتيجة كل عملية حسابية أولية بدقة الحاسوب. مع ذلك، يمكن إنشاء نطاق يُحدد بحدود عليا وسفلى لنتيجة العملية الحسابية الأولية. ثم يُستبدل عددٌ بنطاقات، وتُجرى العمليات الحسابية الأولية بين هذه النطاقات من الأعداد القابلة للتمثيل.
الاعتراضات الفلسفية
تُعدّ البراهين المُساعدة بالحاسوب موضوعًا مثيرًا للجدل في عالم الرياضيات، وكان توماس تيموتشكو أول من طرح اعتراضات عليها. ويرى أنصار تيموتشكو أن البراهين المطوّلة المُساعدة بالحاسوب ليست، بمعنى ما، براهين رياضية "حقيقية" لأنها تتضمن خطوات منطقية كثيرة يصعب على البشر التحقق منها عمليًا ، وأن الرياضيين يُطلب منهم فعليًا استبدال الاستدلال المنطقي من البديهيات المفترضة بالثقة في عملية حسابية تجريبية، والتي قد تتأثر بأخطاء في برنامج الحاسوب، فضلًا عن عيوب في بيئة التشغيل والأجهزة. [ 1 ]
يعتقد بعض علماء الرياضيات أن البراهين المطولة التي تُجرى بمساعدة الحاسوب يجب اعتبارها حسابات ، لا براهين : إذ ينبغي إثبات صحة خوارزمية البرهان نفسها، بحيث يُمكن اعتبار استخدامها مجرد "تحقق". ويمكن دحض الادعاءات بأن البراهين التي تُجرى بمساعدة الحاسوب عُرضة للأخطاء في برامجها المصدرية ومترجماتها وأجهزتها، من خلال تقديم برهان رسمي على صحة برنامج الحاسوب (وهو نهج طُبِّق بنجاح على نظرية الألوان الأربعة عام ٢٠٠٥)، بالإضافة إلى إعادة إنتاج النتيجة باستخدام لغات برمجة ومترجمات وأجهزة حاسوب مختلفة.
ثمة طريقة أخرى ممكنة للتحقق من صحة البراهين المُنشأة بمساعدة الحاسوب، وهي توليد خطوات الاستدلال بصيغة قابلة للقراءة آليًا ، ثم استخدام برنامج مدقق البراهين لإثبات صحتها. ولأن التحقق من صحة برهان مُعين أسهل بكثير من إيجاد برهان، فإن برنامج المدقق أبسط من البرنامج المساعد الأصلي، وبالتالي يسهل اكتساب الثقة في صحته. مع ذلك، لا يروق هذا النهج، الذي يستخدم برنامج حاسوب لإثبات صحة مُخرجات برنامج آخر، للمشككين في البراهين الحاسوبية، الذين يرونه إضافةً لطبقة أخرى من التعقيد دون مراعاة الحاجة المُلحة للفهم البشري.
من الحجج الأخرى ضد البراهين المدعومة بالحاسوب أنها تفتقر إلى الأناقة الرياضية ، أي أنها لا تقدم أي رؤى أو مفاهيم جديدة ومفيدة. وهذه حجة يمكن توجيهها ضد أي برهان مطوّل يعتمد على الاستنفاد.
تُثير البراهين المدعومة بالحاسوب مسألة فلسفية إضافية، وهي ما إذا كانت تُحوّل الرياضيات إلى علم شبه تجريبي ، حيث يصبح المنهج العلمي أكثر أهمية من تطبيق العقل المجرد في مجال المفاهيم الرياضية المجردة. ويرتبط هذا ارتباطًا مباشرًا بالجدل الدائر في الرياضيات حول ما إذا كانت الرياضيات قائمة على الأفكار، أم أنها "مجرد" تمرين في معالجة الرموز الشكلية. كما يُثير هذا التساؤل، إذا كان، وفقًا للرؤية الأفلاطونية ، جميع الكائنات الرياضية الممكنة "موجودة بالفعل" بمعنى ما، فهل تُعدّ الرياضيات المدعومة بالحاسوب علمًا قائمًا على الملاحظة كعلم الفلك، أم أنها علم تجريبي كعلم الفيزياء أو الكيمياء؟ ويتزامن هذا الجدل في الرياضيات مع تساؤلات تُطرح في أوساط الفيزياء حول ما إذا كانت الفيزياء النظرية في القرن الحادي والعشرين تُصبح رياضية أكثر من اللازم، وتتخلى عن جذورها التجريبية.
يواجه مجال الرياضيات التجريبية الناشئ هذا النقاش بشكل مباشر من خلال التركيز على التجارب العددية كأداة رئيسية للاستكشاف الرياضي.
تم إثبات النظريات بمساعدة برامج الحاسوب
لا يعني إدراج أي عنصر في هذه القائمة وجود دليل رسمي تم التحقق منه بواسطة الحاسوب، بل يعني فقط أن برنامج حاسوبي قد شارك بطريقة ما. راجع المقالات الرئيسية لمزيد من التفاصيل.
- مشكلة النقطة الثابتة المشتركة ، 1967 [ 2 ]
- نظرية الألوان الأربعة ، 1976 [ 3 ]
- فرضية ميتشل فيجنباوم حول الشمولية في الديناميكا غير الخطية. تم إثباتها بواسطة أو إي لانفورد باستخدام حسابات حاسوبية دقيقة، 1982
- لعبة "كونكت فور" ، 1988 - لعبة محلولة
- عدم وجود مستوى إسقاطي محدود من الرتبة 10، 1989
- فرضية الفقاعة المزدوجة ، 1995 [ 4 ]
- تخمين روبنز ، 1996
- تخمين كيبلر ، 1998 - مشكلة التعبئة المثلى للكرات في صندوق
- جاذب لورنز ، 2002 – المسألة الرابعة عشرة من مسائل سميل ، أثبتها وارويك تاكر باستخدام حساب الفترات
- حالة من 17 نقطة لمشكلة النهاية السعيدة ، 2006
- قام كوريل [ 5 ] [ 6 ] [ 7 ] (بين عامي 2006 و2016) بحساب العديد من أرقام فان دير فاردن باستخدام محلل SAT القائم على FPGA .
- صعوبة NP للتثليث ذي الوزن الأدنى ، 2008
- قام أحمد [ 8 ] [ 9 ] [ 10 ] [ 11 ] [ 12 ] (بين عامي 2009 و2014) بحساب العديد من أعداد فان دير فاردن باستخدام خوارزمية DPLL لحل مسائل SAT، سواءً كانت مستقلة أو موزعة. استخدم أحمد لأول مرة خوارزميات SAT الموزعة على مستوى المجموعات لإثبات أن w(2; 3, 17) = 279 و w(2; 3, 18) = 312 في عام 2010. [ 9 ]
- يمكن الحصول على الحلول المثلى لمكعب روبيك في 20 حركة وجه على الأكثر، 2010 [ 13 ]
- الحد الأدنى لعدد الأدلة اللازمة لحل لغز سودوكو هو 17، 2012
- في عام 2014، تم حل حالة خاصة من مسألة التباين لإردوش باستخدام برنامج حل SAT . وفي وقت لاحق، تم حل التخمين الكامل بواسطة تيرينس تاو دون مساعدة حاسوبية. [ 14 ]
- تم حل مشكلة الأعداد الثلاثية المنطقية باستخدام 200 تيرابايت من البيانات في مايو 2016. [ 15 ]
- تطبيقات على نظرية كولموغوروف-أرنولد-موسر [ 16 ] [ 17 ]
- خاصية كازدان (T) لمجموعة التشاكل الذاتي لمجموعة حرة رتبتها خمسة على الأقل
- رقم شور الخامس ، تم الإعلان عن البرهان على أن S(5) = 161 في عام 2017 بواسطة ماريجن هيول واستغرق 2 بيتابايت من المساحة [ 18 ] [ 19 ]
- تخمين كيلر في البعد 7 هو الحالة الوحيدة المتبقية في عام 2020 مع برهان بحجم 200 جيجابايت [ 20 ] [ 21 ]
- يبلغ عدد الألوان للتعبئة للشبكة المربعة اللانهائية 15، وذلك وفقًا لما ذكره سوبركاسو وهيول في عام 2023 [ 22 ] [ 23 ] (انظر أيضًا: مسألة هادويجر-نيلسون لعدد الألوان للمستوى).
انظر أيضاً
- التحقق الرسمي – إثبات أو دحض صحة خوارزميات معينة مقصودة
- نظرية المنطق – برنامج حاسوبي صدر عام 1956 من تأليف ألين نيويل، وهربرت أ. سيمون، وكليف شو
- البرهان الرياضي – الاستدلال على العبارات الرياضية
- الرياضيات الميتا - لغة رسمية وبرنامج حاسوبي مرتبط بها
- التحقق من النماذج - مجال علوم الحاسوب
- سبعة عشر أو لا شيء – عدد فردي بخصائص محددة. صفحات تعرض أوصافًا مختصرة لأهداف إعادة التوجيه.
- الحساب الرمزي – مجال علمي يقع على مفترق طرق علوم الحاسوب والرياضيات. صفحات تعرض وصفًا موجزًا لأهداف إعادة التوجيه.
- الأرقام المعتمدة
مراجع
- ↑ تيموتشكو، توماس (1979)، "مسألة الألوان الأربعة وأهميتها الرياضية"، مجلة الفلسفة ، 76 (2): 57-83 ، doi : 10.2307/2025976 ، JSTOR 2025976 .
- ↑ بويس، ويليام م. (مارس 1969). "الدوال التبادلية بدون نقطة ثابتة مشتركة" (ملف PDF) . معاملات الجمعية الرياضية الأمريكية . 137 : 77-92 . doi : 10.1090/S0002-9947-1969-0236331-5 .
- ↑ غونتييه، جورج (2008)، "برهان رسمي - نظرية الألوان الأربعة" (ملف PDF) ، إشعارات الجمعية الرياضية الأمريكية ، 55 (11): 1382-1393 ، MR 2463991 ، مؤرشف (ملف PDF) من الأصل بتاريخ 2011-08-05
- ↑ هاس، ج.؛ هاتشينغز، م.؛ شلافلي، ر. (1995). "فرضية الفقاعة المزدوجة" . الإعلانات البحثية الإلكترونية للجمعية الرياضية الأمريكية . 1 (3): 98-102 . CiteSeerX 10.1.1.527.8616 . doi : 10.1090/S1079-6762-95-03001-0 .
- ↑ كوريل، ميشال (2006). إطار عمل للتراجع لمجموعات بيوولف مع امتداد لحسابات المجموعات المتعددة وتنفيذ مشكلة معيارية لإرضاء النظام (أطروحة دكتوراه). جامعة سينسيناتي.
- ^ كوريل ، ميشال (2012). "حساب رقم فان دير وايردن W(3,4)=293". الأعداد الصحيحة . 12 : أ46. السيد 3083419 .
- ↑ كوريل، ميشال (2015). "الاستفادة من مجموعات FPGA لحسابات SAT". الحوسبة المتوازية: على طريق إكساسكيل : 525-532 .
- ^ أحمد، طنبير (2009). "بعض أرقام van der Waerden الجديدة وبعض أرقام van der Waerden". الأعداد الصحيحة . 9 : أ6. دوى : 10.1515/integ.2009.007 . السيد 2506138 . S2CID 122129059 .
- أحمد ، تنبير ( 2010 ). "عددان جديدان من أعداد فان دير فاردن w(2;3,17) و w(2;3,18)". الأعداد الصحيحة . 10 (4): 369-377 . doi : 10.1515/integ.2010.032 . MR 2684128. S2CID 124272560 .
- ^ أحمد، طنبير (2012). “حول حساب أرقام فان دير وايردن الدقيقة”. الأعداد الصحيحة . 12 (3): 417-425 . دوى : 10.1515/integ.2011.112 . السيد 2955523 . S2CID 11811448 .
- ↑ أحمد، تنبير (2013). "بعض أعداد فان دير فاردن الأخرى". مجلة متواليات الأعداد الصحيحة . 16 (4): 13.4.4. MR 3056628 .
- ↑ أحمد، تنبير؛ كولمان، أوليفر؛ سنيفيلي، هنتر (2014). "حول أعداد فان دير فاردن w(2;3,t)" . الرياضيات التطبيقية المتقطعة . 174 (2014): 27-51 . arXiv : 1102.5433 . doi : 10.1016/j.dam.2014.05.007 . MR 3215454 .
- ↑ "رقم الله هو 20" . cube20.org . يوليو 2010. تم الاطلاع عليه بتاريخ 18 أكتوبر 2023 .
- ↑ سيزار، كريس (1 أكتوبر 2015). "عبقري رياضيات يحل لغزًا محيرًا" . مجلة نيتشر . 526 (7571): 19-20 . Bibcode : 2015Natur.526...19C . doi : 10.1038/nature.2015.18441 . PMID 26432222 .
- ↑ لامب، إيفلين (26 مايو 2016). "برهان رياضي بحجم 200 تيرابايت هو الأكبر على الإطلاق" . مجلة نيتشر . 534 (7605): 17-18 . Bibcode : 2016Natur.534...17L . doi : 10.1038/nature.2016.19990 . PMID 27251254 .
- ↑ سيليتي، أ.؛ تشيركيا، ل. (1987). "تقديرات دقيقة لنظرية KAM بمساعدة الحاسوب" . مجلة الفيزياء الرياضية . 28 (9): 2078-2086 . Bibcode : 1987JMP....28.2078C . doi : 10.1063/1.527418 .
- ↑ فيغيراس، جيه إل؛ هارو، أ؛ لوكي، أ. (2017). "تطبيق دقيق لنظرية KAM بمساعدة الحاسوب: منهج حديث" . أسس الرياضيات الحاسوبية . 17 (5): 1123-1193 . arXiv : 1601.00084 . doi : 10.1007/s10208-016-9339-3 . hdl : 2445/192693 . S2CID 28258285 .
- ^ هيول، مارين جيه إتش (2017). "شور رقم خمسة". أرخايف : 1711.08076 [ cs.LO ].
- ↑ "شور رقم خمسة" . www.cs.utexas.edu . تم الاطلاع عليه بتاريخ 2021-10-06 .
- ^ براكينسيك، جوشوا. هيول، مارين؛ ماكي، جون. نارفايز ، ديفيد (2020). “حل تخمين كيلر”. في بلتيير، نيكولاس؛ سوفروني-ستوكرمانز، فيوريكا (محرران). الاستدلال الآلي . ملاحظات محاضرة في علوم الكمبيوتر. المجلد. 12166. سبرينغر. ص 48 – 65. دوى : 10.1007 / 978-3-030-51074-9_4 . رقم ISBN 978-3-030-51074-9. PMC 7324133 .
- ↑ هارتنيت، كيفن (19 أغسطس 2020). "بحث حاسوبي يحل مشكلة رياضية عمرها 90 عامًا" . مجلة كوانتا . تم الاطلاع عليه بتاريخ 8 أكتوبر 2021 .
- ↑ سوبركاسو، برناردو؛ هيول، مارين جيه إتش (23 يناير 2023). "العدد اللوني للتعبئة في الشبكة المربعة اللانهائية هو 15". أدوات وخوارزميات لبناء وتحليل الأنظمة . سلسلة محاضرات في علوم الحاسوب. المجلد 13993. الصفحات 389-406 . arXiv : 2301.09757 . doi : 10.1007 /978-3-031-30823-9_20 . ISBN 978-3-031-30822-2.
- ↑ هارتنيت، كيفن (2023-04-20). "الرقم 15 يصف الحد السري لشبكة لا نهائية" . مجلة كوانتا . تم الاطلاع عليه بتاريخ 2023-04-20 .
للمزيد من القراءة
- لينات، د.ب. (1976). أ.م.: منهج الذكاء الاصطناعي للاكتشاف في الرياضيات كبحث استدلالي (ملف PDF) (أطروحة دكتوراه). مختبر الذكاء الاصطناعي، جامعة ستانفورد. STAN-CS-76-570، تقرير مشروع البرمجة الاستدلالية HPP-76-8.
- ماير، ك. ر.؛ شميدت، د. س.، محرران. (2012). البراهين بمساعدة الحاسوب في التحليل . مجلدات معهد الرياضيات التطبيقية في الرياضيات وتطبيقاتها. المجلد 28. سبرينغر. ISBN 978-1-4613-9092-3.
- ناكاو، م.؛ بلوم، م.؛ واتانابي، ي. (2019). طرق التحقق العددي والبراهين بمساعدة الحاسوب للمعادلات التفاضلية الجزئية . سلسلة سبرينغر في الرياضيات الحاسوبية. سبرينغر. ISBN 9789811376696.
روابط خارجية
- لانفورد، أوسكار إي. (1982). "برهان بمساعدة الحاسوب لتخمينات فيجنباوم" (ملف PDF) . نشرة الجمعية الأمريكية للرياضيات ، 6 (3): 427-434 . CiteSeerX 10.1.1.434.8389 . doi : 10.1090/S0273-0979-1982-15008-X .
- فورس، إدموند (1990). لماذا نفدت طاقة AM؟ (تقرير فني). قسم دراسات الحاسوب، جامعة جلامورجان. CS-90-4. مؤرشف من الأصل بتاريخ 17 يوليو 2012. تم الاطلاع عليه بتاريخ 6 سبتمبر 2016 .
{{cite tech report}}: CS1 maint: bot: حالة عنوان URL الأصلي غير معروفة ( رابط ) - بيجلي، س. (16 أبريل 2018). "قد تخطئ البراهين العددية التي تُجرى بواسطة الحاسوب" . بيتسبرغ بوست غازيت . مؤرشف من الأصل بتاريخ 16 أبريل 2018.
- "عدد خاص حول البرهان الرسمي" . إشعارات الجمعية الرياضية الأمريكية . ديسمبر 2008.
- تكنولوجيا الحجج
- إثبات النظريات آلياً
- البراهين بمساعدة الحاسوب
- الأساليب الرسمية
- التحليل العددي
- فلسفة الرياضيات