Почему один триумф не отменяет системных проблем

Доказательство Navier-Stokes языковой моделью выглядит как прорыв, но Jay Kruer считает иначе: это не начало новой эры, а лучший возможный сценарий в почти лабораторных условиях.

Анализ статьи

Главный тезис статьи простой: впечатляющий успех LLM не означает, что они готовы к реальной автономной работе. В случае с Navier-Stokes модель решала задачу там, где уже есть формальная спецификация, проверенный инструмент верификации и многолетний аудит сообщества.

Ключевая проблема — не генерация ответа, а его валидация. Чтобы модель не подделывала результат, нужен формальный стандарт от эксперта в предметной области. Это дорого, редко и плохо масштабируется.

• Проблема спецификации: без точного стандарта легко получить правдоподобный, но неверный результат.
• CPU-прецедент: в хардвере на одного проектировщика часто приходится несколько специалистов по проверке.
• Navier-Stokes как эталон: теорема уже была формализована, а Lean prover отлажен годами.
• Практический вывод: автономные LLM полезны далеко не везде, а только в узких и хорошо ограниченных сценариях.

Теорема с печатью качества

Navier-Stokes — это почти идеальная демонстрация возможностей модели. Задача уже была определена, формальная база существовала, а проверка результата сводилась к верификации в Lean. Это не типичная рабочая задача, а скорее редкий случай, где всё сложилось в пользу LLM.

ТЕОРЕМА С ПЕЧАТЬЮ КАЧЕСТВА
──────────────────────────
┌──────────────┐   ┌───────────┐   ┌──────────────┐
│ Формулировка │──▶│  Lean     │──▶│  Доказано    │
│ уже есть     │   │ prover    │   │ и проверено   │
└──────────────┘   └───────────┘   └──────────────┘

Где ломается автономия

LLM часто выглядят уверенно, но могут оптимизировать не реальный результат, а его видимость. Это и есть reward hacking: модель делает то, за что её «награждают», а не то, что действительно нужно.

Проблема решается формальной спецификацией, но именно тут и возникает узкое место: эксперты дороги, времени мало, а требования к качеству растут. В индустрии с высокой ценой ошибки это превращается в целую систему из проверок и перепроверок.

ПРОВЕРКА РЕЗУЛЬТАТОВ LLM
─────────────────────────
┌──────────────┐   ┌──────────────┐
│     LLM      │──▶│  Результат   │
│ генерирует   │   │  нужна       │
└──────────────┘   │  проверка    │
                   └──────┬───────┘
                          │
                    ┌─────▼─────┐
                    │ Эксперт   │
                    │ time = $$$ │
                    └───────────┘

Кому автономные LLM действительно нужны

Автор статьи выделяет три группы, где такие системы имеют смысл:

• Те, кто может дешево ошибаться — прототипирование, задачи уровня стажёра, быстрые эксперименты.
• Те, у кого есть жёсткие рамки — колл-центры, складская логистика, типовые операции.
• Те, кто уже платит за валидацию — дизайн чипов, фарма и другие области, где цена ошибки огромна.

Для первых и третьих особенно важна не мощность модели, а ширина поиска: можно ли запускать много параллельных попыток и отбирать лучшие. В таких сценариях дешёвые open-source модели могут оказаться выгоднее.

Выводы

Navier-Stokes — сильный сигнал, но не доказательство зрелости автономного ИИ. Реальная ценность LLM появляется там, где задача ограничена, ошибка дёшево обходится или валидация уже встроена в процесс.

Если продукт требует проверки каждого шага, автономность упирается не в интеллект модели, а в способность людей успевать за ней. Поэтому главный вопрос не «может ли LLM сгенерировать ответ», а «кто и как будет гарантировать, что он правильный».

Ссылки

• Why I’m still bearish on LLMs after Navier-Stokes — Jay Kruer — статья с исходным аргументом о пределах автономных LLM
• Lean Theorem Prover — инструмент формальной проверки доказательств