ШІ Astra розв'язав задачі, над якими математики билися десятиліттями

1 серпня OpenAI оприлюднила результати роботи нової моделі Astra, яка, за даними компанії, розв'язала десять відкритих математичних задач. Серед них — проблеми з теорії груп, високовимірної геометрії, теорії кодування, квантової складності, криптографії на ґратках та екстремальної комбінаторики. Зокрема, модель підтвердила існування несофічних груп, розв'язала задачу, пов'язану з гіпотезою жорсткості Коннеса, покращила верхню межу щільності упаковки сфер у високих вимірах (цей показник не змінювався з 1978 року) та розв'язала три задачі з каталогу відкритих проблем математика Пола Ердеша.

Головною особливістю проєкту стало те, що кожне доведення формалізоване у системі Lean — програмному помічнику, який автоматично перевіряє логічні кроки. Якщо хоча б один крок хибний, програма відхиляє доказ. Усі сертифікати перевірки опубліковані на GitHub, тож будь-хто може завантажити файли та перевірити їх самостійно. За оцінкою OpenAI, вартість отримання цих результатів становила близько 2000 доларів, а до релізу додається 249-сторінкова збірка розв'язань.

Це вже другий гучний результат Astra: у травні модель спростувала гіпотезу одиничної відстані Ердеша, яка залишалася відкритою близько 80 років. Низка відомих математиків позитивно оцінила нову роботу. Лауреат медалі Філдса Тім Говерс заявив, що без вагань рекомендував би ці доведення до публікації у провідному математичному журналі. Разом із вісьмома колегами, зокрема Ногою Алоном, він підготував окрему статтю з поясненням доказів у доступнішій формі. Томас Блум, який веде каталог задач Ердеша, назвав серпневі результати «великою новиною».

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

Попри суперечки, машинно перевірені сертифікати змінюють підхід до оцінки результатів ШІ: раніше наукова спільнота мусила довіряти заявам розробників, тепер правильність доведень можна незалежно перевірити автоматично. В OpenAI наголошують, що подібні механізми вже використовуються у проєктуванні мікросхем, криптографії та перевірці критичного програмного забезпечення. Тим часом конкуренти не відстають: модель Claude Fable 5 від Anthropic разом із науковцями знайшла ймовірний контрприклад до гіпотези Якобіана, яка залишається нерозв'язаною з 1939 року, але ця робота ще очікує на рецензування.