OpenAI загатна за Astra: Следващото голямо AI поколение решава 10 дългогодишни математически задачи
В официална научна публикация, озаглавена „Ten advances in mathematics and theoretical computer science“ [1], компанията OpenAI обяви забележителен научен пробив, загатвайки за следващото си голямо поколение изкуствен интелект под кодовото име Astra. Съобщението веднага привлече медийния отзвук и вниманието на технологичната общност [2]. Според разкритите данни, вътрешна версия на новия модел успешно е решила или е постигнала безпрецедентен напредък по 10 дългогодишни отворени математически и компютърни проблеми.
Това постижение се отличава от досегашните анонси в индустрията по ключов признак: всяко едно от десетте решения е придружено от пълно компютърно доказателство, формализирано на интерактивния доказателствен език Lean 4. Този подход предоставя т.нар. „машинно проверими сертификати“, които изключват възможността за типичните за невронните мрежи халюцинации и гарантират математическата строгост на резултатите [1].
Илюстрация: Svetni.me / източник на данни: OpenAI
Зад кулисите на Astra: Новата архитектура и цената на пробива
Проектът Astra се явява наследник на методологиите за логическо разсъждение от сериите o1 и o3, но с разширен фокус върху автономните изследвания и научните открития. Важно е да се отбележи, че този модел е напълно независим от едноименния проект Google DeepMind (Project Astra), който представлява мултимодален ИИ асистент за ежедневни задачи [2].
Според данните на OpenAI, изчислителните разходи за намирането на тези десет решения са изненадващо ниски – приблизително 2000 долара на задача, изчислено по вътрешните тарифи за Sol API на компанията. Този факт показва висока ефективност на логическите алгоритми, които не разчитат на груба изчислителна сила (brute force), а на насочено разсъждение и систематично търсене в пространството от доказателства.
Друг безпрецедентен ход е решението на OpenAI да посочи самия изкуствен интелект като единствен автор на представените научни ръкописи. От компанията твърдят, че приписването на авторството на хора би омаловажило ролята на системата, тъй като моделите са генерирали както самите математически идеи, така и съответните кодове в Lean 4 [1][2].
Строга математическа верификация с Lean 4
Исторически погледнато, най-големият проблем пред използването на големи езикови модели в математиката беше липсата на гаранция за достоверност. Тъй като моделите работят на вероятностен принцип, те лесно могат да напишат правдоподобно изглеждащи, но всъщност напълно погрешни математически твърдения.
За да разреши това предизвикателство, екипът на OpenAI е интегрирал Astra с интерактивния език за доказателство на теореми Lean 4. Този инструмент действа като безкомпромисен компилатор: ако кодът, описващ математическото доказателство, премине компилацията без грешки, тогава доказателството е логически вярно. Всички генерирани Lean сертификати са публикувани от компанията в публичното хранилище openai/ten-proofs в GitHub. По този начин математическата общност по света може лично и автоматизирано да провери верността на всяка стъпка от изследванията, което поставя нова, по-висока летва за прозрачност в научните съобщения [1].
Десетте математически пробива на Astra
Колекцията от трудове, публикувана от OpenAI, обхваща широк спектър от изключително сложни области – от алгебра до квантова теория.
Ето десетте научни постижения, които моделът е реализирал самостоятелно:
Не-софически групи (Non-sofic groups): Моделът е предоставил първата в историята експлицитна конструкция на не-софическа група. Това решава централен въпрос в геометричната теория на групите, поставен още от Михаил Громов през 1999 г.
Хипотезата за твърдост на Конес (Connes's rigidity conjecture): Astra е опровергал тази дългогодишна хипотеза в теорията на алгебрите на фон Нойман. Моделът е конструирал безкрайно много неизоморфни групи със свойство (T), които имат една и съща групова алгебра на фон Нойман.
Сферично пакетиране в многомерни пространства (High-dimensional sphere packing): Постигнато е първото подобрение на общата горна граница за плътност на сферично пакетиране в големи измерения от 1978 г. насам, достигайки теоретичната граница на Кон–Елкис. Това е ключов въпрос в дискретната геометрия.
Хипотеза за обема на Ерхарт (Ehrhart's volume conjecture): Доказана е точната горна граница на обема $(n+1)^n/n!$ във всяко измерение за изпъкнали тела, чийто центроид е единствената вътрешна решетъчна точка.
Сложност на аритметичните схеми (Arithmetic circuit complexity): Установени са нови долни граници за изчисляване на перманента на матрица – например $\Omega(n^4/\log n)$ за аритметични формули.
Квантово паралелно повторение (Quantum parallel repetition): Доказана е теорема за експоненциално паралелно повторение за всяка квантова игра с двама играчи, което има значение за квантовата сложност.
Задача за най-близкия вектор (Closest Vector Problem - CVP): Моделът е доказал трудност на апроксимацията до полиномиален коефициент ($n^{1/400}$) за Евклидовата CVP чрез редукция от 3SAT, което е изключително важно за развитието на устойчива на квантови атаки киберсигурност.
Многоцветни числа на Рамзи (Multicolor Ramsey numbers): Установена е суперекспоненциална долна граница за многоцветни триъгълни числа на Рамзи, решавайки изцяло Проблем 183 от известните задачи на Ердьош.
Хипотеза за компактността в екстремалната теория на графите: Успешно е решена хипотезата за компактността, която фигурира като Проблем 146 в каталога на Пал Ердьош.
Хипотеза за дегенерацията в екстремалната теория на графите: Решен е Проблем 180 от задачите на Ердьош, завършвайки триадата от пробиви в комбинаториката и теорията на графите.
Тези постижения демонстрират широк обхват на компетентност на модела Astra, съчетаващ геометрично мислене, абстрактна алгебра и теория на сложността [1][2].
Реакция на научната общност и следващи стъпки
Въпреки че Lean 4 доказателствата гарантират логическата вярност на изчисленията, научната общност подхожда към пробива със здравословен скептицизъм. Математиците изтъкват, че езиковата верификация доказва само, че логическите вериги са валидни според дефинираните формални правила. Сега предстои по-бавната задача за хората: да се анализира дали формулираните от ИИ задачи съответстват напълно на историческите математически проблеми и дали методите предлагат нова, фундаментална математическа интуиция.
Някои външни експерти също така призовават OpenAI за по-голяма яснота относно пълната експериментална постановка – например колко опита са били направени от модела, преди да се стигне до успешните доказателства, и какъв е бил общият процент на неуспешните опити. Допълнително, представените от Astra ръкописи не са преминали през традиционния процес на рецензиране (peer review) от академични списания, а са били подложени на „агентно рецензиране“ и проверка от избрани външни специалисти преди публикуването им. Независимо от тези въпроси, използването на компютърни доказателства за решаване на фундаментални теоретични проблеми бележи нова ера, в която изкуственият интелект се превръща от помощен инструмент в пълноправен изследовател [1][2].
Източници
[1] Ten advances in mathematics and theoretical computer science
[2] OpenAI teases Astra, its next major AI model, after it solves 10 long-standing math problems