هوش مصنوعی استدلال ریاضی: گفته می شود در دهه 1970 ، پل کوهن ، ریاضیدان فقید ، تنها کسی که موفق به کسب مدال فیلدز برای کار در منطق ریاضی شده است ، پیش بینی گسترده ای را انجام داد که همچنان ریاضی دانان را تحریک می کند – که “در آینده نامشخص ، ریاضیدانان توسط رایانه جایگزین می شوند ” کوهن که به دلیل روشهای جسورانه خود در تئوری مجموعه افسانه ای است ، پیش بینی کرد که همه ریاضیات می توانند خودکار باشند ، از جمله نوشتن اثبات. در نتیجه هوش مصنوعی استدلال ریاضیات را می تواند انجام دهد.
اثبات یک بحث منطقی گام به گام است که صحت یک حدس یا یک گزاره ریاضی را تأیید می کند. (هنگامی که اثبات شد ، یک حدس به یک قضیه تبدیل می شود.) هم اعتبار یک جمله را تأیید می کند و هم دلیل درست بودن آن را توضیح می دهد. هر چند یک دلیل عجیب است.این فرایند می تواند عجیب باشد زیرا این یک تجربه انتزاعی و غیر قابل تجسم است.
سایمون دی دئو ، دانشمند علوم شناختی از دانشگاه کارنگی ملون ، که یقین هوش مصنوعی استدلال ریاضی را با تجزیه و تحلیل ساختار اثبات مطالعه می کند ، گفت: ” این یک تماس دیوانه وار بین جهانی خیالی ، غیر فیزیکی و موجودات تکامل یافته بیولوژیکی هستند.” او معتقد است که ما در حال حاضر آنقدر پیشرفت نکرده ایم تا این مفاهیم برایمان قابل درک باشد.
رایانه ها برای محاسبات بزرگ مفید هستند ، اما اثبات آن چیز دیگری می خواهد. حدس ها از استدلال استقرایی ناشی می شود – نوعی شهود در مورد یک مسئله جالب – و اثبات ها به طور کلی از منطق قیاسی و گام به گام پیروی می کنند. آنها اغلب به فکر خلاق پیچیده و همچنین کار پر زحمت بیشتری برای پر کردن خلا نیاز دارند و ماشین آلات نمی توانند به این ترکیب دست پیدا کنند. پس چگونه هوش مصنوعی استدلال ریاضیات پیدا می کن ؟
اثبات قضیه رایانه ای را می توان به دو دسته تقسیم کرد. ارائه دهنده قضیه خودکار یا ATP ، معمولاً از روش های brute-force برای خرد کردن محاسبات بزرگ استفاده می کنند. اثبات قضیه تعاملی یا ITP ، به عنوان دستیار اثبات عمل می کنند که می توانند صحت هوش مصنوعی استدلال ریاضی را تأیید کرده و اثبات های موجود را برای خطا بررسی کنند. اما این دو استراتژی ، حتی اگر با هم ترکیب شوند (همانطور که در مورد قضیه های جدیدتر ارائه می شود) ، به استدلال خودکار اضافه نمی شوند.
یک چالش جدی در این زمینه وجود دارد که می پرسد چقدر از اثبات ریاضی در حقیقت می تواند خودکار شود: آیا یک سیستم می تواند حدس جالبی ایجاد کند و آن را به شکلی که مردم درک کنند اثبات کند؟ تعداد زیادی از پیشرفتهای اخیر آزمایشگاه ها در سراسر جهان روشهایی را پیشنهاد می کند که ابزارهای هوش مصنوعی استدلال ریاضی می توانند به این سوال با استدلال پاسخ دهند.
یوزف اوربان در انستیتوی انفورماتیک ، رباتیک و سایبرنتیک چک در پراگ در حال بررسی روشهای مختلفی است که با استفاده از یادگیری ماشینی کارایی و عملکرد ارائه دهنده های موجود را افزایش می دهد. در ماه ژوئیه ، گروه وی مجموعه ای از حدس و گمان های اصلی را که توسط ماشین آلات تولید و تأیید شده است ، گزارش کرد. در ماه ژوئن ، گروهی در Google Research به سرپرستی Christian Szegedy نتایج اخیر نتایج تلاش برای استفاده از نقاط قوت پردازش زبان طبیعی را برای اثبات رایانه در ساختار و توضیحات انسانی ارسال کردند.
ریاضیدانان ، منطق دانان و فلاسفه مدتها است که بر سر این که کدام قسمت از اثبات اساساً انسانی است بحث کرده اند و بحث ها درباره ریاضیات مکانیزه امروزه نیز ادامه دارد ، به ویژه در بحث های عمیق متصل به علوم کامپیوتر و هوش مصنوعی استدلال ریاضیات محض. برای دانشمندان رایانه ، اثبات قضیه بحث برانگیز نیست.
آنها راهی دقیق برای تأیید عملکرد یک برنامه ارائه می دهند و بحث در مورد شهود و خلاقیت از یافتن راهی کارآمد برای حل یک مسئله اهمیت کمتری دارد. به عنوان مثال ، در مموسسه فناوری ماساچوست ، آدام چلیپالا ، دانشمند کامپیوتر ، ابزارهایی را برای اثبات قضیه طراحی کرده است که الگوریتم های رمزنگاری را تولید می کند – که به طور سنتی توسط انسان نوشته , طراحی می شود که معمولا برای محافظت در معاملات اینترنتی استفاده می شود.
