AlphaProof Nexus با داوری علمی ۹ مسئله باز اردوش را حل کرد

هوش مصنوعی ریاضی گوگل دیپ‌مایند، طبق پژوهشی منتشرشده در نشریه Science، ۹ مسئله باز اردوش را حل کرده است؛ دو مورد از این مسائل ۵۶ سال بی‌پاسخ مانده بودند. این دستاورد بخشی از مجموعه‌ای گسترده‌تر از نتایج AlphaProof Nexus است که علاوه بر مسائل اردوش، اثبات حدس‌های ریاضی و حل یک پرسش در هندسه جبری را نیز شامل می‌شود. انتشار پژوهش پس از داوری علمی، در میانه بحث بر سر نحوه ارزیابی و انتشار اثبات‌های تولیدشده با هوش مصنوعی اهمیت دارد.

AlphaProof Nexus و مسائل باز اردوش

به گزارش The Decoder، پژوهش جدید عملکرد AlphaProof Nexus را در مجموعه‌ای شامل ۳۵۳ مسئله باز اردوش بررسی می‌کند. این مسائل به مسائل ریاضیِ حل‌نشده‌ای گفته می‌شود که در مجموعه مسائل منسوب به ریاضی‌دان پال اردوش ثبت شده‌اند. سامانه توانست ۹ مورد از آن‌ها را حل کند؛ دو مسئله‌ای که بنا بر گزارش، ۵۶ سال بدون راه‌حل باقی مانده بودند.

گروه گوگل دیپ‌مایند راه‌حل‌های این ۹ مسئله را پیش از انتشار مقاله، به‌صورت آنلاین به اشتراک گذاشت. متن منبع می‌گوید AlphaProof Nexus این مسائل را حتی بدون استفاده از ابزار تخصصی AlphaProof نیز حل کرده است؛ نکته‌ای که به گفته گوگل دیپ‌مایند، نشان می‌دهد توانایی حل آن‌ها صرفاً به فراخوانی آن ابزار وابسته نبوده است.

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

مدل Gemini و زبان صوری Lean

AlphaProof Nexus بر پایه Gemini 3.1 Pro ساخته شده است. این مدل پیش‌نویس اثبات‌های ریاضی را تولید و بازبینی می‌کند و برای بیان آن‌ها از Lean، زبانی صوری برای نوشتن اثبات‌ها، استفاده می‌کند. در اثبات صوری، استدلال به شکلی دقیق و قابل بررسی نوشته می‌شود تا سامانه بتواند اعتبار گام‌های آن را کنترل کند.

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

برای زیرمسئله‌های دشوارتر، AlphaProof Nexus می‌تواند از AlphaProof، ابزار تخصصی اثبات، کمک بگیرد. با این حال، گوگل دیپ‌مایند گزارش کرده که حل ۹ مسئله اردوش بدون AlphaProof نیز انجام شده است. بنابراین نقش AlphaProof در این سامانه، پشتیبانی از برخی بخش‌های دشوارتر است، نه پیش‌شرط همه راه‌حل‌های گزارش‌شده.

داوری علمی در میانه اختلاف بر سر اثبات‌های AI

انتشار این پژوهش در فضایی انجام شده که درباره کیفیت و شیوه عرضه اثبات‌های تولیدشده به کمک هوش مصنوعی اختلاف‌نظر وجود دارد. طبق گزارش، OpenAI اخیراً صدها اثبات هوش مصنوعی را به‌جای ارسال به نشریه‌های علمی، در GitHub منتشر کرده است. انجمن Association for Human Mathematics، به رهبری ترنس تائو، در واکنش خواستار تحریم شده است.

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

نتایج اعلام‌شده دامنه‌ای از ریاضیات را دربرمی‌گیرد: مسئله‌های باز اردوش، حدس‌های ثبت‌شده در OEIS، هندسه جبری و بهینه‌سازی مین‌مکس. بهبود یک کران در بهینه‌سازی مین‌مکس نیز از این جهت قابل توجه است که این روش در آموزش برخی مدل‌های هوش مصنوعی به کار می‌رود. با این حال، منبع درباره کاربرد مستقیم این نتیجه در آموزش مدل‌ها یا میزان اثر عملی آن توضیح بیشتری نمی‌دهد.

این خبر برای چه کسانی اهمیت دارد

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

برای شرکت‌های فعال در هوش مصنوعی نیز نتایج AlphaProof Nexus رقابت را به حوزه‌ای فراتر از پاسخ‌گویی عمومی مدل‌ها می‌کشاند: حل مسائل تخصصی و عرضه نتایج در قالب پژوهشی که داوری علمی شده است. در بحث جاری، کار گوگل دیپ‌مایند نشان می‌دهد که اعتبارسنجی و مسیر انتشار می‌توانند بخشی از ارزیابی دستاوردهای ریاضی هوش مصنوعی باشند، نه صرفاً شمار پاسخ‌های منتشرشده.