Компания OpenAI сообщила изданию New Scientist , что ей известно о несоответствии между...
Компания OpenAI сообщила изданию New Scientist , что ей известно о несоответствии между доказательством на естественном языке и кодом Lean, и это не означает, что какое-либо из доказательств является недействительным. Компания заявляет, что исправит любые ошибки в доказательстве на естественном языке по мере их обнаружения, а также продолжит процесс формализации 722 математических статей, опубликованных компанией на этой неделе , лишь некоторые из которых сопровождаются доказательствами Lean, которые сами по себе не были проверены вручную. 🛑 Игла в стопке корректурных образцов Обнаружение расхождения представляло собой несколько сюрреалистический процесс: сначала нужно было попросить ChatGPT найти потенциальные несоответствия между доказательствами, полученными на естественном языке и с помощью Lean-методологии, а затем проверить их вручную. Многие из несоответствий, обнаруженных ChatGPT, при ближайшем рассмотрении оказались вполне обоснованными. «Проверять все это вручную было настоящим кошмаром», — говорит Хансен. В общей сложности команде потребовалось около двух недель, чтобы выявить истинное несоответствие, в то время как, по словам OpenAI, ее агенты потратили 88 часов на создание доказательств. «OpenAI хвастается тем, как быстро им удалось получить этот результат, но это лишь часть процесса», — говорит член команды Александр Бастунис из Королевского колледжа Лондона. Ответ на вопрос о том, могут ли модели ИИ точно автоматически формализовать математические формулы, имеет решающее значение, если математики хотят доверять этим результатам. Андерс и его команда продемонстрировали, что ChatGPT может создать упрощенную версию доказательства, которая не соответствует исходной версии на естественном языке, при этом ИИ незаметно изменяет логическое рассуждение, чтобы скрыть любые ошибки. «Он пытается мне помочь, но, делая это, он не помогает», — говорит Хансен. Если бы это произошло с длинным и сложным доказательством, то заметить это было бы очень сложно без детального изучения обеих версий. Эта проблема стала еще более актуальной из-за партии из 722 статей, недавно опубликованных OpenAI. Если мы думаем: «Все это теперь правда, все, что нам нужно сделать, это прочитать статью», то это опасно, говорит Хансен. «Цель науки состоит в том, чтобы человечество понимало, как устроен мир, чтобы мы могли принимать обоснованные решения. Если мы потеряем это понимание, что мы будем делать?» Кевин Баззард из Имперского колледжа Лондона отмечает, что в подобных дискуссиях важно различать формулировку теоремы и её доказательство. Например, формулировка знаменитой Великой теоремы Ферма гласит, что для положительных целых чисел a , b , c и n , aⁿ + bⁿ = cⁿ только если n равно 1 или 2. Это легко перевести в язык Lean и легко проверить. Если вы уверены в правильности утверждения в Lean и доказательство этого утверждения согласуется с условиями, вы можете быть уверены в истинности доказательства. Проблема, как отметили Хансен и его команда, заключается в том, что это ничего не говорит о версии доказательства на естественном языке, опубликованной в виде PDF-документа. «Я уверен, что проблема Навье-Стокса решена правильно, — говорит Баззард. — Но я гораздо менее уверен в правильности доказательства, описанного в PDF-файле». Хансен говорит, что надеется, что OpenAI отнесется к работе команды «очень серьезно», и что необходимо проделать дополнительную работу по разработке надежных методов автоматической формализации. «Есть ли у нас решение? Пока нет. Возможно ли сделать это контролируемым образом? Да, возможно, но оптимальный и окончательный способ сделать это совершенно неизвестен». Темы: #Математика Автор: Джейкоб Арон