OpenAI просить незалежних експертів перевірити згенеровані ШІ докази в математиці, інформатиці та фізиці

OpenAI заявляє, що її внутрішні моделі спростували одне з центральних припущень інформатики та довели частину однієї з математичних задач тисячоліття. Тепер незалежні фахівці мають визначити, чи витримують докази перевірку.

Компанія описала три результати з математики, інформатики та фізики у своєму дописі. За словами OpenAI, докази створили її внутрішні моделі ШІ. Компанія називає рукописи своєрідними первинними дослідницькими даними, які ще потрібно осмислити.

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

Lean — це мова програмування, яка дає змогу комп’ютеру перевіряти кожен крок доказу. Однак така перевірка не гарантує відсутності помилок: Lean встановлює лише, чи випливає твердження з доказу, записаного цією мовою. Експертам іще потрібно з’ясувати, чи справді формулювання відповідає задачі, яку мали на увазі.

Якщо OpenAI має рацію, одне з базових припущень інформатики хибне

Результат з інформатики стосується гіпотези експоненційного часу (ETH) і задачі булевої здійсненності, або SAT. У SAT потрібно визначити, чи можна надати змінним у логічній формулі значення «істина» або «хиба» так, щоб уся формула стала істинною.

Якщо змінних небагато, можна перебрати всі комбінації. Але кожна нова змінна подвоює кількість варіантів. Для 100 змінних їх уже стільки, що число має 31 цифру.

Простіше кажучи, ETH стверджує, що істотного способу обійти повний перебір немає. Його можна пришвидшити, але в найгіршому випадку час обчислень усе одно зростає експоненційно — з кожною новою змінною в певну кількість разів.

За словами OpenAI, задача SAT тісно пов’язана з проблемою P проти NP. Це відкрите питання про те, чи можна швидко розв’язати задачу, для якої швидко перевіряється правильність відповіді. У випадку SAT перевірити запропонований варіант нескладно: достатньо підставити значення й обчислити формулу. Найважче — знайти відповідний варіант.

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

ETH уточнює це припущення: вона стверджує не лише, що SAT складна, а й наскільки саме. Навіть якщо ETH виявиться хибною, P усе ще може не дорівнювати NP — тобто складні задачі не обов’язково стануть легкими.

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

Тепер OpenAI заявляє, що її система довела хибність ETH. Якщо доказ витримає перевірку, праці, побудовані на цій гіпотезі, втратять підґрунтя. Це не означатиме, що їхні результати автоматично неправильні, але вони вже не матимуть доведеного обґрунтування.

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

Практична користь поки незрозуміла, а теоретичні наслідки можуть бути значними

SAT має багато практичних застосувань. Спеціальні програми — SAT-розв’язувачі — використовують, наприклад, для пошуку помилок у проєктах мікросхем і тестування програмного забезпечення.

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

Професор MIT Раян Вільямс також висловився обережно. Коли користувач X запитав, що першими помітять звичайні розробники, Вільямс відповів, що цього поки ніхто не знає. За нинішнього темпу, припустив він, протягом 12 місяців можливий суттєвий поступ у практичному розв’язанні SAT.

«А може, нічого подібного й не станеться. Я справді не знаю», — додав він.

Результат може вплинути й на теорію складності, зокрема на дослідження схем — мереж простих логічних елементів AND, OR і NOT. Якщо доказ OpenAI правильний, то, за словами Вільямса, з нього випливатиме, що певний клас дуже складних задач неможливо розв’язати за допомогою малих схем. Тут «мала» означає, що зі збільшенням довжини входу вдвічі схемі потрібно не більш як приблизно вдвічі більше елементів.

Гіпотезу ETH перевіряють науковці, які її запропонували

Вільямс незалежно перевірятиме й пояснюватиме результат разом із Расселом Імпальяццо та Рамамоханом Патурі з Каліфорнійського університету в Сан-Дієго. Імпальяццо й Патурі запропонували ETH разом із Френсісом Зейном. Вільямс пише, що група не підписувала угод про нерозголошення, працює без оплати й планує ділитися проміжними висновками.

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

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

Гіпотезу про хвилі, якій кілька десятиліть, могли довести для всіх вимірів

Математичний результат стосується гіпотези про хвилі — зокрема звукові, світлові та сейсмічні. Її запропонував математик Крістофер Соджі у 1991 році.

Хвилі можуть концентруватися в одній точці — подібно до світла у фокусі збільшувального скла. Гіпотеза стверджує, що така надмірна концентрація триває недовго. Якщо усереднити поведінку хвиль у часі, вона виявиться плавнішою або рівномірнішою, ніж можна було б очікувати з огляду на екстремальний випадок. Звідси й назва — гіпотеза про локальне згладжування.

Досі її довели лише для двох вимірів — хвиль на поверхні, наприклад води. Це зробили Гут, Ван і Чжан у 2019 році. OpenAI стверджує, що її моделі створили доказ для будь-якої кількості вимірів: від хвиль у просторі до гіпотетичних просторів із більшою кількістю вимірів.

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

Гіпотеза Какея показує, наскільки складними є навіть похідні результати. У 2025 році Ван і Заль довели її лише для трьох вимірів. За твердженням OpenAI, тепер обидві гіпотези будуть доведені для будь-якої кількості вимірів.

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

OpenAI прагне надати квантовій теорії поля строгого математичного підґрунтя

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

Натомість фізики використовують наближення, наприклад уявну ґратку точок, яку поступово роблять дедалі дрібнішою. Відкритим залишається питання, чи дає це змогу отримати єдину й несуперечливу теорію — тобто чи «існує» вона в математичному сенсі. Питання, чи правильно така теорія описує природу, є окремим.

OpenAI заявляє, що її ШІ довів існування певних квантових теорій поля у чотирьох вимірах — трьох просторових і часі. Досі нікому не вдавалося довести в чотирьох вимірах існування теорій, у яких частинки взаємодіють між собою.

У центрі результату — сильна взаємодія. Вона зв’язує кварки в протони й нейтрони, а ті утворюють атомні ядра. Переносниками цієї взаємодії є частинки-глюони. Доказ охоплює три теорії, які послідовно розвивають одна одну.

Перший рівень — теорія Янга—Міллса. Вона описує лише глюони, без кварків, і пов’язана з однією із семи задач тисячоліття. За розв’язання кожної з них Математичний інститут Клея пропонує приз у розмірі 1 мільйон доларів.

Задача має дві частини: довести математичне існування теорії Янга—Міллса та показати, що в ній є так звана масова щілина. OpenAI прямо зазначає, що розв’язала лише частину про існування. Отже, задачу тисячоліття повністю не розв’язано.

Масова щілина пов’язана з певною загадкою. У рівняннях глюони не мають маси, а сили, які переносять безмасові частинки, зазвичай діють на великих відстанях. Приклад — електромагнітна сила, переносником якої є безмасове світло. Натомість сильна взаємодія діє лише на дуже малих відстанях, наприклад усередині атомного ядра. Фізики пояснюють це тим, що глюони об’єднуються в структури, які мають масу; навіть найлегша з них не є безмасовою. Різниця між нульовою масою та найменшою можливою масою таких структур і називається масовою щілиною. Комп’ютерне моделювання підтверджує її існування, але математично її ще ніхто не довів.

Другий рівень — квантова хромодинаміка (КХД). Вона додає кварки й дає повний опис сильної взаємодії.

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

Третім рівнем зазвичай мала б бути Стандартна модель фізики частинок. Вона описує три з чотирьох фундаментальних взаємодій — усі, крім гравітації. Однак, за словами OpenAI, її не можна поширити на довільно малі відстані: деякі взаємодії в ній там не слабшають, а посилюються.

Тому доказ охоплює найпростішу теорію великого об’єднання. Вона зводить три взаємодії до однієї та включає частинки-переносники сил і частинки матерії зі Стандартної моделі. Як і сильна взаємодія, об’єднана сила може слабшати на малих відстанях. Однак експерименти таких теорій не підтвердили.

Якщо доказ витримає перевірку, усі три рівні матимуть математичне підґрунтя. Це не змінить фізичних передбачень. OpenAI сподівається, що результат допоможе перетворити квантову теорію поля на математично строгий напрям науки.

Роботу перевірятиме група на чолі з Девідом Ґроссом, який розділив Нобелівську премію з фізики 2004 року за дослідження асимптотичної свободи. До групи також увійшли Майкл Дуглас, Артур Джаффе, Ігор Клебанов і Микита Некрасов. Джаффе допомагав формулювати задачу тисячоліття про теорію Янга—Міллса.

OpenAI повідомляє, що вже переклала доказ теорії Янга—Міллса мовою Lean. Однак, на відміну від групи з інформатики, ця група поки не публікуватиме матеріали ШІ й планує самостійно викласти результат.

Процес перевірки OpenAI сам собою порушує питання

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

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

Крім того, OpenAI пообіцяла передати 5 мільйонів доларів Фонду Саймонса на семінари й конференції, присвячені результатам, отриманим за допомогою ШІ.

У відкритому листі група Вільямса закликає до ширшої дискусії, яка не обмежується перевіркою доказів. Ідеться про те, як перевіряти наукові прориви, створені ШІ, хто має отримувати до них доступ і кому належить віддавати наукове визнання.

Нагадаємо, у бенчмарку TheoPhysEval модель GPT-6-Astra розв’язала 49 із 50 задач, а автори дослідження зазначили, що найсильніші AI-агенти вже справляються з обчислювальними задачами з теоретичної фізики на рівні провідних фахівців.