Lean-верификация не гарантирует корректность доказательств на естественном языке
Navier–Stokes Lost in Translation
Автоформализация всё чаще применяется для проверки математических текстов, в том числе сгенерированных AI, как в анонсированном OpenAI доказательстве blow-up решений уравнений Navier–Stokes. AI переводит текст с естественного языка на Lean, после чего формальное рассуждение легко проверяется механически. Однако автор показывает, что такая проверка может не давать никакой уверенности в исходном аргументе: задача разрешения неоднозначностей математического текста лежит на бесконечном уровне иерархии SCI, то есть сложнее проблемы остановки. Приводятся примеры ошибок AI при переводе утверждений и доказательств в Lean, включая доказательство OpenAI для Navier–Stokes.
В частности, мы показываем, что формализованное доказательство в Lean не соответствует доказательству blow-up решений уравнений Navier–Stokes на естественном языке.
- ComplexSystems
Помимо обычных препирательств об ИИ, похоже, главная сенсация здесь такова:
"В частности, мы показываем, что формализованное доказательство на Lean не соответствует доказательству на естественном языке (NL) о взрыве решений уравнений Навье-Стокса."
Так что эти авторы, похоже, утверждают, что OpenAI на самом деле вовсе не доказал Навье-Стокса. Если я правильно понимаю их идею, они заявляют, что LLM неверно формализовала исходную "естественно-языковую" идею Навье-Стокса. Если это правда, это означало бы, что их мнимое доказательство на Lean на самом деле вовсе не является доказательством Навье-Стокса, а представляет собой неверный перевод исходной естественно-языковой идеи. Если это верно, это действительно смелое заявление, и мне хотелось бы узнать, согласны ли с ним другие исследователи.
- buzzy_hacker
Если я правильно понимаю, здесь ставится под сомнение эквивалентность между доказательством на естественном языке и доказательством на Lean, но не корректность самого доказательства на Lean?
- stared
Для освежения памяти о том, что такое Навье-Стокс, в нескольких словах: https://p.migdal.pl/equations-explained-colorfully/#navier-s...
- vanyle
Эта статья — сплошное ничто. Во-первых, естественный язык не так точен, как Lean, поэтому у вас есть несколько способов перевести рассуждение на NL в Lean. Как показано на рис. 1, LLM неплохо справилась с переводом рассуждения о корнях в сжатой форме.
Более того, статья утверждает, что рассуждения на NL о Навье-Стоксе сильнее, чем на Lean. Насколько я понимаю, LLM-переводчик поленилась и написала минимальный объём кода, удовлетворяющий теореме, без дополнительных более сильных утверждений.
В математических статьях часто говорят: "И кстати, это на самом деле доказывает [более сильное утверждение]", но ИИ с точной целью выполнить перевод никогда бы этого не сделал, поскольку его цель — перевести доказательство, а не заниматься качественной математикой.
- infogulch
В статье показано, что доказательство на Lean и прозаическое (pdf) доказательство не совпадают в точности. Но если теорема на Lean, которую принял Lean, эквивалентна исходной постановке задачи, опубликованной Институтом Клэя, это несоответствие не имеет значения для обоснованности самого доказательства. Это не тривиальное "если": точная формулировка задачи часто так же трудна, как и доказательство. Усилия по валидации должны быть сосредоточены на том, эквивалентна ли теорема на Lean той, что опубликована Институтом Клэя.
Тем не менее, разрыв между доказательством на Lean и pdf раздражает с точки зрения интерпретируемости, а интерпретация — это законная цель, но это не влияет на обоснованность доказательства.
- sigbottle
Столкнёмся ли мы когда-нибудь с кризисом теории значения?
_Предполагая_ два сценария отказа:
- В ядре Lean всегда может быть баг.
- Формализованное утверждение может не соответствовать тому, что _математики_ "на самом деле хотели".
Кажется естественным привести аргумент: "Ну, даже если вы допускаете, что в доказательстве могут быть ошибки, проверить постановку задачи чего-либо наверняка проще, чем решение".
(Одно "приятное свойство" состоит в том, что агенту даже не нужно, чтобы "под-аргументы были верны" согласно _второму_ критерию — возможно, в естественном доказательстве он изобретает объект, незаметно отличающийся от формального, но всё сходится. Если вы гарантируете, что _исходное_ утверждение соответствует, то единственная возможная проблема — ядро Lean. Так что в этом случае рекурсия не бесконечна).
Но "определения" — всегда очень странная вещь, для которой, как мне кажется, у нас нет хороших теорий? Как количественно оценить, сколько выразительной силы нужно, чтобы выразить вопрос? Часто в математике самое трудное — правильно сформулировать определение, но что, если само определение становится настолько сложным и непроверяемым, что никто не может соотнести его с чем-либо? Что ж, похоже, что многие интересные давние математические проблемы имеют "относительно" простые постановки, так что их можно легко формализовать в Lean, но не уверен, есть ли на самом деле серебряная пуля с Lean или это будут черепахи до самого низа.
Вероятно, это не имеет значения, пока ИИ продолжает взлетать […]
- dooglius
Учитывая высокоуровневое описание примеров, я думаю, это меньше похоже на "неверный перевод", а скорее на то, что LLM подправляет доказательство по мере его формализации. Переход между m+4 и m+5 — это совсем другое дело, нежели те неоднозначности, которые обычно возникают при разборе математических утверждений на естественном языке.
- Sniffnoy
Хм, просматривая это, я не вижу, где они указывают, что именно OpenAI на самом деле доказал вместо взрыва Навье-Стокса с вынуждающей силой. Я вижу, где они делают это для некоторых других конкретных утверждений, использованных по ходу, но не для главного результата.