Автоматическое доказательство полиномиальных неравенств долгое время остаётся одной из сложных задач математического ИИ. Традиционные символьные методы дают строгие гарантии, но плохо масштабируются из-за быстрого роста промежуточных выражений при увеличении числа переменных или степени. В свою очередь, подходы на основе больших языковых моделей (LLM) показывают прогресс на соревновательных примерах, но не обеспечивают полной автоматизации для сложных случаев.
Группа исследователей предложила NSPI — гибридную нейросимволическую систему, объединяющую сильные стороны LLM и символьных вычислений. На первом этапе LLM выдвигает гипотезу в виде приближённой суммы квадратов (SOS) для целевого многочлена. Затем символьный модуль уточняет это разложение до точного и, если удаётся, получает корректное SOS-представление, которое напрямую доказывает исходное неравенство.
Финальным шагом становится верификация доказательства в системе Lean — формальном языке с машинной проверкой. Таким образом, NSPI предлагает сквозной конвейер от эвристического открытия до сертифицированного доказательства, что повышает надёжность результатов.
Эксперименты на сложных бенчмарках показали, что подход эффективен для многочленов с числом переменных до 10. Это существенное расширение границ применимости по сравнению с чисто символьными или чисто нейросетевыми методами. Разработчики отмечают, что NSPI может быть адаптирован для других задач автоматического математического рассуждения.
Публикация на arXiv вызвала интерес в сообществах символьных вычислений и формальной верификации. Код и тестовые примеры, как ожидается, будут открыты для дальнейшего изучения и воспроизведения результатов.