کامپیوترها چقدر به خودکار کردن استدلال ریاضی نزدیک هستند؟

منتشرشده در QuantaMagazine به تاریخ ۲۷ آگوست ۲۰۲۰
لینک مقاله اصلی: How Close Are Computers to Automating Mathematical Reasoning?

در دهه ۱۹۷۰، پل کوهن، ریاضیدان فقید، تنها کسی که تا به حال یک مدال فیلدز را برای کار در منطق ریاضی برنده شده‌است، بنا بر گزارش‌ها یک پیش‌بینی کلی انجام داد که به تحریک و تهییج ریاضیدانان ادامه می‌دهد-که «در زمان نامشخص آینده، ریاضیدانان با کامپیوتر جایگزین خواهند شد» کوهن، که به خاطر روش‌های جسورانه‌اش در نظریه مجموعه‌ها، افسانه‌ای است، پیش‌بینی کرد که همه ریاضیات می‌توانند خودکار شوند، از جمله نوشتن اثبات.

اثبات یک استدلال منطقی گام‌به‌گام است که حقیقت یک حدس یا یک گزاره ریاضی را ثابت می‌کند. (وقتی ثابت شد، یک حدس تبدیل به یک قضیه می‌شود). اثبات هم اعتبار یک گزاره را مشخص می‌کند و هم توضیح می‌دهد که چرا آن گزاره درست است. اما اثبات عجیب است. انتزاعی بوده و به تجربه مادی وابسته نیست. Simon DeDeo، دانشمند علوم شناختی از دانشگاه کارنگی ملون، که با تحلیل ساختار شواهد، به بررسی قطعیت ریاضی می‌پردازد، می‌گوید: «آن‌ها این ارتباط دیوانه‌وار بین دنیای خیالی، غیر فیزیکی و موجودات تکامل‌یافته بیولوژیکی هستند. ما برای انجام این کار تکامل نیافته‌ایم.»

کامپیوترها برای محاسبات بزرگ مفید هستند اما اثبات به چیز متفاوتی نیاز دارد. حدسیات از استدلال استقرایی-نوعی شهود درباره یک مساله جالب-ناشی می‌شوند و شواهد عموما از منطق قیاسی گام‌به‌گام پیروی می‌کنند. آن‌ها اغلب به تفکر خلاق پیچیده و همچنین کار پرزحمت‌تر پر کردن شکاف‌ها نیاز دارند، و ماشین‌ها نمی‌توانند به این ترکیب دست یابند.

اثبات‌کننده‌های قضیه کامپیوتری را می توان به دو دسته تقسیم کرد. اثبات‌کننده‌های قضیه خودکار، یا ATP ها، معمولا از روش‌های پرقدرت برای خرد کردن از طریق محاسبات بزرگ استفاده می‌کنند. اثبات کنندگان قضیه تعاملی، یا ITP ها، به عنوان دستیاران اثبات عمل می‌کنند که می‌توانند از دقت یک استدلال اطمینان حاصل کرده و دلایل موجود برای خطاها را بررسی کنند. اما این دو استراتژی، حتی زمانی که با هم ترکیب می‌شوند (همان طور که در مورد اثبات‌کننده‌های قضیه جدیدتر صادق است) ، به استدلال خودکار اضافه نمی‌کنند.

به علاوه، این ابزارها با آغوش باز مورد استقبال قرار نگرفته‌اند و اکثر ریاضیدانان از آن‌ها استفاده و استقبال نمی‌کنند. DeDeo گفت: «آن‌ها برای ریاضیدانان بسیار بحث‌برانگیز هستند. اغلب آن‌ها این ایده را دوست ندارند.»

یک چالش آشکار و بزرگ در این زمینه این سوال را مطرح می‌کند که واقعا چقدر اثبات می‌تواند خودکار باشد: آیا یک سیستم می‌تواند یک حدس جالب ایجاد کند و به روشی آن را اثبات کند که مردم درک کنند؟ تعداد زیادی از پیشرفت‌های اخیر از آزمایشگاه‌های سراسر جهان راه‌هایی برا پاسخ ابزارهای هوش مصنوعی به این سوال را پیشنهاد می‌دهند. جوزف اوربن در موسسه انفورماتیک، رباتیک و سایبرنتیک چک در پراگ در حال بررسی رویکردهای مختلفی است که از یادگیری ماشین برای افزایش بهره‌وری و عملکرد وسایل موجود استفاده می‌کنند. در ماه جولای، گروه او مجموعه‌ای از فرضیات و شواهد اولیه را که توسط ماشین‌ها ایجاد و تایید شده بودند، گزارش دادند. و در ماه ژوئن، یک گروه در گوگل ریسرچ به رهبری Christian Szegedy نتایج اخیر را از تلاش برای مهار نقاط قوت پردازش زبان طبیعی برای ایجاد مدارک کامپیوتری به ظاهر انسانی‌تر در ساختار و توضیح منتشر کرد.

برخی از ریاضی دانان، اثبات‌کنندگان قضیه را به عنوان یک ابزار بالقوه تغییردهنده بازی برای آموزش نوشتن اثبات به دانشجویان دوره لیسانس می‌بینند. برخی دیگر می‌گویند که به کار گرفتن کامپیوتر برای نوشتن اثبات برای پیشرفت ریاضیات غیر ضروری و احتمالا غیرممکن است. Szegedy گفت که اما یک سیستم که می‌تواند یک حدس مفید را پیش‌بینی کرده و یک قضیه جدید را ثابت کند به چیزی جدید دست خواهد یافت-نوعی درک ماشینی. و این خود احتمال خودکارسازی استدلال را نشان می‌دهد.

ماشین‌های مفید

ریاضیدانان، منطق دانان و فلاسفه از دیرباز در مورد اینکه اساسا چه بخشی از ایجاد اثبات انسانی است، بحث کرده‌اند و امروزه مباحث مربوط به ریاضیات مکانیزه، به ویژه در دره‌های عمیق ارتباط دهنده علوم کامپیوتر و ریاضیات محض، ادامه دارد.

برای دانشمندان علوم کامپیوتر، اثبات‌کنندگان قضیه بحث‌برانگیز نیستند. آن‌ها یک روش دقیق برای تایید کارآمدی یک برنامه ارائه می‌کنند، و بحث درباره حدس و خلاقیت اهمیت کمتری از پیدا کردن یک روش کارآمد برای حل یک مساله دارد. برای مثال در موسسه فن‌آوری ماساچوست، دانشمند علوم کامپیوتر آدام چلیپالا ابزارهای اثبات قضیه را طراحی کرده‌است که الگوریتم های رمزنگاری-که به طور سنتی توسط انسان‌ها نوشته شده‌اند-را برای حفاظت از معاملات اینترنتی تولید می‌کند. در حال حاضر کد گروه او برای اکثر ارتباطات در مرورگر کروم گوگل مورد استفاده قرار می‌گیرد.

چلیپالا گفت: «شما می‌توانید از هر گونه استدلال ریاضی استفاده کرده و آن را با یک ابزار کدگذاری کنید و استدلال‌های خود را به هم متصل کنید تا دلایل امنیتی ایجاد شود.»

در ریاضیات، اثبات‌کنندگان قضیه به ایجاد اثبات‌های پیچیده و سنگینی کمک کرده‌است که در غیر این صورت صدها سال از عمر ریاضی‌دانان را به خود اختصاص می‌داد. حدس کپلر، که بهترین روش برای توده کردن گوی‌ها (یا، از نظر تاریخی، پرتقال‌ها یا توپ‌ها) را توصیف می‌کند، یک مثال گویا ارائه می‌دهد. در سال ۱۹۹۸، توماس هیلز به همراه شاگردش سم فرگوسن، اثبات را با استفاده از انواع تکنیک‌های ریاضی کامپیوتری شده کامل کردند. نتیجه آن‌چنان پیچیده بود-نتایج ۳ گیگابایت حجم داشتند-که ۱۲ ریاضی‌دان آن را سال‌ها آنالیز کردن تا بتوانند اعلام کنند که ۹۹٪ از صحت آن مطمئن هستند.

حدس کپلر تنها سوال مشهوری نیست که توسط ماشین‌ها حل می‌شود. قضیه چهار رنگ، که می‌گوید شما برای رنگ کردن هر نقشه دو بعدی فقط به چهار رنگ نیاز دارید، در سال ۱۹۷۷ توسط ریاضی دانان با استفاده از یک برنامه کامپیوتری که از طریق نقشه‌های پنج رنگ حرکت می‌کرد تا نشان دهد که همه آن‌ها را می‌توان به چهار کاهش داد، حل شد. و در سال ۲۰۱۶، سه ریاضی‌دان از یک برنامه کامپیوتری برای اثبات چالشی باز به نام مساله سه‌گانه‌های بولی فیثاغورث استفاده کردند، اما نسخه اولیه اثبات آن ۲۰۰ ترابایت بود. با یک ارتباط اینترنتی پرسرعت، یک فرد می‌تواند آن را در عرض سه هفته دانلود کند.

احساسات پیچیده

این مثال‌ها اغلب به عنوان موفقیت‌هایی سر و صدا می‌کنند، اما به بحث‌ها اضافه می‌کنند. بررسی کد کامپیوتری اثبات قضیه چهار رنگ، که بیش از ۴۰ سال پیش حل و فصل شده بود، برای انسان‌ها غیر ممکن بود. ریاضیدان مایکل هریس از دانشگاه کلمبیا گفت: «ریاضیدانان از آن زمان تا کنون بحث می‌کنند که آیا این یک اثبات است یا خیر.»

نکته دیگر این است که اگر ریاضیدان‌ها بخواهند از اثبات‌کنندگان قضیه استفاده کنند، ابتدا باید کد کردن را یاد بگیرند و سپس یاد بگیرند که چطور مشکل خود را به زبان آشنا با کامپیوتر بیان کنند. هریس گفت: «زمانی که من سوال خود را به شکلی که بتواند با این فن‌آوری متناسب باشد، شکل دادم، خودم مسئله را حل کردم.»

بسیاری از آن‌ها نیازی به حل‌کننده‌های قضیه در کارشان نمی‌بینند. کوین بورد، ریاضیدانی در کالج سلطنتی لندن که سه سال پیش کار خود را از ریاضیات محض برای تمرکز بر اثبات‌کنندگان قضیه و شواهد رسمی انتخاب کرد، گفت: «آن‌ها یک سیستم دارند، و این قلم و کاغذ است و کارآمد هم هست.» او گفت: «کامپیوترها محاسبات فوق‌العاده‌ای برای ما انجام داده‌اند، اما آن‌ها هرگز مشکل سختی را خودشان حل نکرده اند. تا وقتی که این کار را نکنند، ریاضی‌دانان نمی‌خواهند این چیزها را بخرند.»

اما بازارد و دیگران فکر می‌کنند که شاید آن‌ها باید این کار را بکنند. DeDeo گفت: «از یک نظر، اثبات‌های کامپیوتری ممکن است آنقدرها که ما فکر می‌کنیم بیگانه نباشند.» اخیرا، او به همراه اسکات ویتری، دانشمند علوم کامپیوتر که اکنون در دانشگاه استنفورد مشغول به کار است، تعدادی از برهان‌های متعارف مشهور (از جمله یکی از عناصر اقلیدس) و ده‌ها اثبات ماشینی که با استفاده از یک قضیه به نام Coq نوشته شده بودند را مهندسی کردند تا به دنبال نقاط مشترک باشند. آن‌ها دریافتند که ساختار شبکه‌ای اثبات ماشین بسیار شبیه به ساختار اثبات ساخته‌شده توسط مردم است. او گفت که این ویژگی مشترک ممکن است به محققان کمک کند تا راهی برای پیدا کردن دستیاران اثبات برای توضیح خودشان پیدا کنند.

DeDeo گفت: «اثبات‌های ماشینی ممکن است به آن اندازه که به نظر می‌رسند مرموز نباشند.»

برخی دیگر می‌گویند اثبات‌کنندگان قضیه می‌تواند ابزار آموزشی مفیدی هم در علوم کامپیوتر و هم در ریاضیات باشد. در دانشگاه جانز هاپکینز، ریاضیدانی به نام امیلی ریهل، دوره‌هایی را ایجاد کرده‌است که در آن دانشجویان با استفاده از اثبات‌کننده قضیه، اثبات را می‌نویسند. او گفت: «این کار را مجبور می‌کند که بسیار سازمان‌یافته باشید و به وضوح فکر کنید. دانش آموزانی که برای اولین بار اثبات‌هایی را می‌نویسند، می‌توانند در شناخت آنچه نیاز دارند و درک ساختار منطقی دچار مشکل شوند.»

ریهل همچنین می‌گوید که به طور فزاینده‌ای در کار خود از اثبات‌کنندگان قضیه استفاده کرده‌است. او گفت: « این لزوما چیزی نیست که شما مجبور باشید همیشه از آن استفاده کنید و هرگز جایگزین نوشتن بر روی یک تکه کاغذ نمی‌شود، اما استفاده از یک دستیار اثبات روش تفکر من در مورد نوشتن اثبات را تغییر داده‌است.»

اثبات‌کنندگان قضیه راهی برای صادق نگه داشتن موضوع نیز ارایه می‌دهد. در سال ۱۹۹۹ ولادیمیر وودوسکی ریاضیدان روسی آمریکایی در یکی از اثبات‌های خود خطایی را کشف کرد. از آن زمان تا زمان مرگش در سال ۲۰۱۷، او طرفدار استفاده از کامپیوتر برای بررسی اثبات‌ها بود. هالز گفت که وقتی او و فرگوسن اثبات اصلی خود را با کامپیوتر بررسی کردند، صدها خطا در آن یافتند. حتی اولین گزاره در عناصر اقلیدس کامل نیست. اگر یک ماشین می‌تواند به ریاضیدانان کمک کند تا از چنین اشتباهی اجتناب کنند، چرا از آن استفاده نکنند؟

اما تیموتی گوویرز، ریاضیدان و مدال‌دار فیلدز در دانشگاه کمبریج، می‌خواهد پا را فراتر بگذارد: او آینده‌ای را تصور می‌کند که در آن اثبات‌کنندگان قضیه جایگزین داوران انسانی در مجلات اصلی می‌شود. او گفت: «من می‌توانم ببینم که این یک روش استاندارد شده‌است که اگر می‌خواهید مقاله‌تان پذیرفته شود، باید آن را از یک جستجوگر خودکار عبور دهید.»

صحبت کردن با کامپیوترها

اما قبل از اینکه کامپیوترها بتوانند به طور جهانی اثبات‌ها را بررسی یا حتی مطرح کنند، محققان ابتدا باید یک مانع مهم را برطرف کنند: مانع ارتباطی بین زبان انسان‌ها و زبان کامپیوترها.

اثبات‌کنندگان قضیه امروز برای استفاده و سازگاری با ریاضیدانان طراحی نشده‌ بودند. ATP ها، نوع اول، معمولا برای بررسی اینکه آیا یک عبارت صحیح است یا نه، اغلب با تست کردن موارد ممکن، استفاده می‌شوند. برای مثال از یک ATP بخواهید تا تایید کند که یک فرد می‌تواند از میامی به سیاتل برود، و ممکن است تمام شهرهای مرتبط با جاده‌هایی که از میامی دور می‌شوند را جستجو کند و در نهایت شهری با جاده‌ای که به سیاتل می‌رسد را پیدا کند.

یک برنامه‌نویس با یک ATP می‌تواند تمام قوانین یا اصول را کد کند و سپس سوال کند که آیا یک حدس خاص از آن قوانین پیروی می‌کند یا خیر. سپس کامپیوتر تمام کارها را انجام می‌دهد. دانیل هوانگ، دانشمند علوم کامپیوتر که به تازگی دانشگاه کالیفرنیا، برکلی را ترک کرده تا در یک استارت‌آپ شروع به کار کند گفت: «شما فقط حدسیاتی که می‌خواهید ثابت کنید را تایپ می‌کنید، و امیدوارم که پاسخی دریافت کنید.»

اما مشکل اینجاست: کاری که ATP انجام نمی‌دهد توضیح کار آن است. تمام این محاسبات در داخل ماشین اتفاق می‌افتد، و برای چشم انسان شبیه یک رشته طولانی از ۰ و ۱ خواهد بود. هوانگ گفت که اسکن کردن اثبات و دنبال کردن استدلال غیرممکن است، چون شبیه یک توده از داده‌های تصادفی است. او گفت: «هیچ انسانی هرگز به این اثبات نگاه نمی‌کند و نمی‌تواند بگوید، من آن را می‌فهمم.»

ITP ها، دسته دوم، مجموعه داده‌های گسترده‌ای دارند که شامل ده‌ها هزار قضیه و برهان است، که می‌توانند برای تایید اینکه اثبات دقیق است آن را اسکن کنند. بر خلاف ATP ها، که در یک جعبه سیاه عمل می‌کنند و تنها یک پاسخ را به بیرون بروز می‌دهند، ITP ها نیاز به تعامل انسان و حتی راهنمایی در طول مسیر دارند، بنابراین آن‌ها به آن اندازه غیرقابل‌دسترس نیستند. هوانگ گفت: «یک انسان می‌تواند بنشیند و تکنیک‌های سطح اثبات را درک کند.» (اینها انواع اثبات‌های ماشینی هستند که Deo و Viteri مورد مطالعه قرار دادند).

ITP ها در سال‌های اخیر به طور فزاینده‌ای محبوب شده‌اند. در سال ۲۰۱۷، گروه سه تایی که در پشت مساله سه‌گانه‌های بولی فیثاغورثی قرار داشت از Coq، یک ITP، برای ایجاد و تایید یک نسخه رسمی از اثبات خود استفاده کرد؛ در سال ۲۰۰۵، ژرژ گوتیه در مایکروسافت ریسرچ کمبریج از Coq برای رسمی کردن قضیه چهار رنگ استفاده کرد. همچنین Hales از ITPs به نام HOL Light و ایزابل در اثبات رسمی حدس کپلر استفاده کردند. («HOL» مخفف «منطق مرتبه بالا» است.)

امروزه تلاش‌ها در خط مقدم این حوزه با هدف ترکیب یادگیری با استدلال انجام می‌شود. آن‌ها اغلب ATP ها را با ITP ها ترکیب می‌کنند و همچنین ابزارهای یادگیری ماشین را برای بهبود کارایی هر دو ترکیب می‌کنند. آن‌ها برنامه‌های ATP/ITP را تصور می‌کنند که می‌توانند از استدلال قیاسی استفاده کنند-و حتی ایده‌های ریاضی را منتقل کنند-همان کاری که مردم انجام می‌دهند؛ یا حداقل به روش‌های مشابه آن‌ها.

محدودیت‌های دلیل

جوزف اوربن بر این باور است که ازدواج استدلال قیاسی و استقرایی مورد نیاز برای اثبات را می توان از طریق این نوع رویکرد ترکیبی به دست آورد. گروه او اثبات‌کنندگان قضیه را با راهنمایی ابزارهای یادگیری ماشین ساخته‌است که به کامپیوترها اجازه می‌دهد خودشان از طریق تجربه یاد بگیرند. در طول چند سال گذشته، آن‌ها استفاده از شبکه‌های عصبی-لایه‌های محاسبات که به ماشین‌ها کمک می‌کنند تا اطلاعات را از طریق یک تخمین تقریبی از فعالیت نورونی مغز ما پردازش کنند- را بررسی کرده‌اند. در ماه جولای، گروه او فرضیات جدید ایجاد شده توسط شبکه عصبی آموزش‌دیده بر روی داده‌های اثبات قضیه را گزارش دادند.

اوربن تا حدودی از آندرج کارپاتی الهام‌گرفته بود، کسی که چند سال پیش یک شبکه عصبی را آموزش داد تا مزخرفاتی که به نظر ریاضی می‌آمدند را تولید کند، چیزهایی که به نظر یک فرد غیر متخصص منطقی می‌آمد. اوربن یاوه نمی‌خواست-او و گروهش در عوض ابزار خود را برای پیدا کردن دلایل جدید بعد از آموزش بر روی میلیون‌ها قضیه طراحی کردند. سپس آن‌ها از شبکه برای ایجاد حدس‌های جدید استفاده کرده و اعتبار آن حدس‌ها را با استفاده از یک ATP به نام E بررسی کردند.

این شبکه بیش از ۵۰۰۰۰ فرمول جدید پیشنهاد کرد، اگرچه ده‌ها هزار مورد تکراری بودند. اوربن گفت: «به نظر می‌رسد که ما هنوز قادر به اثبات حدس‌های جالب‌تر نیستیم.»

Szegedy در گوگل ریسرچ چالش خودکار کردن استدلال در اثبات کامپیوتری را به عنوان زیر مجموعه‌ای از یک زمینه بسیار بزرگ‌تر می‌بیند: پردازش زبان طبیعی، که شامل شناسایی الگو در استفاده از کلمات و جملات است. (شناخت الگو ایده محرک در پس دید کامپیوتری نیز هست، هدف پروژه قبلی Szegedy در گوگل). تیم او نیز مانند سایر گروه‌ها اثبات‌کنندگان قضیه‌ای را می‌خواهد که می‌تواند دلایل مفید را بیابد و توضیح دهد.

گروه Szegedy با الهام از توسعه سریع ابزارهای هوش مصنوعی مانند AlphaZero-برنامه DeepMind که می‌تواند انسان‌ها را در بازی‌هایی مثل شطرنج شکست دهد- می‌خواهند از پیشرفت‌های اخیر در تشخیص زبان برای اثبات حروف استفاده کنند. او گفت که مدل‌های زبانی می‌توانند به طرز شگفت آوری استدلال ریاضی محکم را نشان دهند.

گروه او در گوگل ریسرچ به تازگی روشی را برای استفاده از مدل‌های زبانی-که اغلب از شبکه‌های عصبی استفاده می‌کنند-برای تولید اثبات‌های جدید شرح داده‌است. پس از آموزش مدل برای تشخیص نوع ساختار شبه درختی در قضایایی که به درستی شناخته شده‌اند، آن‌ها نوعی آزمایش فرم آزاد را اجرا کردند و به سادگی از شبکه خواستند تا یک قضیه را بدون هیچ راهنمایی دیگری تولید و اثبات کند. از هزاران حدس تولید شده، حدود ۱۳٪ هم قابل‌اثبات و هم جدید بودند (به این معنی که آن‌ها قضایای دیگر در پایگاه‌داده را تکرار نکردند). او گفت که آزمایش نشان می‌دهد که شبکه عصبی می‌تواند نوعی درک از این که یک اثبات چگونه به نظر می‌رسد را به خود آموزش دهد.

Szegedy گفت: «شبکه‌های عصبی قادر به توسعه یک شیوه حدس مصنوعی هستند.»

البته، هنوز مشخص نیست که آیا این تلاش‌ها از بیش از ۴۰ سال پیش به پیشگویی کوهن منجر خواهد شد یا خیر. گورز گفته‌است که او فکر می‌کند کامپیوترها تا سال ۲۰۹۹ قادر خواهند بود ریاضی‌دانان را با منطق خود خارج کنند. او پیش‌بینی می‌کند که در ابتدا، ریاضیدانان از یک عصر طلایی لذت خواهند برد؛ »زمانی که ریاضیدانان تمام قسمت‌های جالب را انجام داده و کامپیوترها تمام قسمت‌های خسته‌کننده را انجام می‌دهند. اما به نظر من این موضوع فقط زمان کوتاهی باقی خواهد ماند.»

به هر حال، اگر ماشین‌ها به بهبود خود ادامه دهند و به مقادیر زیادی از داده‌ها دسترسی داشته باشند، باید در انجام قسمت‌های سرگرم‌کننده نیز بسیار خوب باشند. گورز گفت: «آن‌ها یاد خواهند گرفت که چگونه دستورالعمل‌های خود را انجام دهند.»

هریس موافق نیست. او فکر نمی‌کند که اثبات‌کنندگان کامپیوتری لازم هستند، یا اینکه به ناچار « ریاضیدانان انسانی را منسوخ خواهند کرد.» او می‌گوید، اگر دانشمندان علوم کامپیوتر قادر به برنامه‌ریزی نوعی شهود مصنوعی باشند، هنوز هم با آن دسته از انسان‌ها رقابت نخواهند کرد. « حتی اگر کامپیوترها درک کنند، به روش انسانی درک نمی‌کنند.»

این متن با استفاده از ربات ترجمه مقاله علمی ترجمه شده و به صورت محدود مورد بازبینی انسانی قرار گرفته است.در نتیجه می‌تواند دارای برخی اشکالات ترجمه باشد.