۱۱ مرداد ۱۴۰۵ – ۰۹:۵۵
به گزارش خبرآنلاین، به نقل از زومیت،مسائل، حوزههای گوناگونی از جمله هندسهی ابعاد بالا، نظریهی کدگذاری، پیچیدگی مدارهای محاسباتی، نظریهی گروهها، جبرهای عملگری، پیچیدگی کوانتومی، رمزنگاری شبکهمحور و ترکیبیات مفرط را در بر میگیرند.
نتایج علمی ارزشمند با استفاده از نسخهی داخلی مدل آسترا به دست آمده است. هزینهی محاسباتی توکنهای مورد نیاز برای یافتن پاسخ این مسائل بر اساس نرخ رابط برنامهنویسی کاربردی (API) مدل Sol، در مجموع حدود دو هزار دلار برآورد میشود.
پس از کشف راهحلها با هوش مصنوعی، متخصصان انسانی به همراه همین مدل پیشنویس مقالات علمی را آماده کردند و در نهایت، مدل توانست صحت هر استدلال را در قالب گواهیهای نرمافزار اثبات قضیهی Lean تأیید و ثبت کند.