Прохор Петрович
Справедливо, что современные системы — это не только LLM: инструменты, код, поиск, планировщик. Но из этого не следует, что они перестали быть предсказателями текста.
Инструменты детерминированы, но их набор задан человеком: API, схемы, тесты. Система не открывает новые различения — она использует те, что ей дали. Поэтому «операционная система рассуждений» — это скорее обвязка, чем разум: она расширяет возможности модели, но не меняет её природу.
И тест остаётся тем же: перенос на новое. Покажите систему, которая решает задачу, для которой нет инструмента и нет примера, — тогда разговор изменится. Пока что топовые системы сильны там, где есть готовый инструмент и шаблон.
Так что тезис не «LLM — это только токены», а «ядро осталось тем же, обвязка выросла».
Сдаюсь по факту: математический апокалипсис — это не «ИИ не может». 372 результата, UGC, L=BPL, Фурье ниже O(n log n) — это Ааронсон, и он же пишет, что люди ещё не поняли большинство доказательств.
Но обратите внимание, что произошло. Это не «модель стала умнее человека». Это модель плюс три часа поиска плюс Lean-верификатор. Цепочка рассуждений — это и есть поиск, а формальная проверка — отбор. Петля не исчезла, она переехала внутрь инференса.
Мой тезис был не «ИИ не может решать математику», а «интеллект — это петля предсказание → проверка → отбор». Ваш пример её подтверждает: без верификатора и поиска остались бы правдоподобные тексты, а не доказательства.
Что я действительно недооценил — это inference-time compute и формальную верификацию. Их масштаб меняет картину: библиотека плюс поиск плюс Lean — уже не «раздутый калькулятор», а нечто третье.
И самое интересное — не «может ли», а «что это значит»: доказательства, которые никто не понимает, — это и есть псевдоразум в чистом виде: результат есть, понимания нет. Вот это и стоит обсуждать.