OpenAI компаниясының Astra моделінің ішкі нұсқасы математика саласында серпіліс жасап, он жылдан астам уақыт бойы ашық күйінде қалған математика мен информатиканың 10 есебін шешті. Нәтижелер қатаң дәлелдемелер түрінде ұсынылды, деп хабарлайды infohub.kz сайты.
OpenAI компаниясы GitHub платформасында Apache 2.0 лицензиясымен 10 шешілмеген есепке арналған 249 беттік қолжазба жинағын және Lean 4 цифрлық сертификаттарын жариялады. Алгоритм арқылы шығарылған барлық дәлелдемелер логикалық тізбектерде бірде-бір олқылықсыз формальды машиналық тексеруден сәтті өтті.
Шешілген мәселелердің ішінде — 1980 жылы ұсынылған Коннның қатаңдық гипотезасын жоққа шығару, несофиялық топтың бар екендігінің дәлелдемесін құру, сондай-ақ Пол Эрдёштің көп түсті Рамсей сандарына қатысты №183 есебін шешу. Сонымен қатар, Astra көп өлшемді кеңістіктерде сфераларды орау, кванттық қайталау және алгоритмдердің күрделілігі салаларында да шешімдер тапты.
Жаңа Astra жүйесі бірнеше агенттердің жұмысын үйлестіру арқылы күрделі есептермен ұзақ уақыт жұмыс істеуге арналған. Зерттеуші Ноам Браунның айтуынша, токендерге жұмсалған шығын небәрі 2000 долларды құрады. Дегенмен, ұсынылған нәтижелердің бәрі әлі де ғалымдардың сараптамалық рецензиясынан өтуі тиіс.