DeepMind اعلام کرد هوش مصنوعی جدیدش، AlphaProof Nexus، برای مجموعه‌ای از پرسش‌های ریاضی که پیش‌تر حل‌نشده بودند، اثبات‌های صوری ارائه کرده است. نتایج این پژوهش در مقاله‌ای داوری‌شده در مجلهٔ Science منتشر شده‌اند. این سامانه از Gemini 3.1 Pro برای نوشتن اثبات‌ها به زبان صوری Lean استفاده می‌کند و هر گام را به‌طور خودکار بررسی می‌کند.
AlphaProof Nexus به چه دستاوردهایی رسید؟
این مقاله گزارش می‌دهد که AlphaProof Nexus از میان ۳۵۳ مسئلهٔ اردوش که همچنان حل‌نشده فهرست شده‌اند، ۹ مسئله را حل کرده است؛ از جمله دو مسئله که ۵۶ سال بی‌پاسخ مانده بودند. این سامانه همچنین ۴۴ حدس را از پایگاه دادهٔ دنباله‌های صحیح OEIS اثبات کرد، به پرسشی حل‌نشده در هندسهٔ جبری پاسخ داد و کران شناخته‌شده‌ای را در بهینه‌سازی مین‌مکس ــ روشی که در آموزش برخی مدل‌های هوش مصنوعی به کار می‌رود ــ بهبود داد.
این سامانه چگونه کار می‌کند؟
AlphaProof Nexus بر پایهٔ Gemini 3.1 Pro ساخته شده است؛ این مدل پیش‌نویس اثبات‌ها را به زبان Lean می‌نویسد و بلافاصله از راستی‌آزمای Lean بازخورد می‌گیرد. اگر پیش‌نویس درست نباشد، Lean پیام خطایی می‌دهد که مسیر تلاش بعدی را مشخص می‌کند. برای زیرمسئله‌های دشوارتر، سامانه می‌تواند از ابزار تخصصی‌ای به نام AlphaProof کمک بگیرد. گروه پژوهشی ۹ راه‌حل مسائل اردوش را پیش از انتشار مقاله به‌صورت آنلاین منتشر کرد.
چرا مهم است
برای ریاضی‌دانان، این هوش مصنوعی راه تازه‌ای برای بررسی مسائل دشوار و راستی‌آزمایی خودکار اثبات‌ها فراهم می‌کند و می‌تواند روند پژوهش را سرعت ببخشد. برای کاربران ابزارهای هوش مصنوعی، بهبود در بهینه‌سازی مین‌مکس ممکن است به آموزش کارآمدتر مدل‌های آینده منجر شود. انتشار مقاله پس از داوری نشان می‌دهد جامعهٔ علمی اثبات‌های تولیدشده با هوش مصنوعی را جدی می‌گیرد، هرچند هنوز به اعتبارسنجی گسترده‌تری نیاز است.
