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