Математична спільнота дедалі гучніше ставить під сумнів, чи можна довіряти 719 штучно згенерованим рукописам OpenAI, після того як нова робота заявила: оприлюднений раніше доказ Нав’є–Стокса у статті не збігається з його формально перевіреною версією в Lean.
Основне:
- Каталог OpenAI скоротився з 722 до 719 рукописів після відкликання трьох робіт через помилку зі знаком.
- Троє математиків із Великої Британії задокументували дві розбіжності між текстовим доказом Нав’є–Стокса та його кодом на Lean.
- Автори не називають доказ хибним, але наголошують: машинна перевірка не може замінити рецензування фахівцями.
Масовий реліз математичних результатів OpenAI
Компанія виклала колекцію робіт 6 жовтня. Як з’ясувалося у звіті, оприлюдненому в четвер, вона відступила від рекомендацій, які незалежна група математиків розробила спеціально для лабораторій ШІ. Каталог спершу містив 722 рукописи, але вже наступного дня OpenAI відкликала три роботи: одна впала через помилку зі знаком, ще дві спиралися на цей зламаний аргумент.
Рекомендації, оприлюднені 29 вересня дев’ятичленною Advisory Group on Mathematics and Artificial Intelligence, починаються з заклику до лабораторій припинити тестувати складні математичні задачі на закритих моделях. У своєму репозиторії OpenAI зазначає, що статті отримано шляхом прогону нерелізної внутрішньої моделі по відкритим дослідницьким задачам.
Лише до 10 результатів додані розлогі описи міркувань моделі, а приблизно 42% «верхньорівневих» тверджень формалізовані в Lean — мові, що дозволяє комп’ютеру формально перевірити доказ.
Читайте також: Скільки заробляє СЕО Anthropic? Відповідь у заявці на IPO
Прогалини в доказі Нав’є–Стокса
Alexander Bastounis з King’s College London та Fabian Circelli й Anders Hansen з University of Cambridge проаналізували представлений OpenAI у вересні доказ задачі Нав’є–Стокса. Вони виявили дві ділянки, де рукопис і код Lean розходяться, зокрема випадок, коли код доводить слабшу оцінку, ніж та, що заявлена в статті.
Автори наголошують, що не стверджують хибність паперового доказу. Їхня теза вужча: Lean підтверджує істинність фінальної теореми, але не може гарантувати коректність усіх проміжних кроків, які читає людина. Тож навіть формалізовані докази потребують повноцінного експертного рецензування.
Лауреат медалі Філдса Terence Tao 6 жовтня написав, що задачі зараз розв’язують «AI-промптери», які самі недостатньо розуміють отримані результати, аби відповідати на запитання чи читати на їхній основі доповіді. Професорка Гарварду Melanie Matchett Wood, членкиня дорадчої групи, зауважила: у момент публікації ніхто з людей повністю не розуміє такі результати, «і саме тепер починається справжня робота».
Суперечка навколо доказів OpenAI
Дорадча група наголосила: лише широка математична спільнота може оцінити, наскільки ретельно OpenAI дотрималася її рекомендацій. Цей пильний погляд наклався на напружений місяць. 8 вересня OpenAI оголосила про результат щодо Нав’є–Стокса, що відразу спричинило конфлікт навколо авторства з математиком New York University Tristan Buckmaster. Уже через три дні 25 медалістів Філдса оприлюднили декларацію з попередженням, що масове штампування AI-результатів може зашкодити розвиткові галузі.
Читайте далі: AI-математика OpenAI: 722 роботи стали публічними — тепер слово за спільнотою
