Ученые не оценили открытия ChatGPT в математике
Ученые не оценили открытия ChatGPT в математике В OpenAI недавно отчитались об очередном триумфе: их новые модели научились решать сложнейшие математические задачи, над которыми думали столетия. И формально решения подтверждаются через специализированный язык Lean. Кажется, это прорыв, но в сообществе математиков возникло раздражение, о чем пишет TechCrunch. И на то есть причины. Как ChatGPT решает задачи Процесс сложный, требует мощности и время на вывод правильного ответа. Сначала ИИ начинает рассуждать и проверяет гипотезы, сопоставляет их и ищет пути решения. Система формулирует доказательство через Lean, то есть, в виде кода. Причем этот код исключает ошибки и отражает правильный результат. Программа-компилятор Lean прогоняет код через набор базовых математических аксиом. Если в логике есть хоть малейший изъян, система выдает ошибку, и модель уходит переписывать код. Что не нравится математикам На бумаге схема ИИ выглядит красиво: модель пишет решение задачи простым человеческим языком, а затем переводит его в строгий код на языке Lean, чтобы компьютер мог математически проверить каждую строчку. Но научное сообщество отмечает, что решения не соответствуют стандартам и модели все равно что-то додумывает. В доказательствах есть разрыв между кодом и логикой. Lean может и четко структурирован и кажется правильным, но при этом все равно может быть набором галлюцинаций. Тогда все решение ставится под сомнение. «В отношении работ, которые непонятны людям, математики предложили формализовать доказательства — однако лишь 42% доказательств, опубликованных OpenAI, не прошли эту процедуру». Другой вопрос, а как именно ИИ приходит к решению. Опять же, в коде все прописано, но чем модели руководствуются? Какими путями они идут к итогу? Учитывая, что разработчики все хуже начинают контролировать нейросети, проблема рискует стать критической — ведь под сомнение ставится вся цепочка рассуждений при решении. Есть еще подводный камень Научное сообщество крайне консервативно. Оно столетиями вырабатывало принципы и алгоритм доказательств теорем, поэтому любое расхождение с их установками как минимум противоречиво, а то и вовсе фатально. Вспомните, как в школе на уроках физики, химии и геометрии всегда ставили четкий шаблон решения примеров. Если ему не соответствовать, оценка сразу снижалась. Соответственно, насколько ИИ корректен и предлагает верные результаты — открытый вопрос. Математики призывают перепроверять решения и все же не принижать роль человека. «Эти расхождения (в доказательстве теорем) не обязательно опровергают ни одно из решений, но они поднимают вопросы о том, можем ли мы просто полагаться на модели в формализации собственных решений без участия человека». Фото: Unsplash / Crissy Jarvis