Математична спільнота ставить під сумнів надійність 719 згенерованих ШІ математичних манускриптів OpenAI після того, як у новій роботі заявили, що оприлюднений компанією доказ рівнянь Нав’є–Стокса не збігається з його формалізованою, комп’ютерно перевіреною версією.
Головне:
- Каталог OpenAI скоротився з 722 до 719 робіт після відкликання трьох манускриптів через помилку зі знаком.
- Троє математиків з Великої Британії задокументували дві невідповідності між опублікованим доказом Нав’є–Стокса та його кодом Lean.
- Автори не стверджують, що доказ хибний, але наголошують: машинна перевірка не може замінити рецензування фахівцями.
Публікація математичної добірки OpenAI
Компанія виклала колекцію робіт 6 жовтня, а оприлюднений у четвер звіт виявив, що вона відхиляється від принципів, які незалежна група математиків розробила як орієнтир для лабораторій ШІ. Спочатку каталог містив 722 манускрипти. Уже наступного дня OpenAI відкликала три з них після того, як помилка зі знаком зруйнувала один ключовий аргумент і, відповідно, ще дві роботи, що на ньому ґрунтувалися.
Ці принципи, оприлюднені 29 вересня дев’ятичленною Advisory Group on Mathematics and Artificial Intelligence, відкриваються закликом до лабораторій припинити тестувати складні задачі з вищої математики на закритих моделях. У репозиторії OpenAI зазначено, що подані роботи отримано шляхом прогону внутрішньої, ще не релізної моделі на відкритих дослідницьких задачах.
Пояснення ходу міркувань моделі надані лише для десяти результатів, а приблизно 42% фінальних тверджень формалізовано в Lean — мові програмування, яка дає змогу комп’ютеру формально перевірити доказ.
Також читайте: Скільки заробляє CEO Anthropic? IPO‑документи дають відповідь
Прогалини в доказі Нав’є–Стокса
Олександр Бастуніс з King’s College London та Фабіан Чирчеллі й Андерс Хансен з University of Cambridge проаналізували доказ рівнянь Нав’є–Стокса, про який OpenAI оголосила у вересні. Вони описали два місця, де паперовий виклад і код Lean розходяться, зокрема фрагмент, де у формалізації доведено слабшу оцінку, ніж заявлено в статті.
Автори наголошують, що не беруться судити, чи правильний рукописний доказ. Їхній висновок вужчий: Lean підтверджує істинність фінальної теореми, але не гарантує коректність усіх проміжних кроків, які читає людина, тому подібні роботи й надалі потребують повноцінного рецензування.
Лауреат медалі Філдса Теренс Тао написав 6 жовтня, що задачі нині розв’язують «AI‑промптери», які недостатньо розуміють отримані результати, щоб відповідати на запитання чи робити доповіді. Професорка Гарварду Мелані Матчетт Вуд, членкиня консультативної групи, зауважила, що на момент публікації «жодна людина не розуміє таких результатів, і тепер справжня робота лише починається».
Суперечка навколо доказів OpenAI
Консультативна група наголошує, що лише широка математична спільнота може оцінити, наскільки ретельно OpenAI дотрималася її рекомендацій. Цей аналіз розгортається після напруженого місяця. OpenAI оголосила про результат щодо Нав’є–Стокса 8 вересня, що спричинило суперечку про пріоритет з математиком Нью-Йоркського університету Трістаном Бакмастером, а вже за три дні 25 лауреатів медалі Філдса опублікували декларацію з попередженням: масове тиражування результатів за участі ШІ може завдати шкоди розвиткові галузі.
Читайте далі: OpenAI оприлюднила 722 математичні роботи ШІ — тепер слово за математиками
