Математики нашли способ приручить LLM через символьную верификацию
Может ли алгоритм, который иногда не может сложить два трехзначных числа, помочь в доказательстве серьезных теорем? Оказывается, может, если приставить к нему строгого надзирателя. Как сообщает издание Let’s Data Science, современные математики начали активно внедрять большие языковые модели в свои рабочие процессы, используя их как генераторы идей, которые затем проверяются «железобетонными» символьными вычислениями.
Суть подхода проста: LLM берет на себя роль креативного ассистента, набрасывающего черновики доказательств и неформальные гипотезы. Но так как доверять нейросетям на слово в математике не стоит, в связку добавляются SAT-солверы и интерактивные доказатели теорем вроде Lean или Coq. Эти инструменты выступают в роли финального арбитра, превращая вероятностные догадки модели в строгие, математически верифицированные факты.
Но действительно ли это шаг к автоматизации интеллекта или просто очень дорогой калькулятор для гипотез? Исследователи, среди которых выделяется Марейн Хёле, превращают сложные математические утверждения в задачи на удовлетворение ограничений. Это похоже на то, как мы в разработке пишем тесты: LLM генерирует код на формальном языке, а бэкенд-система (в данном случае логический движок) проверяет его на соответствие правилам системы. Если «тест» пройден, у математика на руках оказывается сертификат истинности, который невозможно оспорить.
Техническая связка: от галлюцинаций к формальному коду
Почему нельзя просто спросить у ChatGPT доказательство гипотезы Римана? Проблема в «хрупкости» внутреннего рассуждения нейросетей — они отлично распознают паттерны, но часто «галлюцинируют», выдавая желаемое за действительное. Чтобы обойти это, инженеры обучают модели переводить естественный язык математики в формальный код. Это напоминает работу транспайлера, где на входе у нас расплывчатые мысли человека, а на выходе — строгий синтаксис, понятный машине.
В этой схеме человек остается в контуре управления (human-in-the-loop), выполняя роль архитектора. Мы используем few-shot и chain-of-thought промптинг, чтобы заставить модель рассуждать пошагово. Каждая лемма или конструкция, предложенная ИИ, рассматривается лишь как предположение, пока она не будет прогнана через оптимизированные пайплайны верификации. Это избавляет от необходимости проверять тысячи страниц выкладок вручную, делегируя рутину алгоритмам.
Пока LLM не научатся понимать семантическую глубину объектов за пределами статистических корреляций, они останутся продвинутыми интерфейсами к классическим солверам. Стратегически мы рискуем получить гору доказанных, но абсолютно нечитаемых для человека теорем, превращая математику в кладбище формальных сертификатов без искры понимания.
Для индустрии это означает смену парадигмы. Разработчикам и ML-инженерам теперь нужно строить мосты между вероятностными и символьными системами. Это не просто вопрос обучения очередной модели, а задача проектирования тулчейнов, которые умеют эффективно «скармливать» вывод нейросети в верификаторы. (Кстати, создание качественных датасетов, где неформальные рассуждения сопоставлены с формальным кодом — это сейчас золотая жила для R&D отделов).
Но не ведет ли это к деградации самого исследователя? Математики старой закалки опасаются потери прямого контакта с объектом изучения. Тем не менее, текущий тренд показывает, что гибридные системы скорее усиливают интуицию, позволяя быстро отсеивать тупиковые пути. В конечном счете, цель не в том, чтобы заменить человека, а в том, чтобы сделать его «быстрее» в мире, где объем данных и сложность структур давно переросли возможности биологического мозга.
