توسط: استیون اونرز
۲۷ آگست، ۲۰۲۰
هوش مصنوعی، اثبات کننده های فرضیوی و همرای آنها، روابط میان ریاضی و ماشین را تغییر شکل میدهد.
در سال 1970 م. پاول کوهن ریاضیدان فقید، یگانه کسی که برنده مدال میدانی در بخش منطق ریاضی است، پیش بینی کرد که “در آینده نه چندان دور، ریاضیدانان با ماشین ها جایگزین خواهند شد”. کوهن، با کار های قهرمانانه خود در زمینه فرضیه مجموعه ها، گفت که تمام بخش های ریاضی نظیر نوشتن اثبات ها خودکار میشوند.
اثبات، مجموعه از استدلال های منطقی قدم به قدم برای اثبات صحت یک حدس یا قضیه ریاضی است. (زمانی که حدس یا قضیه اثبات شد، تبدیل به برهان یا تیوریم می شود) هر دو حدس و قضیه، صحت یک جمله را تعیین کرده و تشریح میکنند که چرا باید حدس یا قضیه درست باشد.
اثبات یک قضیه یا حدس، به نوعی عجیب است، اثبات یک مسئله خیالی و غیر وابسته به تجربه های مادی هست. سیمون دیدیو از دانشگاه کارنیج میلون، که مسلم های ریاضیکی را با تحلیل و تجزیه ساختار اثبات ها مطالعه میکند، گفته است “آنها (اثبات) یک رابطه عجیب میان یک دنیای خیالی و غیر فزیکی با دنیای موجودات تکامل یافته بیالوژیکی هستند”.
کمپیوتر ها برای محاسبات پیچیده یا بزرگ مناسب هستند، اما اثبات چیزی متفاوت نیاز دارد.
حدس ها از استدلال استقرای بوجود میآیند، استدلال استقرایی نوعی درک مستقیم روی یک مسئله جالب است. اثبات ها معمولا از یک روند منطقی قدم به قدم و قیاسی استفاده میکنند. اثبات ها نیاز به تفکر خلاقانه و پرش از روی موانع بوجود آمده دارند، چیزی که کمپیوتر ها فاقد آن هستند.
اثبات کننده های ماشینی، معمولا به دو بخش: اثبات کننده های خودکار (ا تی پی) که معمولا از روش جستجوی کورکورانه برای حل اثبات ها استفاده میکنند، و اثبات کننده های متقابل، که مانند یک دستیار اثبات در بخش تعیین صحت حدس ها و بررسی اثبات ها برای مشکلات موجود عمل میکنند. این استراتیژی ها حتی زمانی که با هم ترکیب می شوند (مانند اثبات کننده های نوین) قادر به خودکار سازی استدلال ها نیستند.
بر علاوه، این برنامه با آغوش باز از طرف ریاضیدانان پذیرفته نمی شود، دیدیو می گوید که “این اثبات کننده ها برای ریاضیدانان تا حد زیادی جنجال برانگیز هستند”.
یکی از چالش های قوی در این بخش، این است که تا چه حد از روند اثبات باید خودکار سازی شود، آیا یک سیستم قادر است که یک حدس را بسازد و آنرا به نوعی اثبات کند که برای انسان ها قابل فهم باشد؟ پیشرفت های بدست آمده در لابراتوار های سراسر جهان، پیشنهاد می کنند که برنامه های هوش مصنوعی معاصر شاید به این سوال پاسخ بدهد. یوسف اوربان از انستیتو انفورماتیک، روباتیک و سایبرنیتک چک در پراگ در حال بررسی روش های مبتنی بر یادگیری ماشینی برای افزایش موثریت و عملکرد اثبات کننده های فعلی هست. در ماه جولای، گروه او مجموعه ای از حدس ها و اثبات آنها را که از طریق ماشین صورت گرفته بود، منتشر کرد.
بعضی از ریاضیدانان، اثبات کننده ها را مانند یک برنامه انقلابی در عرصه نوشتن اثبات ها میدانند. بعضی دیگر می گویند که اصولا نوشتن اثبات برای ریاضیات پیشرفته غیر ضروری و احتمالا ناممکن خواهد بود. اما یک سیستمی که حدس جدیدی بزند و برهان جدیدی را اثبات کند قادر خواهد بود تا به نحوی به استدلال سازی خودکار برسد.
