OpenAI неправильно переводит математику в код для своего доказательства навиг-стокс

Похоже, что OpenAI совершила незначительную ошибку при публикации доказательств проблемы Навьер-Стокс, как утверждает группа математиков. Ошибка не означает, что доказательства являются неправильными или что OpenAI правильно не разрешила проблему, но она ставит под сомнение возможность всегда полагаться на математические результаты, полученные с помощью моделей AI. ▪ Что необходимо сделать со всеми этими большими языковыми доказательствами, созданными моделью, это то, что они должны быть зачитаны людьми и это создает огромное дополнительное бремя для математиков, — говорит Андерс Хансен в Кембриджском университете. 8 сентября OpenAI объявила, что нашла решение проблемы Навьер-Стокс — одной из самых известных открытых проблем в математике. Она опубликовала доказательство в двух вариантах – одно написано на языке естественного, что означает комбинацию английских и математических символов, как пишется математик человеком, а другое — компьютерный код Lean. Доказательство леан предназначено для формализации естественной версии, что позволяет компьютеру механически проверять правдивость всех его логических заявлений. Проблема в том, скажем Хансен и его команда, что они не совпадают. Реклама . Этот процесс формализации пытается заменить коллегиальный обзор, — говорит член команды Фабиан Цирселли также в Кембриджском университете. — Рецензия Пира означает, что человеческие глаза смотрят на доказательства. Но в этом документе мы показали, что использование такого типа AI…