محققان مدل جدیدی به نام «Aria» را معرفی کردهاند که به طور تخصصی برای اثبات قضایای ریاضی در زبان Lean طراحی شده است. این مدل با استفاده از یک ساختار «گرافگونه» (Dependency Graph) و فرآیند تفکر دومرحلهای، قادر است مسائل پیچیده تحقیقاتی را با دقت بسیار بالا حل کند.
نکته هیجانانگیز اینجاست که Aria نه تنها در بنچمارکهای استاندارد از مدلهای قبلی پیشی گرفته، بلکه در حوزههای فوق تخصصی (مانند حدسهای هومولوژیکی) که مدلهای دیگر شکست میخورند، نتایج چشمگیری ارائه داده است. این یعنی گامی بزرگ به سوی حل خودکار مسائل علمی که قبلاً فقط توسط نوابغ ریاضی قابل انجام بود. 🧠🔢
منبع: arXiv AI
