📌 سیستم LEAP: سیستمی که به مدل زبانی کمک کرد تمام مسائل المپیاد پاتنم ۲۰۲۵ را حل کند
گوگل مقاله‌ای دربارهٔ سیستم LEAP منتشر کرده است که برای اثبات خودکار قضایا طراحی شده. این سیستم به مدل‌های زبانی امکان می‌دهد تا اثبات‌های رسمی و قابل راستی‌آزمایی ماشین را به زبان Lean بسازند.
اثبات به زبان طبیعی (انسان) به سختی به صورت خودکار قابل بررسی است، زیرا تقریباً همیشه شامل خلأهای منطقی می‌شود. اما اثبات رسمی (فرمال) با زبان ماشین نوشته می‌شود و توسط کامپایلر بررسی می‌گردد که تضمین‌کنندهٔ درستی است، هرچند نوشتن آن بسیار دشوارتر است.
در این حوزه، مدل‌های تخصصی که صرفاً برای Lean آموزش دیده‌اند، پیشتاز هستند. اما LEAP که به عنوان یک چارچوب عاملی (agentic framework) کار می‌کند، از مدل‌های عمومی استفاده می‌نماید: مسئله را به بخش‌های کوچک تقسیم کرده و بر اساس خطاهای بازگردانده شده توسط کامپایلر، به صورت بازگشتی اشکالات را رفع می‌کند.
دستاورد اصلی پژوهشی این پروژه، المپیاد پاتنم ۲۰۲۵ است؛ مسابقه سالانه ریاضی برای دانشجویان آمریکا. LEAP موفق شد هر ۱۲ مسئله این المپیاد را به صورت رسمی حل کند، در حالی که Gemini 3.1 Pro به تنهایی و همچنین سیستم تخصصی متن‌باز Goedel-Prover-V2 حتی یک مسئله را حل نکردند. سیستم بسته Aristotle که در المپیاد ریاضی IMO ۲۰۲۵ عملکردی در سطح مدال طلا داشت، در ارزیابی نویسندگان این مقاله ۹ مسئله از ۱۲ را حل کرده است.
در این مقاله مجموعه داده جدیدی به نام IMO-LeanProofBench شامل ۶۰ مسئله المپیادی معرفی شده که در زبان Lean فرمال شده‌اند و نیازمند استنتاج‌های غیرمعمول و اثبات‌های ساختاری پیچیده هستند. در این مجموعه، LEAP به طور میانگین در بخش‌های پایه و پیشرفته به حدود ۷۰٪ موفقیت می‌رسد، در حالی که Aristotle حدود ۴۸٪ است.
دستاورد جانبی: LEAP بخش کمکی یکی از مسائل ترکیبیاتی منتسب به ریاضیدان دونالد کانت را به طور رسمی تأیید کرده و بیش از ۵۰۰۰ خط کد در Lean 4 تولید نموده است.
🟡 نکتهٔ طعنه‌آمیز
نویسندگان مقاله در متن خود از سیستم‌های بسته رقیب (Axiom3, Numina, Aristotle) به دلیل در دسترس نبودن برای بررسی علمی انتقاد کرده‌اند. با این حال، کد خود LEAP نیز منتشر نشده است. انتشار اثبات‌های نهایی تا حدی این مشکل را کاهش می‌دهد (چون می‌توان آنها را با کامپایلر Lean بازبینی کرد)، اما بازتولید کامل این پروژهٔ گوگل در حال حاضر ممکن نیست.
منبع: Google Research – LEAP
#AI #ML #LLM #LEAP #Research #Google
🆔 @asrgooyeshpardaz
گوگل مقاله‌ای دربارهٔ سیستم LEAP منتشر کرده است که برای اثبات خودکار قضایا طراحی شده. این سیستم به مدل‌های زبانی امکان می‌دهد تا اثبات‌های رسمی و قابل راستی‌آزمایی ماشین را به زبان Lean بسازند.
اثبات به زبان طبیعی (انسان) به سختی به صورت خودکار قابل بررسی است، زیرا تقریباً همیشه شامل خلأهای منطقی می‌شود. اما اثبات رسمی (فرمال) با زبان ماشین نوشته می‌شود و توسط کامپایلر بررسی می‌گردد که تضمین‌کنندهٔ درستی است، هرچند نوشتن آن بسیار دشوارتر است.
در این حوزه، مدل‌های تخصصی که صرفاً برای Lean آموزش دیده‌اند، پیشتاز هستند. اما LEAP که به عنوان یک چارچوب عاملی (agentic framework) کار می‌کند، از مدل‌های عمومی استفاده می‌نماید: مسئله را به بخش‌های کوچک تقسیم کرده و بر اساس خطاهای بازگردانده شده توسط کامپایلر، به صورت بازگشتی اشکالات را رفع می‌کند.
دستاورد اصلی پژوهشی این پروژه، المپیاد پاتنم ۲۰۲۵ است؛ مسابقه سالانه ریاضی برای دانشجویان آمریکا. LEAP موفق شد هر ۱۲ مسئله این المپیاد را به صورت رسمی حل کند، در حالی که Gemini 3.1 Pro به تنهایی و همچنین سیستم تخصصی متن‌باز Goedel-Prover-V2 حتی یک مسئله را حل نکردند. سیستم بسته Aristotle که در المپیاد ریاضی IMO ۲۰۲۵ عملکردی در سطح مدال طلا داشت، در ارزیابی نویسندگان این مقاله ۹ مسئله از ۱۲ را حل کرده است.
در این مقاله مجموعه داده جدیدی به نام IMO-LeanProofBench شامل ۶۰ مسئله المپیادی معرفی شده که در زبان Lean فرمال شده‌اند و نیازمند استنتاج‌های غیرمعمول و اثبات‌های ساختاری پیچیده هستند. در این مجموعه، LEAP به طور میانگین در بخش‌های پایه و پیشرفته به حدود ۷۰٪ موفقیت می‌رسد، در حالی که Aristotle حدود ۴۸٪ است.
دستاورد جانبی: LEAP بخش کمکی یکی از مسائل ترکیبیاتی منتسب به ریاضیدان دونالد کانت را به طور رسمی تأیید کرده و بیش از ۵۰۰۰ خط کد در Lean 4 تولید نموده است.
🟡 نکتهٔ طعنه‌آمیز
نویسندگان مقاله در متن خود از سیستم‌های بسته رقیب (Axiom3, Numina, Aristotle) به دلیل در دسترس نبودن برای بررسی علمی انتقاد کرده‌اند. با این حال، کد خود LEAP نیز منتشر نشده است. انتشار اثبات‌های نهایی تا حدی این مشکل را کاهش می‌دهد (چون می‌توان آنها را با کامپایلر Lean بازبینی کرد)، اما بازتولید کامل این پروژهٔ گوگل در حال حاضر ممکن نیست.
منبع: Google Research – LEAP
#AI #ML #LLM #LEAP #Research #Google
🆔 @asrgooyeshpardaz
❤1👎1👏1