LLMها با گسترش قابلیت‌هایشان از طریق زبان طبیعی، پیشرفت‌های قابل توجهی در استدلال ریاضیاتی از خود نشان داده‌اند که منجر به بهبود عملکرد در بنچمارک‌هایی مانند MATH و AIME شده است. با این حال، یادگیری تقویتی (RL) برای آموزش این مدل‌ها با یک چالش اساسی روبرو است: تأیید صحت اثبات‌های به زبان طبیعی بسیار دشوار است و نیاز به بررسی دقیق و دستی هر مرحله استدلال دارد. این محدودیت، کاربرد RL را برای آموزش مدل‌های اثبات قضیه ریاضیاتی محدود می‌کند. در حالی که زبان‌های رسمی مانند Lean امکان تأیید خودکار صحت را فراهم می‌کنند، اثبات‌کننده‌های رسمی LLM کنونی با محدودیت‌های خود مواجه هستند. اثبات‌کننده‌های سطح گام به گام، کد را به صورت افزایشی تولید می‌کنند اما نیاز به بستر ویژه‌ای دارند و فاقد قابلیت‌های استدلال سطح بالا هستند.

معرفی Seed-Prover: گامی نوین در اثبات قضایای ریاضی

تیم Seed ByteDance سیستم Seed-Prover را معرفی کرده است، یک مدل استدلال کامل اثباتی به سبک لم (lemma-style whole-proof reasoning model). این سیستم با استفاده از بازخورد Lean، لم‌های از پیش اثبات شده و خودخلاصه‌سازی، اثبات‌ها را به صورت تکراری اصلاح می‌کند. Seed-Prover از سه استراتژی استنتاج تخصصی در زمان آزمایش بهره می‌برد که امکان روش‌های استدلال عمیق و گسترده را برای حل مسائل در سطح مسابقات IMO فراهم می‌سازد. نوآوری اصلی آن در اتخاذ روش اثبات بر مبنای لم به عنوان هسته اصلی رویکردش است که به جای تکیه بر روش‌های سنتی تولید اثبات گام به گام یا کامل، لم‌ها را در مرکز فرآیند استدلال قرار می‌دهد.

علاوه بر این، این مقاله Seed-Geometry را معرفی می‌کند، یک موتور استدلال هندسی مکمل که محدودیت‌های Lean را در مدیریت پشتیبانی هندسی برطرف می‌سازد. Seed-Geometry قادر است با ارائه ابزارهای لازم برای تعامل موثر با مسائل هندسی، شکاف مهمی را در قابلیت‌های سیستم‌های اثبات قضیه پر کند. این امر به Seed-Prover اجازه می‌دهد تا نه تنها در حوزه‌های سنتی ریاضیات بلکه در مسائل پیچیده هندسی نیز برتری یابد.

توسعه Seed-Prover نشان‌دهنده یک پیشرفت چشمگیر در زمینه اثبات قضیه خودکار است. در گذشته، سیستم‌های خودکار اثبات قضیه عمدتاً بر منطق صوری و الگوریتم‌های جستجو تکیه داشتند که اغلب برای مسائل پیچیده و در دنیای واقعی کارایی کافی نداشتند. Seed-Prover با تلفیق قدرت مدل‌های زبان بزرگ با سخت‌گیری زبان‌های رسمی، راه را برای اثبات‌های ریاضیاتی قابل اعتمادتر و کارآمدتر هموار می‌کند.

این رویکرد ترکیبی، Seed-Prover را قادر می‌سازد تا به صورت هوشمندانه، نه تنها راه‌حل‌های صحیح را کشف کند بلکه فرآیند استدلال را نیز به گونه‌ای منطقی و قابل پیگیری سازماندهی نماید. این قابلیت، به خصوص در مواجهه با چالش‌های دشوار ریاضیاتی که نیازمند چندین مرحله استدلال میانی هستند، حیاتی است. این مدل، قادر به شناسایی و استفاده از لم‌های میانی است که می‌تواند به طور قابل توجهی پیچیدگی اثبات‌های طولانی را کاهش دهد و کارایی سیستم را در رسیدن به نتیجه نهایی افزایش دهد.

چالش‌های فعلی در استدلال ریاضیاتی LLMها

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

این مشکل به خصوص در کاربردهای حساس مانند توسعه نرم‌افزار، طراحی سخت‌افزار یا سیستم‌های امنیتی که نیاز به اثبات‌های کاملاً دقیق و بی‌عیب دارند، اهمیت پیدا می‌کند. عدم قابلیت اتکاء به صحت اثبات‌های تولید شده توسط LLMها به زبان طبیعی، مانع از پذیرش گسترده آن‌ها در این حوزه‌ها می‌شود و نیاز به مکانیزم‌های تأیید رسمی را بیش از پیش ضروری می‌سازد.

در مقابل، زبان‌های رسمی مانند Lean به دلیل ساختار منطقی و قواعد صریح خود، امکان تأیید خودکار صحت اثبات‌ها را فراهم می‌کنند. هر گام در یک اثبات رسمی باید دقیقاً از قواعد منطق پیروی کند و هرگونه خطا بلافاصله توسط سیستم شناسایی می‌شود. با این حال، تولید اثبات در زبان‌های رسمی برای LLMها دشوار است. اثبات‌کننده‌های رسمی فعلی LLM، عمدتاً بر رویکرد “گام به گام” متمرکز هستند که در آن مدل، کد Lean را به صورت افزایشی تولید می‌کند. این رویکرد اگرچه کنترل بیشتری بر فرآیند اثبات می‌دهد، اما اغلب نیازمند “بسترهای” خاص (scaffolding) و راهنمایی‌های دستی است و فاقد قابلیت‌های استدلال سطح بالا برای حل مسائل پیچیده است.

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

نوآوری‌های کلیدی Seed-Prover و Seed-Geometry

Seed-Prover از یک رویکرد اثبات به سبک لم بهره می‌برد که آن را از سایر روش‌ها متمایز می‌کند. به جای تلاش برای تولید کل اثبات به صورت یکجا یا گام به گام، Seed-Prover بر شناسایی و اثبات لم‌های (قضیه‌های کوچک کمکی) میانی تمرکز می‌کند. این لم‌ها سپس به عنوان بلوک‌های سازنده برای اثبات قضیه اصلی مورد استفاده قرار می‌گیرند. این رویکرد به سیستم اجازه می‌دهد تا مشکلات پیچیده را به بخش‌های کوچکتر و قابل مدیریت‌تر تقسیم کند، که فرآیند استدلال را کارآمدتر و قابل پیگیری‌تر می‌سازد.

یکی از قابلیت‌های منحصر به فرد Seed-Prover، توانایی آن در “خودخلاصه‌سازی” است. این به مدل اجازه می‌دهد تا خلاصه‌ای از اثبات‌های موجود و لم‌های کشف شده را درک کرده و از آن برای هدایت استدلال‌های بعدی استفاده کند. این مکانیسم یادگیری و سازگاری داخلی، کارایی مدل را در مواجهه با مسائل جدید و پیچیده به طرز چشمگیری افزایش می‌دهد. با بازخورد مداوم از Lean، Seed-Prover قادر است اشتباهات خود را شناسایی و تصحیح کند و اثبات‌ها را به صورت تکراری و متوالی اصلاح کند.

علاوه بر Seed-Prover، تیم ByteDance Seed سیستم Seed-Geometry را معرفی کرده است. Lean، علیرغم قابلیت‌های قدرتمند خود در اثبات قضیه رسمی، در مواجهه با مسائل هندسی دارای محدودیت‌هایی است. Seed-Geometry به طور خاص برای پر کردن این شکاف طراحی شده است و پشتیبانی کامل برای استدلال هندسی را فراهم می‌آورد. این سیستم، به عنوان یک موتور استدلال هندسی مکمل، به Seed-Prover امکان حل مسائلی را می‌دهد که در حالت عادی برای Lean چالش‌برانگیز هستند، به خصوص در حوزه‌هایی که به درک فضایی و استدلال بصری نیاز دارند.

Seed-Geometry به Seed-Prover اجازه می‌دهد تا با اطمینان بیشتری به مسائل هندسی نزدیک شود. این همکاری بین دو سیستم، مجموعه‌ای قدرتمند را برای رسیدگی به طیف وسیعی از مسائل ریاضیاتی، از جبر و نظریه اعداد گرفته تا ترکیبات و هندسه، ایجاد می‌کند. این ترکیب نه تنها دقت اثبات‌ها را بالا می‌برد بلکه سرعت و کارایی فرآیند اثبات قضیه خودکار را نیز بهینه می‌کند، که یک گام بزرگ رو به جلو در هوش مصنوعی استدلال‌گر به حساب می‌آید.

روش‌های آموزش و تعامل با Lean

تعامل کارآمد بین Seed-Prover و Lean، سنگ بنای موفقیت این سیستم است. برای دستیابی به این هدف، از یک رویکرد یادگیری تقویتی چندمرحله‌ای و چندوظیفه‌ای مبتنی بر VAPO (Value-Augmented Policy Optimization) استفاده شده است. VAPO به مدل اجازه می‌دهد تا نه تنها اقدامات مناسب را (تولید گام‌های اثبات) یاد بگیرد، بلکه ارزش احتمالی هر مسیر اثبات را نیز تخمین بزند که به هدایت جستجو به سمت راه‌حل‌های موفق کمک می‌کند.

مجموعه داده آموزشی از ترکیب داده‌های متن‌باز موجود و مسائل رسمی تولید شده در داخل شرکت استفاده می‌کند. یک جزء کلیدی این فرآیند، استفاده از یک “پیشنهاد دهنده” (proposer) است که برای مسائل دشوار، نسخه‌های ساده‌تر و قابل حل‌تری را تولید می‌کند. این کار به مدل کمک می‌کند تا به تدریج مهارت‌های خود را روی مسائل پیچیده‌تر توسعه دهد. برای جلوگیری از آموزش روی مسائل بسیار ساده، مشکلاتی که نرخ اثبات بیش از ۲۵ درصد دارند، از مجموعه داده حذف می‌شوند. این فیلتراسیون تضمین می‌کند که مدل بر یادگیری استدلال‌های چالش‌برانگیزتر تمرکز کند.

پشتیبانی Seed-Geometry در بخش باطن، امکان تولید مسائل در مقیاس بزرگ را فراهم می‌کند. این بخش قادر است بیش از ۲۳۰ میلیون مسئله منحصر به فرد را در طول هفت روز شناسایی کند که نشان‌دهنده بهبود هشت برابری در کارایی جستجو است. این قابلیت تولید انبوه داده، برای آموزش مدل‌های یادگیری تقویتی بسیار حیاتی است، زیرا نیاز به حجم زیادی از داده‌های متنوع و چالش‌برانگیز دارند تا بتوانند به تعمیم‌پذیری و عملکرد مطلوب دست یابند.

اگرچه یک مدل سیاست (policy model) و یک مدل ارزش (value model) جداگانه آموزش داده شده‌اند، آزمایشات گسترده نشان می‌دهد که مدل‌های ارزش ممکن است به دلیل خطاهای تخمین، عملکرد کلی را کاهش دهند. در نتیجه، برای تنظیمات توزیع شده (distributed setups)، از تولید گام به گام با جستجوی بیم (beam search) استفاده می‌شود. این انتخاب نشان‌دهنده یک توازن عملی بین دقت و کارایی است، به طوری که جستجوی بیم به کاوش چندین مسیر ممکن اثبات به صورت موازی کمک می‌کند و شانس یافتن راه‌حل‌های معتبر را افزایش می‌دهد، در حالی که از پیچیدگی‌های مرتبط با مدل‌های ارزش پرهیز می‌شود.

عملکرد بی‌نظیر در بنچمارک‌های ریاضیاتی

Seed-Prover در چندین بنچمارک ریاضیاتی به نتایج بی‌نظیری دست یافته است. برای مسابقه IMO 2025، Seed-Prover موفق به حل کامل ۵ از ۶ مسئله شده است که یک دستاورد چشمگیر محسوب می‌شود. Seed-Geometry فوراً مسئله ۲ را حل کرد و Seed-Prover اثبات مسائل باقیمانده را با استفاده از تنظیمات مختلف استنتاج انجام داد. این نشان‌دهنده نه تنها قدرت Seed-Prover در استدلال خالص، بلکه قابلیت همکاری بی‌نظیر آن با Seed-Geometry در مواجهه با مسائل پیچیده هندسی است.

در مسائل گذشته IMO، Seed-Prover توانست ۱۲۱ از ۱۵۵ مسئله را ثابت کند که نرخ موفقیت ۷۸.۱ درصدی را در تمامی سطوح دشواری به ثبت رسانده است. تجزیه و تحلیل عملکرد نشان‌دهنده نتایج قوی در دسته‌بندی‌های مختلف مسائل است: ۴۷ از ۵۵ مسئله آسان، ۴۷ از ۵۶ مسئله متوسط و ۲۷ از ۴۴ مسئله دشوار حل شده‌اند. نرخ موفقیت در موضوعات خاص شامل ۷۲ از ۸۵ در جبر، ۴۲ از ۵۵ در نظریه اعداد و ۷ از ۱۴ در ترکیبیات است. این آمارها نشان‌دهنده تعمیم‌پذیری بالا و استحکام Seed-Prover در حوزه‌های مختلف ریاضیات است.

در بنچمارک MiniF2F، محققان به نرخ اثبات ۹۹.۶ درصد برای هر دو مجموعه اعتبارسنجی و تست در تنظیمات متوسط دست یافتند که شامل حل مسائل دشواری مانند IMO 1990 P3 می‌شود. این نتیجه نشان می‌دهد که Seed-Prover نه تنها قادر به حل مسائل دشوار است، بلکه دقت بسیار بالایی را در اثبات‌ها حفظ می‌کند. نتایج PutnamBench نیز بهبود قابل توجهی را نشان می‌دهد؛ از ۲۰۱ مسئله حل شده به ۳۳۱ مسئله از ۶۵۷ مسئله با ارتقا از تنظیمات استنتاج “سبک” به “متوسط”. این جهش عملکردی قابل توجهی نسبت به سیستم‌های استدلال ریاضیاتی سطح کارشناسی قبلی را نشان می‌دهد.

در بنچمارک CombiBench، Seed-Prover ۳۰ از ۱۰۰ مسئله ترکیبیات را حل کرده است. این عملکرد اگرچه از روش‌های موجود بهتر است، اما چالش‌های مداوم در استدلال ترکیبیاتی را نیز آشکار می‌کند که نشان می‌دهد هنوز جای پیشرفت در این زمینه وجود دارد. علاوه بر این، محققان به موفقیت ۸۱.۸ درصدی در MiniCTX-v2 دست یافتند که تعمیم‌پذیری قوی Seed-Prover را فراتر از مسائل رقابتی نشان می‌دهد و عملکرد o4-mini baseline را که در Pass@8 به ۴۴.۳ درصد رسیده بود، به طرز چشمگیری پشت سر می‌گذارد.

آینده اثبات قضایای خودکار

معرفی Seed-Geometry و Seed-Prover توسط تیم Seed ByteDance، گامی عظیم در ادغام قابلیت‌های مدل‌های زبان بزرگ (LLMs) با روش‌های استدلال رسمی محسوب می‌شود. Seed-Geometry با ارائه قابلیت تأیید سریع و مکانیسم‌های جستجوی پیشرفته، به ویژه در حوزه هندسه، به Seed-Prover کمک می‌کند. در همین حال، Seed-Prover از اصلاح تکراری و استراتژی‌های استنتاج پیچیده در زمان آزمایش بهره می‌برد تا به نتایج بی‌سابقه‌ای در اثبات قضایا دست یابد.

دستاورد حل ۵ از ۶ مسئله در IMO 2025 به وضوح اثربخشی عملی این روش‌ها را در رویارویی با رقابت‌های ریاضیاتی سطح بالا نشان می‌دهد. این موفقیت نه تنها اعتبار Seed-Prover را به عنوان یک سیستم پیشرو در هوش مصنوعی اثبات قضیه تأیید می‌کند، بلکه پتانسیل بالای این فناوری را برای کمک به پیشرفت دانش ریاضی نشان می‌دهد.

استفاده از زبان‌های رسمی مانند Lean، تأیید سریع و خودکار اثبات‌ها را ممکن می‌سازد که هم از نظر هزینه مقرون به صرفه‌تر از کارشناسان انسانی است و هم از LLM‌های مبتنی بر قضاوت، قابل اعتمادتر است. این قابلیت تأیید رسمی، یک لایه حیاتی از اطمینان را به اثبات‌های تولید شده توسط هوش مصنوعی اضافه می‌کند که برای پذیرش آن در کاربردهای علمی و صنعتی ضروری است. تحقیقات آینده بر ترکیب سیستم‌های رسمی با LLMها برای پرداختن به حدس‌های باز (open conjectures) در ریاضیات تمرکز خواهد کرد. این مسیر، پتانسیل کشف دانش ریاضی جدید و حل مسائلی را دارد که دهه‌ها یا حتی قرن‌هاست بشریت را به چالش کشیده‌اند. این تلفیق قدرت هوش مصنوعی و سخت‌گیری منطق رسمی، مرزهای اکتشاف ریاضی را گسترش خواهد داد.

منبع مقاله: MarkTechPost