Эпоха завышенных ожиданий от логических способностей ИИ подходит к концу. Исследователи переводят оценку моделей на стандарт Hard Mode («сложный режим»), отказываясь от «подсказок», которые ранее были скрыты прямо в условиях задач. Согласно отчету о системе Discover And Prove (DAP), современные большие языковые модели (LLM) научились виртуозно имитировать интеллект: они угадывают верный ответ в 80% случаев, но когда дело доходит до формального доказательства на языке Lean 4, справляются менее чем в 10% ситуаций. На наш взгляд, это наглядная иллюстрация пропасти между интуицией и подлинной логикой.
Пока модели просто «галлюцинируют в правильном направлении», они бесполезны для верификации критически важного ПО или инженерных систем. Чтобы устранить этот разрыв, разработчики представили DAP — агентный фреймворк, который заменяет встроенные подсказки процессом осознанного рассуждения. Как указано в препринте на arXiv, система сначала формулирует гипотезу на естественном языке, проводит рефлексию и только после этого транслирует выводы в формальный код для автоматических доказателей.
Результаты такой «шоковой терапии» для алгоритмов уже заметны в бенчмарках. DAP стал первым фреймворком, решившим 36 теорем из набора PutnamBench в режиме Hard Mode. В тесте CombiBench система установила новый мировой рекорд (SOTA), подняв планку с 7 до 10 решенных задач при метрике Pass@16. Чтобы держать индустрию в тонусе, авторы также выпустили MiniF2F-Hard и FIMO-Hard — пересмотренные базы данных, из которых удалены все вспомогательные «костыли».
Для технических директоров и архитекторов программного обеспечения это важный сигнал: надежная верификация сегодня невозможна через простой цикл «промпт — ответ». Необходимы многошаговые агентные рабочие процессы. Если ваш ИИ не способен решать задачи в режиме Hard Mode, его хваленая логика — не более чем иллюзия, порожденная обучающей выборкой. Использовать такой инструмент в реальном производстве попросту опасно.