Эра больших языковых моделей (LLM) в роли послушных «решателей» типовых математических задач упирается в потолок. Исследователи из Калифорнийского университета в Лос-Анджелесе (UCLA) и Ливерморской национальной лаборатории (LLNL) констатируют: пока DeepSeek-R1 и модели серии o1 демонстрируют чудеса на олимпиадных бенчмарках, они остаются заложниками обучающей выборки. Настоящий вызов — Research Frontier, передний край науки, где нет готовых ответов. Эрик Цзян и Сяо Лян в своем программном документе подчеркивают, что переход к статусу полноценного научного агента невозможен без жесткого логического фундамента.
Предохранитель от галлюцинаций: интерактивное доказательство
Чтобы ИИ перестал быть дорогой игрушкой, генерирующей правдоподобный бред, индустрии придется внедрять языки интерактивного доказательства теорем (ITP). В отличие от размытого естественного языка, ITP обладают проверяемой семантикой. Это идеальный фильтр: если модель не может формализовать свою логику, ее «рассуждения» остаются лишь статистической догадкой. Математика в данном случае выступает не просто как дисциплина, а как полигон для обкатки чистого мышления (Reasoning), где любая ошибка ведет к отказу системы принимать доказательство.
Современные системы фундаментально ограничены в работе с фронтирной математикой: они пасуют перед открытыми гипотезами, требующими многоуровневой абстракции и подлинной новизны, а не просто перебора знакомых паттернов.
Человек и ИИ на границе неизведанного
Переход от «решателя» к «исследователю» означает смену парадигмы: от работы с четко сформулированными вопросами к поиску в условиях неопределенности. Тот факт, что в исследованиях группы участвует Терренс Тао, — важнейший индикатор для рынка. Это больше не попытка научить чат-бота помогать студентам с домашней работой; это заявка на создание соавтора научных открытий. Участие математика такого калибра подтверждает: LLM начинают воспринимать как серьезный инструмент для верификации новых истин.
Для руководителей R&D и технический директоров это четкий сигнал: метрики «интеллекта» смещаются от баллов в тестах к способности модели работать в связке с формальными методами. Основная ценность теперь не в том, сколько задач из учебника решит модель, а в том, способна ли она выдать проверяемое доказательство там, где человеческая интуиция заходит в тупик. Пока системы ограничены стоимостью формализации и дефицитом «интуитивных прыжков», но вектор задан: будущее AI — в доказательной строгости, а не в имитации человеческой речи.