Синергия LLM и символьной математики
Исследователи представили IneqAgent — фреймворк, решающий проблему формального доказательства неравенств в системе Lean4. Ключевая инновация заключается в интеграции рассуждений больших языковых моделей (LLM) с точными символьными вычислениями. Архитектура использует Monte Carlo Tree Search (MCTS) на уровне лемм для координации построения лемм, реформирования целей и выбора символьного бэкенда.
Система опирается на три основных бэкенда для генерации точных сертификатов: сумма квадратов (sum-of-squares), многочлены Бернштейна и последовательная подстановка разностей. Это позволяет агенту не только генерировать шаги, но и верифицировать их через обратную связь от Lean, создавая полные доказательства.
Результаты на бенчмарках
IneqAgent продемонстрировал выдающиеся результаты при использовании модели DeepSeek-V4-Flash. Система успешно решила 175 из 186 задач, что составляет 94.09% успеха. Это лучший показатель среди всех протестированных методов. Кроме того, агент показал более высокую эффективность при низких порогах стоимости инференса по сравнению с Direct Agent.
| Метрика / Показатель | Значение / Результат |
|---|---|
| Базовая модель | DeepSeek-V4-Flash |
| Всего задач | 186 |
| Решено задач | 175 |
| Успешность (Success Rate) | 94.09% |
| Сравнение с Direct Agent | Выше успешность при той же стоимости инференса |
Научные достижения: подтверждение гипотез
Помимо статистических метрик, IneqAgent позволил получить новые математические результаты, верифицированные в Lean. Исследователи получили формально подтвержденные усиления конъектуры Диттерта (Dittert's conjecture) для размерностей четыре и пять. Также была сертифицирована неравенство Холенса-Джокоровича (Holens--Djokovic) для случая (4,4), что влечет за собой подтверждение конъектуры Мерриса (Merris's conjecture) в размерности четыре.
Значение для AI и математики
Работа демонстрирует переход от «генерации текста» к «генерации верифицируемых доказательств». Использование символьных бэкендов снижает вероятность галлюцинаций LLM, характерных для сложных математических задач. Это открывает путь к автоматизации исследований в области алгебры и анализа, где точность вычислений критична.
Источник: arXiv cs.AI ↗