Post #22

⚙️ Lean 4 × LLM: первые шаги к «логически-оснащённым» моделям В свежем препринте исследователи показали интересную связку: берут привычную LLM, добавляют к ней Lean 4 — формальный доказатель, где каждое утверждение компилируется как строгий тип — и заставляют модель решать олимпиадную математику под надзором компилятора. Результат: точность на бенчмарке MATH выросла почти на 5 пунктов. Не потому, что модель стала «умнее», а потому что Lean отсекает всё, что логически не проходит. Это важный этап, потому что LLM-ы сильны в вероятностных догадках, но с формальной логикой у них беда: аргумент может звучать убедительно, но быть дырявым. Добавив Lean как внешний «слой проверки», мы даём модели то, чего ей хронически не хватало — жёсткое правило истинности. Как устроен гибрид 1. Формализация. Текст задачи превращают в теорему Lean. 2. Генерация. Модель предлагает шаги доказательства. 3. Проверка. Lean компилирует: прошёл — принято, нет — ищем другой путь. Это, по сути, первый зримый шаг к тому, чтобы языковые модели играли не только «на ощущениях», а с опорой на формальную базу. Если идея приживётся, гибридный подход может закрыть разрыв между ИИ и человеком в тех областях, где пока выигрывает строгая логика: проверка научных выкладок, сложные инженерные расчёты, критически важный код. Ну и понятно, что это пока только препринт, но направление мысли интересное. Похоже, дальше интереснее: вместо наращивания миллиардов параметров мы начнём окутывать модели цепочками проверяемых правил. А значит — меньше «магии вероятностей», больше гарантированной корректности. Источник: https://arxiv.org/abs/2505.23703