OpenAI опублікувала 722 математичні роботи, створені невипущеною моделлю
OpenAI опублікувала на GitHub масштабну добірку математичних результатів, створених її внутрішньою AI-моделлю. Йдеться про 722 рукописи, об'єднані у 372 групи результатів, які охоплюють різні галузі математики.
Про це повідомляє The Verge.
Сама модель, яка створила ці результати, залишається невипущеною. OpenAI описує її як внутрішню frontier-модель, яку компанія використовувала для пошуку розв'язань відкритих математичних задач.
Разом із результатами компанія оприлюднила матеріали для їхньої перевірки, окремі формалізовані докази та інформацію про обчислювальні ресурси, витрачені під час роботи AI.
Що саме опублікувала OpenAI
У репозиторії OpenAI Math на GitHub зараз містяться 722 рукописи. Їх об'єднали у 372 групи, оскільки деякі роботи стосуються одного результату, доповнюють одна одну або пропонують альтернативні докази.
Матеріали охоплюють різні напрямки математики та теоретичної інформатики.
Серед опублікованих тем є, зокрема:
- гіпотези Махлера;
- задача про NP-складність;
- гіпотеза Капланського;
- формула Мезара-Парізі;
- властивості квантових ферромагнетиків;
- структура вільних групових факторів;
- рівняння Власова-Максвелла.
Це не один великий математичний доказ, а велика колекція результатів, отриманих у процесі роботи моделі над тисячами дослідницьких задач.
AI розв'язувала близько 4000 задач
Підписуйтеся на наші соцмережі
OpenAI розповіла і про те, як отримувала ці результати. Під час дослідження моделі їй запропонували приблизно 4000 математичних задач. Після цього результати відбирали, об'єднували та оформлювали у фінальні рукописи.
За даними компанії, в середньому на один результат витрачався обсяг обчислень, еквівалентний приблизно трьом годинам режиму Thinking у ChatGPT Pro.
Водночас OpenAI підкреслює важливе обмеження: не всі результати пройшли однаковий рівень перевірки.
Деякі роботи вже мають формалізовані докази, інші — ще ні. Компанія прямо зазначає, що окремі неформалізовані результати можуть містити помилки, і обіцяє виправляти їх у міру виявлення.
Тобто опубліковані 722 роботи не варто сприймати як 722 незалежні математичні теореми, які вже остаточно підтвердила наукова спільнота. Це набір результатів AI, які ще мають пройти перевірку та осмислення математиками.
Частину доказів можна перевірити комп'ютером
Однією з найцікавіших частин релізу стали формалізації доказів у Lean. Lean — це мова програмування та система формальної перевірки, яка дозволяє записувати математичні докази у формі, яку може перевірити комп'ютер.
OpenAI додає такі формалізації до репозиторію в міру їх підготовки. Тому дослідники можуть не просто прочитати твердження моделі, а й перевірити окремі докази формальними методами.
Це особливо важливо для AI-генерованої математики. Модель може створити переконливий текст доказу, але переконливість сама по собі не означає математичну правильність. Формальна перевірка дозволяє винести частину цієї роботи за межі довіри до самої AI.
OpenAI не показала саму модель
Попри масштаб публікації, компанія поки не випускає модель, яка створила результати. OpenAI називає її внутрішньою невипущеною моделлю. Компанія використовувала її для оцінювання можливостей AI на відкритих дослідницьких задачах після того, як попередні математичні тести перестали достатньо добре відрізняти рівень сучасних моделей.
Ще у вересні OpenAI заявляла, що ця модель вирішила понад 100 давніх відкритих математичних проблем у різних галузях. Серед результатів компанія також називала роботу над задачею Нав'є-Стокса, однією з відомих Millennium Prize Problems. Тепер масштаб результатів став значно зрозумілішим — OpenAI опублікувала сотні пов'язаних із математикою рукописів.
Чому це важливо для науки
Поява таких систем змінює роль AI у математиці. Раніше моделі переважно використовували для допомоги з уже сформульованими задачами, перевірки обчислень або написання коду. Тепер AI-системи дедалі частіше намагаються працювати безпосередньо з відкритими дослідницькими проблемами, де відповідь не була відома заздалегідь. Це потенційно може прискорити математичні дослідження.
AI може перебирати величезну кількість підходів, шукати нетривіальні зв'язки між уже відомими результатами та пропонувати докази, які люди потім перевірятимуть. Але виникає й інша проблема — хто має перевіряти весь цей масив результатів.
Якщо AI починає генерувати сотні нових математичних тверджень, людським дослідникам потрібно витрачати час не лише на власні дослідження, а й на перевірку роботи моделей.
Математики вже критикували OpenAI за спосіб публікації
Цей реліз відбувається на тлі суперечок між OpenAI та частиною математичної спільноти. У вересні компанія створила Advisory Group on Mathematics and Artificial Intelligence — консультативну групу з математиків, яка має допомагати визначати, як відповідально публікувати результати AI у цій сфері.
Деякі математики критикували OpenAI за поспішні публічні заяви про досягнення AI та недостатню увагу до академічних правил публікації результатів.
The Verge раніше писав, що представники математичної спільноти закликали OpenAI публікувати повноцінні наукові роботи, які дозволяють дослідникам розібратися у результатах, а не просто оголошувати про них як про досягнення нової моделі.
У новому релізі компанія намагається зробити результати доступнішими для перевірки. Вона опублікувала рукописи, вихідні матеріали, формалізації в Lean та опис методології.
Водночас OpenAI зазначає, що надалі хоче покращувати оформлення таких матеріалів, зокрема цитування, математичні пояснення та презентацію результатів.
AI поступово стає інструментом для відкриття нової математики
Найважливіше у новому релізі OpenAI — не сама цифра 722. Компанія фактично показує нову модель роботи з математичними дослідженнями: AI генерує потенційні результати, люди перевіряють їх, а формальні системи на кшталт Lean можуть автоматично підтверджувати окремі частини доказів.
Якщо такий підхід масштабуватиметься, AI може стати для математиків не просто інструментом для виконання розрахунків, а своєрідним партнером у пошуку нових результатів.
Поки що, однак, до остаточних висновків далеко. OpenAI сама попереджає, що частина опублікованих матеріалів потребує подальшої перевірки.