Математики обнаружили, что текстовое доказательство, опубликованное OpenAI для задачи Навье — Стокса, не полностью совпадает с его компьютерной формализацией на языке Lean. Это не доказывает, что само решение неверно, но ставит вопрос о том, насколько надежно ИИ переводит математические рассуждения в код для автоматической проверки.
Разница оказалась в одном из условий: в текстовом доказательстве определенная величина должна быть меньше m+4m+4m+4, где mmm — целое число, а в версии на Lean указано более слабое ограничение — меньше m+5m+5m+5. Второе условие допускает больше возможных значений, поэтому компьютерная проверка не подтверждает в точности то же утверждение, что изложено в тексте.
Исследователи также нашли другие расхождения между текстом и кодом, в том числе в оценке потока давления. По их мнению, проверка в Lean подтверждает корректность формального утверждения, но сама по себе не гарантирует, что оно соответствует исходному математическому доказательству.
В OpenAI сообщили, что знают о несоответствии. По словам компании, оно не означает автоматически, что одно из доказательств неверно. OpenAI намерена исправлять ошибки в текстовой версии по мере их обнаружения и продолжать формализацию математических работ.
Оптимальный заголовок: Математики нашли расхождения между доказательством OpenAI и его компьютерной проверкой
Читайте также:
Математики не доверяют доказательствам ИИ — нейросети научились обходить компьютерную проверку
25 лауреатов Филдсовской премии предупредили об угрозе ИИ для математики