Внутрішня система OpenAI створила аналітичний доказ, який, за твердженням компанії, розв’язує одну із семи задач тисячоліття — проблему існування та гладкості розв’язків рівнянь Нав’є — Стокса. OpenAI також представила формалізацію доказу мовою Lean.
Внутрішня система OpenAI створила аналітичний доказ, який, за твердженням компанії, розв’язує одну із семи задач тисячоліття — проблему існування та гладкості розв’язків рівнянь Нав’є — Стокса. OpenAI також представила формалізацію доказу мовою Lean.
Йдеться про одну з найвідоміших нерозв’язаних проблем сучасної математики. Питання про те, чи можуть тривимірні рівняння руху рідини за певних умов породити сингулярність, залишалося відкритим близько 90 років.
OpenAI підкреслює: компанія не претендує на грошову премію Clay Mathematics Institute за цю роботу. Результат опублікований як демонстрація можливостей її нової AI-системи.
Рівняння Нав’є-Стокса описують рух рідин і газів. Вони лежать в основі багатьох практичних задач — від проєктування літаків і прогнозування погоди до моделювання кровотоку.
Проблема полягає не в тому, чи можна розв’язати ці рівняння для конкретної ситуації. Математики десятиліттями намагалися з’ясувати фундаментальніше питання: чи завжди гладкий початковий рух тривимірної нестисливої рідини залишається гладким, чи за кінцевий час у ньому може виникнути сингулярність.
У цьому контексті сингулярність означає ситуацію, коли швидкість частинок у математичній моделі за кінцевий проміжок часу зростає без обмеження.
Це особливо цікаво через наявність в’язкості. Вона, навпаки, має згладжувати рух рідини. Тобто математична конструкція повинна показати, як система сама доходить до точки, де її опис ламається, попри цей стабілізуючий ефект.
Рівняння пов’язані з роботами Клода-Луї Нав’є та Джорджа Габріеля Стокса у XIX столітті. У 1934 році Жан Лере довів існування узагальнених розв’язків, але питання про те, чи залишаються вони гладкими, так і залишилося відкритим.
У 2000 році Clay Mathematics Institute включив проблему Нав’є — Стокса до семи задач тисячоліття.
За даними OpenAI, її система створила аналітичний доказ того, що рідина, яка спочатку перебуває у стані спокою та є гладкою, може за кінцевий час сформувати сингулярність.
При цьому на систему діє гладка зовнішня сила, а енергія рідини залишається кінцевою протягом усього процесу — від початкового стану до моменту формування сингулярності.
Розв’язок являє собою вихор. Він закручується всередину і водночас витягується вздовж осі — OpenAI порівнює його форму зі спагеті. Центральна область вихору стискається і прискорюється, але загальна енергія залишається кінцевою.
Саме тут і полягає математична складність. У рівнянні одночасно присутні прискорення, градієнти тиску, перенесення імпульсу та в’язкість. Вони повинні ставати дуже великими, але при цьому точно компенсувати один одного. У результаті зовнішня сила залишається гладкою, тоді як швидкість рідини необмежено зростає.
OpenAI стверджує, що цей результат відповідає твердженню C, а також D в офіційній постановці задачі тисячоліття.
Цікава частина історії — не лише сам доказ, а спосіб, у який його отримали.
28 серпня OpenAI почала тренувати нову внутрішню модель. А 1 вересня команда компанії отримала інформацію про те, що нібито могли бути розв’язані дві задачі тисячоліття.
Після цього OpenAI запустила систему, яка мала перевірити всі нерозв’язані задачі тисячоліття та кілька інших складних математичних проблем.
Замість одного агента компанія використала систему координованих AI-агентів. Вони могли працювати з кешованою версією інтернету та запускати код, а також обмінюватися інформацією всередині своїх груп.
Група, яка працювала над Нав’є — Стоксом, налічувала близько 10 000 одночасних агентів. OpenAI каже, що під час експерименту зберігала ті самі запобіжники, що й під час інших оцінювань frontier-моделей, зокрема ізоляцію та моніторинг.
Для різних груп агентів формулювали різні варіанти задачі. У випадку Нав’є — Стокса частині систем запропонували версії A і B, де потрібно було знайти доказ, а іншим — C і D, де результатом мав стати контрприклад.
Це дозволило не змушувати всю систему рухатися в одному напрямку.
До Нав’є — Стокса агенти працювали і над дещо простішою спорідненою проблемою — регулярністю рівнянь Ейлера, де відсутній член, що відповідає за в’язкість.
Тут система також знайшла результат, який OpenAI описує як спростування відповідної гіпотези. Над ним працювали майже 100 агентів приблизно 50 годин.
Після цього команда вирішила, що саме Нав’є — Стокс є найбільш перспективною ціллю, і перенаправила туди ресурси з інших задач тисячоліття.
OpenAI також використовувала Codex, щоб об’єднувати найбільш корисні результати, отримані різними групами агентів.
Агенти отримали свій результат 5 вересня — приблизно через 88 годин після запуску роботи.
Після цього знадобилося ще 17 годин, щоб формалізувати та перевірити доказ за допомогою Lean і GPT-6 Astra.
У підсумку OpenAI опублікувала не лише математичний текст, а й формалізований доказ, який можна перевіряти за допомогою системи формальної математики.
За весь експеримент агенти відправили 4,9 млн повідомлень і використали близько 300 млрд output-токенів.
Безпосередньо під час роботи над Нав’є — Стоксом вони відправили 2,7 млн повідомлень і використали приблизно 130 млрд output-токенів.
Тобто це не історія про один запит до чат-бота на кшталт «розв’яжи задачу, яку математики не можуть вирішити 90 років». Йдеться про величезну багаторівневу систему, в якій тисячі агентів паралельно шукали різні математичні конструкції, перевіряли їх і передавали результати іншим агентам.
Є важливе уточнення. Навіть сама OpenAI не називає це отриманням Millennium Prize.
Компанія прямо зазначає, що її мета — продемонструвати прогрес можливостей AI-моделей, а не претендувати на грошову премію.
Формально премія за задачу Нав’є — Стокса становить $1 млн і присуджується Clay Mathematics Institute. Для цього результат має пройти відповідний процес математичного визнання та перевірки. Тому наразі коректніше говорити, що OpenAI опублікувала AI-генерований доказ, який, за твердженням компанії, розв’язує задачу, а не що математичну задачу остаточно закрито всією науковою спільнотою.
OpenAI опублікувала повний опис доказу, а також формалізацію в Lean на GitHub.
За словами співзасновника IT-підприємця Ярослава Ажнюка, це величезний прорив, який матиме наслідки для авіації та ракетобудування, медицини, прогнозування погоди, енергетики, кораблебудування, напівпровідникової електроніки, та інших сфер.
«Але більший вплив це матиме на застосування ШІ для подальших наукових винаходів. На сьогодні — це найвидатніше досягнення ШІ у сфері науки. Вочевидь — це лише початок. І так, звичайно ж є двоє вчених, один з яких ще й працює у конкурентів OpenAI — Antropic, які ствоерджують що були першими хто знайшов рішення, і довкола цього зараз розгорається контраверсія. У неймовірні часи ми живемо, друзі. Неймовірні часи», — зауважи він.
