Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Автоматический доказатель научился соединять рассуждения LLM с точными алгебраическими проверками и выдавать завершённые доказательства для Lean 4. Хотя препринт не рецензирован и числа в нём получили сами авторы, IneqAgent с DeepSeek-V4-Flash решил 175 из 186 задач. Работа предлагает практическую схему для систем, где модель должна не просто предложить ответ, а довести его до машинно проверяемого результата.
Как агент превращает неравенство в проверяемое доказательство
IneqAgent получает формулировку теоремы на Lean и приводит цель к стандартному виду. Затем агент проверяет, подходит ли текущее выражение для точного символического метода. Если подходит, задачу сразу передают вычислительному модулю; если нет, LLM предлагает промежуточную лемму, замену переменных или другую форму цели.
Поиск идёт на уровне лемм с помощью поиска Монте-Карло по дереву. Узел дерева хранит текущие предпосылки, цель и состояние доказательства. При расширении узла модель предлагает следующий содержательный шаг, а Lean сразу определяет, закрывает ли он цель, оставляет новые подцели или содержит ошибку.
Агент оценивает открытые ветви по двум сигналам. Lean показывает, какие обязательства уже закрыты и принял ли проверяющий ядро добавленный фрагмент. LLM сравнивает новое состояние с предыдущим и оценивает, приблизило ли преобразование доказательство к завершению. Поиск возвращается к ветвям с более высокой оценкой, но продолжает создавать альтернативы у корня.
Для полиномиальных целей предусмотрены три дополняющих друг друга метода. Представление через суммы квадратов подходит для неравенств с полиномиальными ограничениями. Представление Bernstein работает на ограниченных прямоугольных областях и при необходимости делит их на меньшие части. Последовательная замена разностями обрабатывает полиномы над неотрицательными переменными.
Численный решатель может сначала найти приближённый сертификат, но такой результат не попадает в доказательство напрямую. Система восстанавливает рациональные коэффициенты, точно проверяет полиномиальные тождества и только затем создаёт локальный фрагмент Lean. Ядро Lean принимает итоговое доказательство исходной теоремы без незакрытых допущений.
Проверка охватила четыре набора неравенств и несколько LLM, а на каждую обычную задачу действовал двухчасовой лимит. Отдельно систему применили к исследовательским задачам о перманентах матриц; эти случаи не входили в основной набор и не подчинялись тому же лимиту.
Символические модули повысили долю дешёвых решений
С DeepSeek-V4-Flash полная конфигурация решила 175 из 186 задач. При лимите в 5 центов на обращения к LLM доля решений составила 88,17% против 66,67% у Direct Agent с той же моделью. На малом бюджете IneqAgent опередил прямого агента со всеми проверенными моделями.
При более высоких бюджетах преимущество оказалось не универсальным: с некоторыми моделями Direct Agent решал столько же задач или больше. Однако IneqAgent во всех сравнениях тратил меньше средств на LLM в среднем по собственным успешным запускам. Эти средние нельзя считать сравнением на полностью одинаковом наборе примеров, поскольку каждый метод мог справиться с разными задачами.
Удаление поиска по дереву или символических вычислений ухудшало итог. Каждый компонент отдельно помогал базовому агенту, но наибольшую долю решений дала их совместная работа. Полная система также показала минимальные средние затраты на LLM и минимальное время среди проверенных вариантов.
На задачах о перманентах система построила проверенные Lean усиления гипотезы Dittert и точный сертификат для неравенства Holens–Djokovic. Последний результат позволил вывести частный случай гипотезы Merris. Здесь существенен не только найденный ответ: длинное алгебраическое вычисление осталось за символическим модулем, а LLM связала сертификат с исходной формулировкой.
Архитектура полезнее замены одной LLM на другую
Работа меняет планы команд, которые строят агентов для формальной математики или других задач с точным проверяющим модулем. Вместо цикла «модель пишет доказательство — Lean возвращает ошибку» можно выделить отдельный слой маршрутизации: LLM строит промежуточные цели, специализированные решатели закрывают подходящие фрагменты, а проверяющее ядро остаётся окончательной границей доверия.
Такая схема снижает зависимость от способности модели выполнить длинное вычисление без ошибки. Она также позволяет менять базовую LLM отдельно от символических модулей: в работе один и тот же агентный контур запускали с несколькими моделями, не переписывая математические решатели.
Переносить результат на произвольные доказательства пока нельзя. Символическая часть ориентирована на полиномиальную неотрицательность и требует подходящей формы цели; выражения с корнями, логарифмами или другими функциями сначала приходится сводить к поддерживаемым леммам. Эксперименты показывают результат на неравенствах, а не на всём спектре задач Lean.
Для прикладной команды отсюда следует архитектурное решение: сначала определить классы подзадач, для которых существуют точные сертификаты, и только затем добавлять поискового агента. Если продукт не располагает формальным проверяющим модулем или предметным решателем, одни результаты IneqAgent не дают оснований менять стек. Если такие инструменты уже есть, работа показывает, как соединить их с LLM без передачи модели роли последней инстанции.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
