پژوهش AlphaProof Nexus در Science؛ اثبات ریاضی با Gemini و Lean

از پیش‌نویس مدل تا اثبات قابل‌بررسی

طبق اطلاعیه AAAS، پژوهش AlphaProof Nexus در ۸ اکتبر ۲۰۲۶ در مجله Science منتشر شد. این چارچوب از عامل‌های هوش مصنوعی و بازخورد ابزار اثبات رسمی Lean برای جست‌وجوی اثبات‌های ریاضی استفاده می‌کند؛ انتشار مقاله به معنای عرضه مدل یا API عمومی نیست. پیش‌چاپ پژوهش نخستین‌بار در ۲۱ مه ۲۰۲۶ منتشر شده بود.

در سازوکار توصیف‌شده، Gemini 3.1 Pro پیش‌نویس اثبات را تولید و اصلاح می‌کند و پیام‌های خطای Lean برای تلاش بعدی به مدل بازگردانده می‌شوند. معماری کامل از جست‌وجوی تکاملی و Gemini 3.0 Flash برای رتبه‌بندی پیش‌نویس‌ها نیز بهره می‌گیرد. تفاوت با یک پاسخ زبانی این است که اثبات رسمی باید بررسی مکانیکی Lean را بگذراند، نه اینکه فقط قانع‌کننده به نظر برسد.

به گزارش نویسندگان، سامانه ۹ مسئله از ۳۵۳ مسئله اردوش آزموده‌شده، حدود ۲٫۵ درصد، و ۴۴ حدس از ۴۹۲ حدس باز پایگاه OEIS، حدود ۸٫۹ درصد، را حل کرده است. آزمایش اردوش سقف ۳۰۰۰ دوره جست‌وجو برای هر مسئله داشت. عامل ساده‌تر نیز همان ۹ مسئله را حل کرد؛ بنابراین این نتیجه به‌تنهایی برتری معماری پیچیده‌تر را نشان نمی‌دهد.

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