OpenAI перепутала математику с кодом в доказательстве гипотезы Навье — Стокса
OpenAI mistranslated mathematics into code for its Navier-Stokes proof
Математики утверждают, что OpenAI допустила тонкую ошибку при публикации доказательств задачи Навье — Стокса: две версии — для людей и для компьютеров — не совпадают. Это не значит, что доказательство неверно, но ставит под сомнение надёжность результатов, сгенерированных AI. Андерс Хансен из Кембриджского университета отмечает, что все подобные доказательства LLM придётся проверять вручную, а это огромная дополнительная нагрузка на математиков.
«Все эти доказательства, сгенерированные большими языковыми моделями, придётся читать людям, а это создаёт огромную дополнительную нагрузку на математиков».
- krackers
- jey
Этот заголовок совершенно неверен. Правильная аналогия с программированием скорее такая: статья на естественном языке была «проектным документом» перед тем, как её закодировали, а затем, когда её кодировали в виде доказательств на Lean4, конкретные детали оказались немного неточными[1] и были исправлены по ходу написания реализации в коде как машинно-проверяемых доказательств. Что, я уверен, чрезвычайно знакомая ситуация для большинства из нас здесь. Но статья, или «проектный документ», после этого не была исправлена.
Я также считаю, что этот подход «сначала статья, потом код» теперь устарел. Современный способ, в рабочих процессах с поддержкой ИИ, — сначала итеративно работать над «наброском вывода <-> машинно-проверяемым доказательством», постепенно выстраивая свой результат. Вы, конечно, можете оставлять по пути заглушки `sorry` и заполнять их, так что вы не ограничены полностью восходящим подходом. Наконец, когда у вас есть доказательство без `sorry` для ваших утверждений верхнего уровня (теорем), которые вас интересуют, вы можете затем заняться написанием изложения в LaTeX на основе кода на Lean.
1. См. https://arxiv.org/abs/2610.08144 для подробностей, но пример, который они приводят, состоит в том, что ключевая оценка требовала 5 дополнительных порядков производных (и так и было сформулировано в Lean), но в статье утверждалось, что оценка выполняется всего с четырьмя дополнительными производными.