دنیای اثبات قضایای ریاضی (Formal Theorem Proving) همیشه یکی از چالشبرانگیزترین حوزهها برای یادگیری ماشین بوده است. مشکل اصلی؟ سیستمهای مختلفِ اثبات ریاضی (مثل Lean 4 یا Isabelle) با هم سازگار نیستند و این یعنی دانشمندان نمیتوانند به راحتی از دانش یک سیستم در سیستم دیگر استفاده کنند.
حالا محققان با معرفی ITPEval، اولین بنچمارک استاندارد برای ترجمه خودکار اثباتهای ریاضی بین سیستمهای مختلف را ارائه دادهاند. این ابزار به مدلهای زبانی (LLMs) کمک میکند تا «زبان»ِ سیستمهای مختلف اثبات را یاد بگیرند و فاصله بین کتابخانههای ریاضی را پر کنند.
نتایج نشان میدهد که اگرچه مدلهای هوش مصنوعی هنوز در ترجمه کامل اثباتها در سطح اکوسیستمهای پیچیده مسیر طولانی دارند، اما این قدم بزرگ، راه را برای خودکارسازی اثباتهای ریاضیِ فوقپیچیده باز میکند.
منبع: arXiv AI