OpenAI опублікувала на GitHub 372 математичні результати, створені ШІ

OpenAI опублікувала добірку математичних результатів, створених внутрішньою моделлю ШІ. Їх розмістили на GitHub, а не в академічних журналах; формальна верифікація має полегшити перевірку робіт.

• OpenAI оприлюднила 372 математичні результати, згенеровані внутрішньою моделлю.
• Результати мають розв’язувати відкриті задачі або суттєво просуватися до їх розв’язання. Серед них — удосконалення комп’ютерних алгоритмів і поступ у дослідженнях, пов’язаних із гіпотезою Рімана.
• За даними OpenAI, більшість результатів отримали одним запитом до одного агента. У середньому на кожен витратили близько трьох годин обчислень ChatGPT Pro Thinking.

Компанія опублікувала 372 нових математичних результати. Кожен із них, за задумом, розв’язує відкриту проблему або суттєво наближає до її розв’язання. Серед робіт є вдосконалення важливих комп’ютерних алгоритмів і результати, пов’язані з гіпотезою Рімана.

Результати розміщено в репозиторії GitHub разом із журналами змін і посиланнями на джерела. OpenAI також повідомила, що та сама модель створила розв’язок задачі з рівнянь Нав’є—Стокса, який уже кілька тижнів проходить формальну перевірку.

За словами OpenAI, майже кожен результат отримали одним запитом до одного ШІ-агента, хоча деякі задачі потребували кількох спроб. Це різко відрізняється від роботи над розв’язком задачі Нав’є—Стокса: там залучили рій із 10 000 агентів і витратили мільйони доларів на обчислення. У середньому на один результат пішло приблизно три години обчислень ChatGPT Pro Thinking.

Формальна верифікація може полегшити перевірку результатів

Частину доведень формалізували мовою програмування Lean, призначеною для створення математичних доведень, які можна перевірити за допомогою комп’ютера. OpenAI планує формалізувати й інші роботи. Це практичний крок: великий потік результатів, згенерованих ШІ, може перевищити можливості математичної спільноти з перевірки кожного з них вручну.

OpenAI також оприлюднила інформацію про методологію: зокрема, короткі описи процесу міркування моделі, статистику спроб розв’язати задачі й оцінки обчислювальних витрат.

Традиційні журнали не пристосовані до такого темпу

OpenAI розмістила результати на GitHub, а не в рецензованих журналах. Це рішення вказує на те, що традиційний науковий процес може бути надто повільним для такого обсягу потенційно нових знань.

Під час підготовки публікації OpenAI консультувалася з дорадчою групою з математики та штучного інтелекту Інституту перспективних досліджень і загалом дотримувалася її публічних рекомендацій. Водночас компанія не оприлюднила запитів до моделі й подала лише середні обчислювальні витрати, а не дані для кожної задачі. До дорадчої групи входить, зокрема, лауреат Філдсівської премії Тімоті Говерс.

Компанія також оголосила, що фінансуватиме семінари й конференції, присвячені аналізу результатів, створених ШІ. OpenAI визнала, що має покращити якість посилань на джерела та виклад матеріалів. Крім того, компанія працює над відповідальним випуском моделі, який має «безпосередньо надати науковцям найсучасніші можливості».

Водночас OpenAI заздалегідь окреслила повноваження дорадчої групи: математики можуть радити, як повідомляти про результати, але не можуть впливати на те, чи створюватимуть їх і з якою швидкістю.

Математична спільнота не дійшла згоди щодо масового виробництва доведень

Формалізація в Lean дає змогу перевірити логічну коректність доведення, але не визначає, чи є результат математично важливим або оригінальним. OpenAI розраховує, що її напрацювання розширять межі людського знання, однак математики ще не дійшли згоди щодо їхнього значення. Реакції на публікацію варіюються від захоплення до розчарування.

У нещодавньому відкритому листі «Глибока невідповідність ШІ математиці» 25 лауреатів Філдсівської премії попередили про значний розрив між цілями індустрії штучного інтелекту та цілями математиків. На їхню думку, розв’язування задач — лише інструмент і непрямий показник справжньої мети: концептуального розуміння та інсайту. Масове створення правильних тверджень може знищити ґрунт для нових ідей, а не сприяти їх появі; наслідки можуть позначитися й на інших галузях.

Тімоті Говерс застерігав, що за одне-два десятиліття математична література може настільки розростися, що не залишиться спільноти людей, які справді її розуміють. Лауреат Філдсівської премії Теренс Тао наголошував, що підготовка молодих математиків має зосереджуватися на людському складнику, а використання ШІ-інструментів слід суворо обмежувати, щоб зберегти справжнє навчання й розуміння.

Нагадаємо, комп’ютерний зір дає машинам змогу інтерпретувати візуальну інформацію та аналізувати зображення й відео; його застосовують, зокрема, для контролю якості, медичної діагностики та спостереження.