ByteDance представляет Seed-Prover: прорыв в автоматическом доказательстве математических теорем

Прогресс в математическом рассуждении с LLM

Большие языковые модели (LLM) значительно улучшили математическое рассуждение, используя естественный язык, что повысило результаты на таких бенчмарках, как MATH и AIME. Однако обучение с подкреплением (RL) сталкивается с проблемами, так как проверка доказательств на естественном языке требует тщательной ручной проверки, что ограничивает применение RL для обучения моделей доказательства теорем.

Seed-Prover: доказательство с использованием лемм

Команда ByteDance Seed представила Seed-Prover — систему доказательства, основанную на леммах, которая итеративно улучшает доказательства с помощью обратной связи из Lean, ранее доказанных лемм и самосуммирования. В отличие от традиционных методов пошагового или полного доказательства, Seed-Prover сосредоточен на леммах, что позволяет применять глубокие и широкие методы вывода для решения сложных задач, включая задачи Международной математической олимпиады (IMO).

Решение ограничений с помощью Seed-Geometry

В дополнение к Seed-Prover представлен Seed-Geometry — движок геометрического рассуждения, который устраняет ограничения Lean в поддержке геометрии, что расширяет возможности системы для работы с геометрическими задачами.

Методика обучения и набор данных

Seed-Prover использует многоступенчатое и многозадачное обучение с подкреплением на основе VAPO для взаимодействия с Lean. Обучающий набор данных объединяет открытые и внутренние формальные задачи, при этом генератор создает упрощенные варианты сложных задач, исключая слишком простые с высоким уровнем доказательств. Бэкенд Seed-Geometry поддерживает масштабную генерацию задач, выявив более 230 миллионов уникальных задач за неделю и повысив эффективность поиска в восемь раз.

Результаты на различных бенчмарках

Seed-Prover демонстрирует передовые результаты:

IMO 2025: полностью решены 5 из 6 задач; Seed-Geometry мгновенно решил задачу 2; комбинированные методы доказали оставшуюся задачу.
Прошлые задачи IMO: решено 121 из 155 задач с успехом 78,1% по всем уровням сложности.
MiniF2F: достигнута 99,6% успешность доказательств на валидации и тестах, решая сложные задачи, например IMO 1990 P3.
PutnamBench: улучшение с 201 до 331 решенной задачи из 657 при переходе на средние настройки вывода.
CombiBench: решено 30 из 100 комбинаторных задач, превосходя существующие методы, но показывая сложности в комбинаторных рассуждениях.
MiniCTX-v2: достигнуто 81,8% успеха, значительно превосходя базовые методы.

Перспективы развития

Интеграция формальных языков, таких как Lean, с возможностями LLM обеспечивает быструю, экономичную и надежную проверку доказательств по сравнению с экспертами и оценщиками на основе LLM. В будущем планируется объединить формальные системы и LLM для решения открытых математических гипотез.

Для дополнительной информации посетите статью и GitHub с учебными материалами, кодами и ноутбуками. Следите за командой в Twitter и присоединяйтесь к их сообществу ML для обновлений.