В OpenAI допустила ошибку в переводе математических выражений в код при доказательстве уравнений Навье-Стокса.😇
👥 Когда компания OpenAI объявила о своем неожиданном решении задачи Навье-Стокса, она представила одно доказательство для людей и одно для компьютеров — однако они не совпадают.‼
Группа математиков утверждает, что OpenAI, по всей видимости, допустила незначительную ошибку при публикации доказательств задачи Навье-Стокса. Эта ошибка не означает, что доказательства неверны или что OpenAI не смогла правильно решить задачу, но она ставит под сомнение возможность полагаться на математические результаты, полученные с помощью моделей ИИ.
«Все эти объемные доказательства, созданные с помощью языковых моделей, должны быть прочитаны людьми, а это создает огромную дополнительную нагрузку на математиков», — говорит Андерс Хансен из Кембриджского университета.
8 сентября компания OpenAI объявила о нахождении решения задачи Навье-Стокса , одной из самых известных открытых проблем в математике. Доказательство было опубликовано в двух версиях – одна написана на «естественном языке», то есть на комбинации английского языка и математических символов, как это сделал бы математик, а другая – на языке Lean. Доказательство на языке Lean призвано формализовать версию на естественном языке, позволяя компьютеру механически проверять истинность всех его логических утверждений. Проблема, по словам Хансена и его команды, заключается в том, что они не совпадают.
«Этот процесс формализации пытается заменить экспертную оценку», — говорит член команды Фабиан Чирчелли , также работающий в Кембриджском университете. «Экспертная оценка означала бы, что доказательства проверяются человеческим взглядом. Но в этой статье мы показали, что использование такого типа автоматической формализации с помощью ИИ не может служить той же цели».
Чтобы было понятно, исследователи не утверждают, что OpenAI не удалось решить задачу Навье-Стокса. Вполне возможно, что и доказательство на естественном языке, и доказательство на языке Lean предоставляют решение, так же как существуют сотни допустимых доказательств теоремы Пифагора . Вместо этого, их тезис более тонкий: модель OpenAI «неправильно перевела» данные при преобразовании в формат Lean.
«Мы не утверждаем, что доказательство на естественном языке неверно, — говорит Хансен. — И мы не утверждаем, что оно верное». Проблема в том, что OpenAI представляет два доказательства как идентичные, заявляя на Github : «Этот репозиторий содержит формализации результатов, представленных в [статье] „Взрыв в уравнениях Навье-Стокса за конечное время“, выполненные с использованием Lean 4».
Эта ошибка перевода возникает потому, что ИИ должен создать «бережливое» доказательство, которое «компилируется», то есть компьютерный код полностью самосогласован и не выдает ошибок, говорит Хансен. Если в процессе автоматической формализации ИИ обнаружит участок доказательства, который не компилируется, он попытается найти обходное решение, даже если это означает отклонение от доказательства, написанного на естественном языке.
Конкретное утверждение команды основано на части доказательств, называемой леммой 8.6. В доказательстве на естественном языке уравнение в этой части требует, чтобы определенное значение было меньше m + 4, где m — целое число. В доказательстве Lean эквивалентное значение должно быть меньше m + 5, что математически слабее.
Чтобы понять почему, представьте, что вас просят решить уравнение x + 3 = 6, ответ на которое x = 3. Можно написать доказательство того, что x должно быть меньше 4, а также того, что x должно быть меньше 5. Оба эти утверждения являются совершенно верными математическими утверждениями, но они говорят о разных вещах. Последнее доказательство допускает больше возможных ответов для x , что делает его математически менее убедительным.