LLM в решении сложных задач: математика, логика и RL

О чем этот урок:

Это финальный урок нашего курса, и в нем мы подводим важный итог: мы отходим от классической генерации текстов и смотрим на LLM как на системы символьных вычислений и решения сложных задач. Исторически математика и строгая логика давались языковым моделям тяжело из-за токенизации чисел и стохастической природы генерации. Но с появлением огромных моделей, специализированных наборов данных и новых алгоритмов обучения эта преграда была прорвана.

В этом уроке мы совершим краткий экскурс в историю того, как модели учились считать (от Minerva до современных Qwen Math и DeepSeek Math). Затем мы сфокусируемся на текущих трендах: почему интернет-данные закончились, зачем нужны миллионы сгенерированных синтетических примеров и почему будущее за обучением с подкреплением (RL) при поиске оптимальных деревьев рассуждений. Мы также затронем инженерные проблемы: как заставить модель проверять саму себя и почему даже самая умная нейросеть может упасть на простой задачке про гнилые яблоки.

Основные темы и рассматриваемые вопросы:

• Фундаментальные проблемы LLM с математикой: как ошибки ранних токенизаторов мешали моделям понимать числа и почему стохастическое сэмплирование вредит строгим научным рассуждениям.

• Историческая эволюция LLM для науки:

  • Minerva (Google): первый успех на 540B параметров и почему нотация LaTeX оказалась критически важной.

  • Galactica (Meta): попытка создать научную Википедию за счет глубокой чистки датасетов.

• Использование внешних инструментов (Tools): как модели Microsoft (ToRA) научились писать и запускать код Python для выполнения вычислений, обходя свои слабые стороны в арифметике.

• Синтетические данные: почему все разработчики перешли на генерацию математических датасетов и как QwenMath выиграла гонку благодаря триллионам синтетических токенов.

• Обучение с подкреплением (RL) в задачах рассуждения:

  • Сложность оценки длинного ответа: зачем нужны Process Reward Models (модели оценки процесса), которые проверяют каждый шаг, а не только первый ответ.

  • Методы поиска по дереву (Monte Carlo Tree Search) при генерации ответа.

  • Системы автоматического доказательства теорем (Lean) и как они используются для формальной верификации LLM.

• Масштабирование во время инференса (Time Scaling): концепция моделей OpenAI o1/o3 и DeepSeek R1 — почему долгие размышления («цепочки рассуждений») на этапе ответа пользователю дают скачок качества на PhD-задачах.

• Инженерная боль при обучении RL: как ненормализованные запятые в числах или лишние пробелы ломают верификаторы и почему чистота данных определяет успех обучения модели.