Astra OpenAI-дан: жаңа модель он шешілмеген математикалық есепті шешті
Жасанды интеллект әлемінде математиктер ондаған жылдар бойы күткен оқиға болды. 1 тамызда OpenAI компаниясы 2016 жылдан бері және одан да ертерек ашық күйінде қалған он математикалық есепке дәлелдемелер ұсынды. Бұл — жай ғана ИИ дамуындағы кезекті қадам емес, іргелі ғылымдағы үлкен тілдік модельдердің мүмкіндіктері туралы түсінікті өзгертетін серпіліс.
Шешімдер Astra-ның ішкі нұсқасымен алынды — бұл ChatGPT әзірлеушісі іске қосуға дайындап жатқан келесі флагмандық модель. OpenAI бағалауынша, жауаптарды іздеуге кеткен есептеу шығындары Sol үшін API тарифтері бойынша шамамен $2000 құрар еді, бұл жаңа тәсілдің тиімділігін көрсетеді. Қолжазбаларды зерттеушілер модельмен бірлесіп дайындады, содан кейін ол әрбір дәлелдемені Lean — теоремаларды машиналық тексеру тілінде формализациялады. Барлық сертификаттар мен пайымдау жазбалары ашық қолжетімділікте жарияланды, бұл ғылыми қоғамдастыққа нәтижелерді тексеруге мүмкіндік береді.
Astra Sol, Terra және Luna қатарлы модельдердің жеке класы ретінде ұсынылады. OpenAI әзірге оның GPT-6 ретінде ме, әлде GPT-5 желісіндегі нұсқа ретінде ме шығатынын шешкен жоқ, ал шығарылым күні белгіленбеген. Дегенмен, 26 шілдеде бас директор Сэм Альтман Astra-ны Вашингтонда саясаткерлер мен реттеушілерге көрсетті. Бұл кездейсоқ емес: модель Дональд Трамп әкімшілігінің ИИ әзірлеушілерін жаңа жүйелерді жұртшылыққа іске қосуға дейін федералды билікке бағалауға тапсыруға міндеттейтін жаңа ережелері бойынша тексерілетін алғашқы модель болуы мүмкін.
Математикадағы серпіліс: софикалық емес топтардан кванттық ойындарға дейін
Негізгі нәтижелердің ішінде — софикалық емес топтардың бар екенін дәлелдейтін конструкция. Бұл математиктер 1999 жылдан бері, Михаил Громов софикалық ұғымын енгізгеннен бері шеше алмаған орталық мәселені жабады. Сондай-ақ модель Конның фон-Нейман алгебралары туралы қаттылық гипотезасын жоққа шығарды, Эрхарттың көлем туралы гипотезасын шешті және Эрдештің №183 көптүсті Рамсей сандары туралы есебін шешті. Astra арифметикалық схемалармен перманентті есептеу күрделілігінің жаңа төменгі бағаларын алды және екі ойыншының кванттық ойындары үшін параллель қайталау теоремасын дәлелдеді.
Жоғары өлшемдерде шарларды орау кезіндегі тығыздықтың жоғарғы бағаларын Кон–Элкис шегіне дейін жақсарту және кез келген берілген минималды қашықтықта екілік кодтар үшін шекараларды күшейту ерекше назар аударуға тұрарлық. Манчестер университетінің математигі Томас Блум бұл нәтижелерді «үлкен жаңалық» және конструкциялар саласындағы «салмақты қадам» деп атады.
Big news! (And not really my area, but yes, I would rank this as bigger than the unit distance counterexample. Maybe not bigger than a proof of unit distance would have been, but in terms of constructions, this is big.) https://t.co/VDRti1HZ6Z
— Thomas Bloom (@thomasfbloom) August 1, 2026
Дегенмен, Astra бәрін де істей алмайды. Модельдің пайымдау технологиясының авторларының бірі Ноам Браун OpenAI-да басқа да ірі мәселелерге кірісуге тырысқанын, бірақ сәтсіз болғанын хабарлады. Модель «мыңжылдық есептерін» — Клэй математика институты 2000 жылы математикадағы басты мәселелер деп атаған жеті сұрақты шеше алмады, әрқайсысын шешу үшін $1 млн уәде етілген.
Бұл нәтиже ИИ мен іргелі ғылымның симбиозындағы жаңа дәуірді белгілейді. «Мыңжылдық есептердің» толық шешіміне әлі алыс болса да, Astra-ның Lean-де формальды дәлелдемелермен жұмыс істеу қабілеті — бұл жай техникалық жетістік емес, математикалық жаңалықтарды жылдар бойы алға жылжыта алатын құрал. Менің талдауымша, бұл нарық үшін де сигнал: ИИ зерттеулеріне салынған инвестициялар коммерциялық қосымшалардан әлдеқайда асып түсетін нәтижелер бере бастады, бұл OpenAI сияқты компаниялардың стратегиялық құндылығын арттырады.