چندین سال قبل از اینکه ChatGPT شروع به پخش مطالب بیهوده کند، گوگل نوع بسیار متفاوتی از برنامه هوش مصنوعی به نام AlphaGo را توسعه داده بود که با تمرین خستگی ناپذیر بازی رومیزی Go را با مهارتی فوق بشری یاد گرفت.
محققان این شرکت به تازگی مطالعهای منتشر کردهاند که قابلیتهای یک مدل زبان بزرگ (هوش مصنوعی در پشت رباتهای چت امروزی) را با قابلیتهای AlphaZero، جانشین AlphaGo که قادر به بازی در شطرنج است، ترکیب میکند تا اثباتهای ریاضی بسیار ظریف را حل کند.
خلاقیت جدید فرانکشتاینی آنها به نام AlphaProof، توانایی خود را با مقابله با چندین مشکل از المپیاد بینالمللی ریاضیات (IMO) 2024 نشان داد، رقابتی معتبر برای دانشآموزان دبیرستانی.
AlphaProof از مدل زبان Gemini برای تبدیل سوالات ریاضی با فرمول طبیعی به زبان برنامه نویسی به نام Lean استفاده می کند. این ماده آموزشی را برای الگوریتم دوم فراهم میکند که از طریق آزمون و خطا، نحوه یافتن شواهدی را که میتوان صحت آن را تأیید کرد، یاد میگیرد.
اوایل سال جاری، Google DeepMind از الگوریتم ریاضی دیگری به نام AlphaGeometry رونمایی کرد که همچنین یک مدل زبان را با رویکرد هوش مصنوعی متفاوت ترکیب میکند. AlphaGeometry از Gemini برای تبدیل مسائل هندسی به قالبی استفاده می کند که می تواند توسط برنامه ای که عناصر هندسی را کنترل می کند، دستکاری و آزمایش کند. گوگل همچنین امروز نسخه جدید و بهبود یافته AlphaGeometry را معرفی کرد.
محققان دریافتند که دو برنامه ریاضی آنها می تواند برای پازل های IMO و همچنین یک مدال نقره اثبات کند. از مجموع شش مسئله، AlphaProof دو مسئله جبر و یک مسئله تئوری اعداد را حل کرد، در حالی که AlphaGeometry یک مسئله هندسه را حل کرد. این برنامه ها یک مشکل را در عرض چند دقیقه برطرف کردند، اما چندین روز طول کشید تا برخی دیگر حل شوند. Google DeepMind میزان قدرت محاسباتی خود را برای حل این مشکلات نشان نداده است.
Google DeepMind رویکرد مورد استفاده برای AlphaProof و AlphaGeometry را “عصب نمادین” می نامد زیرا آنها یادگیری ماشینی خالص یک شبکه عصبی مصنوعی، فناوری که زیربنای جدیدترین پیشرفت های هوش مصنوعی است، با زبان برنامه نویسی معمولی ترکیب می کنند.
دیوید سیلور، محقق گوگل، که رهبری کار روی AlphaZero را بر عهده داشت، میگوید: «ما در اینجا دریافتیم که میتوان رویکردی را که بسیار موفق بوده و ابزارهایی مانند AlphaGo را با مدلهای زبان بزرگ ترکیب کرد و چیزی بسیار قدرتمند تولید کرد. سیلور میگوید که تکنیکهای نشاندادهشده با AlphaProof، در تئوری، باید به سایر حوزههای ریاضیات نیز گسترش یابد.
در واقع، این تحقیق چشمانداز مقابله با بدترین گرایشهای مدلهای اصلی زبانشناختی را با استفاده از منطق و استدلال به شیوهای پایهتر باز میکند. به همان اندازه که مدلهای زبانی عالی میتوانند معجزهآسا باشند، اغلب برای درک ریاضیات پایه یا حل مسائل منطقی تلاش میکنند.
در آینده، روش عصبی نمادین میتواند به سیستمهای هوش مصنوعی اجازه دهد تا سؤالات یا وظایف را به قالبی تبدیل کنند که بتوان در مورد آن به روشی استدلال کرد که نتایج قابل اعتمادی تولید کند. OpenAI نیز بر روی چنین سیستمی با نام رمز “Strawberry” کار خواهد کرد.
با این حال، سیستمهایی که امروز معرفی شدند، همانطور که سیلور اذعان میکند، یک محدودیت کلیدی دارند. راهحلهای ریاضی یا درست یا نادرست هستند و به AlphaProof و AlphaGeometry اجازه میدهند پاسخ صحیح را پیدا کنند. بسیاری از مشکلات دنیای واقعی (به عنوان مثال، یافتن مسیر ایده آل برای سفر) راه حل های ممکن زیادی دارند و تشخیص اینکه کدام یک ایده آل است می تواند دشوار باشد. سیلور میگوید راهحل سؤالات مبهمتر ممکن است این باشد که یک مدل زبانشناختی تلاش کند تا تعیین کند که چه چیزی یک پاسخ «خوب» در طول آموزش است. او میگوید: طیف وسیعی از راهحلهای مختلف وجود دارد که میتوان آنها را امتحان کرد.
سیلور همچنین مراقب است که تأکید کند Google DeepMind قرار نیست ریاضیدانان را بیکار کند. او می گوید: “هدف ما ارائه سیستمی است که بتواند هر چیزی را ثابت کند، اما این پایان کار ریاضیدانان نیست.” بسیاری از ریاضیات در مورد طرح مسائل و یافتن سؤالات جالب برای پرسیدن است. این می تواند ابزار دیگری در نظر گرفته شود، درست مانند یک قانون اسلاید، ماشین حساب یا ابزار محاسبه. »
به روز شده در 24/07/25 در ساعت 13:25 به وقت شرقی: این داستان بهروزرسانی شده است تا مشخص شود که AlphaProof و AlphaGeometry چه تعداد از مشکلات را برطرف کردهاند.
منبع: https://www.wired.com/story/google-deepmind-alphaproof-ai-math/