OpenAI офіційно представила нове сімейство моделей штучного інтелекту Astra, внутрішня версія якого змогла розв’язати десять складних математичних задач, над якими науковці працювали від 10 до 40 років без суттєвого прогресу. Про результати компанія повідомила після завершення перевірки доказів, а дослідники назвали досягнення одним із найпомітніших застосувань штучного інтелекту у фундаментальній математиці за останні роки.
За інформацією OpenAI, для тестування були обрані відкриті математичні проблеми з різних галузей, серед яких багатовимірна геометрія, теорія кодування, квантова складність та криптографія. У компанії стверджують, що модель не лише знаходила готові відповіді, а й будувала повні логічні доведення, які згодом були оформлені у науковий рукопис обсягом 249 сторінок за участю кількох взаємодіючих агентів штучного інтелекту.
Серед найрезонансніших результатів OpenAI називає першу в історії побудову несофічної групи, а також спростування гіпотези жорсткості Конна, запропонованої ще 1980 року. Крім того, Astra знайшла нові підходи до задач, сформульованих угорським математиком Полом Ердьошем, і покращила оцінки щільності пакування сфер, які залишалися незмінними з 1978 року.
Математик Манчестерського університету Томас Блум, коментуючи результати, назвав їх великою подією для математичної спільноти. Водночас незалежна наукова оцінка всіх отриманих результатів ще триває, адже частина робіт має пройти процедуру рецензування та подальшу перевірку іншими дослідницькими групами.
Для виключення логічних помилок OpenAI повідомила, що всі математичні доведення були формалізовані мовою Lean 4. Такий підхід дозволяє машинно перевіряти кожен крок доказу та підтверджувати його коректність незалежно від людського аналізу. Формальна верифікація дедалі активніше використовується в сучасній математиці для підтвердження складних теорем.
Ще однією особливістю проєкту стала його вартість. За оцінками компанії, обсяг обчислень, необхідний для отримання всіх десяти розв’язків, відповідає приблизно 2 тис. доларів за чинними тарифами API моделі Sol. Розробники наголошують, що це демонструє потенційну можливість використання потужних моделей ШІ у фундаментальних дослідженнях без надзвичайно високих витрат.
Попри досягнення, OpenAI визнає, що Astra поки не змогла розв’язати жодної із семи задач тисячоліття, за кожну з яких Інститут Клея встановив винагороду в розмірі 1 млн доларів. Один із керівників проєкту Ноам Браун зазначив, що команда ще не спрямовувала значні обчислювальні ресурси саме на ці проблеми, однак планує продовжити відповідні експерименти.
Компанія також повідомила, що Astra стане першою лінійкою моделей OpenAI, яка проходитиме нову систему державної оцінки безпеки у США. Генеральний директор OpenAI Сем Альтман уже представив можливості моделі американським політикам і регуляторам. До сімейства також входять моделі Sol, Terra та Luna. Однією з головних відмінностей Astra називають здатність працювати над одним складним завданням безперервно протягом кількох годин або навіть днів із використанням механізмів самокорекції та координації між окремими агентами.
OpenAI була заснована у 2015 році як дослідницька компанія у сфері штучного інтелекту. Після запуску ChatGPT наприкінці 2022 року компанія стала одним із ключових світових розробників генеративного ШІ. Останніми роками OpenAI активно інвестує у створення моделей, здатних виконувати складні наукові дослідження, програмування та математичні доведення.
Формальна перевірка математичних доказів за допомогою Lean 4 вважається одним із найперспективніших напрямів розвитку сучасної математики та комп’ютерних наук. Такий підхід дозволяє автоматично перевіряти правильність кожного логічного кроку й дедалі частіше використовується під час роботи над складними теоремами, де ризик людської помилки особливо високий.
