Системы на базе больших языковых моделей (LLMs) продемонстрировали заметные улучшения в математическом мышлении благодаря работе с естественным языком. Это привело к повышению производительности по таким бенчмаркам, как MATH и AIME. Однако при обучении этих моделей с помощью подкрепляющего обучения (RL) возникает проблема: проверка правильности доказательств на естественном языке очень сложна. Требуется тщательная ручная проверка каждого шага рассуждения. Это ограничивает применение RL для обучения моделей доказательства математических теорем.
Хотя формальные языки, такие как Lean, предлагают автоматическую проверку правильности, текущие формальные доказывающие системы LLM сталкиваются с ограничениями. Доказывающие системы пошагового уровня генерируют код постепенно, но требуют специальных лесов и не обладают возможностями высокоуровневого рассуждения.
Команда ByteDance Seed представляет Seed-Prover — модель рассуждений в стиле лемм для доказательства всего доказательства. Она уточняет доказательства итеративно, используя обратную связь Lean, ранее установленные леммы и самосуммирование.
Seed-Prover использует три специализированные стратегии логического вывода во время тестирования, которые позволяют применять глубокие и широкие методы рассуждения для решения конкурсных задач уровня Международной математической олимпиады (IMO). Основное нововведение заключается в том, что в качестве основного метода используется доказательство в стиле лемм, при этом леммы ставятся в центр процесса рассуждения, а не полагаются на традиционные пошаговые методы или методы генерации доказательств всего доказательства.
Кроме того, в этой статье представлена Seed-Geometry — дополнительный механизм геометрических рассуждений, который преодолевает ограничения Lean в обработке геометрической поддержки.
Для взаимодействия между Seed-Prover и Lean используется многоэтапное, многозадачное RL на основе VAPO. Набор данных для обучения объединяет открытые наборы данных с внутренними формальными задачами, используя предлагающий механизм для создания более простых вариантов сложных задач. Он исключает чрезмерно простые задачи с уровнем доказанности выше 25%.
Seed-Geometry поддерживает генерацию крупномасштабных задач, выявляя более 230 миллионов уникальных задач за семь дней с восьмикратным повышением эффективности поиска.
Seed-Prover достигает передовых результатов по множеству математических тестов. На IMO 2025 Seed-Prover полностью решает 5 из 6 задач, причём Seed-Geometry мгновенно решает задачу 2, а Seed-Prover выводит доказательства для оставшейся задачи, используя различные настройки логического вывода.
На прошлых задачах IMO было доказано 121 из 155 задач, что составляет 78,1% успешных решений на всех уровнях сложности.
В заключение ByteDance Seed представляет Seed-Geometry и Seed-Prover — два метода формальных рассуждений, которые объединяют возможности LLM. Seed-Geometry обеспечивает ускоренную проверку и расширенные механизмы поиска, в то время как Seed-Prover использует итеративное уточнение и сложные стратегии логического вывода во время тестирования.
Решение 5 из 6 задач на IMO 2025 показывает практическую эффективность этих методов в решении элитных математических соревнований. Использование формальных языков, таких как Lean, обеспечивает быструю проверку доказательств, которая более рентабельна, чем работа экспертов-людей, и более надёжна, чем судьи на базе LLM.
Будущие исследования будут сосредоточены на сочетании формальных систем с LLM для решения открытых гипотез.
Ознакомиться с подробностями можно в статье и на странице проекта на GitHub. На нашей странице GitHub вы найдёте учебные пособия, коды и блокноты. Подписывайтесь на нас в Twitter, присоединяйтесь к нашему сообществу в ML SubReddit (более 100 тысяч участников) и подписывайтесь на нашу рассылку.
1. Какие проблемы существуют при обучении больших языковых моделей (LLMs) с помощью подкрепляющего обучения (RL) для доказательства математических теорем?
Ответ: при обучении LLMs с помощью RL для доказательства математических теорем существует проблема проверки правильности доказательств на естественном языке. Ручная проверка каждого шага рассуждения требует значительных усилий и времени, что ограничивает применение RL для обучения моделей доказательства математических теорем.
2. Какие стратегии логического вывода использует Seed-Prover во время тестирования?
Ответ: Seed-Prover использует три специализированные стратегии логического вывода во время тестирования, которые позволяют применять глубокие и широкие методы рассуждения для решения конкурсных задач уровня Международной математической олимпиады (IMO). Основное нововведение заключается в том, что в качестве основного метода используется доказательство в стиле лемм, при этом леммы ставятся в центр процесса рассуждения.
3. Какие преимущества предоставляет Seed-Geometry по сравнению с традиционными методами доказательства математических теорем?
Ответ: Seed-Geometry — дополнительный механизм геометрических рассуждений, который преодолевает ограничения Lean в обработке геометрической поддержки. Он поддерживает генерацию крупномасштабных задач, выявляя более 230 миллионов уникальных задач за семь дней с восьмикратным повышением эффективности поиска.
4. Какие результаты показал Seed-Prover на Международной математической олимпиаде (IMO) 2025?
Ответ: на IMO 2025 Seed-Prover полностью решает 5 из 6 задач. Seed-Geometry мгновенно решает задачу 2, а Seed-Prover выводит доказательства для оставшейся задачи, используя различные настройки логического вывода. Это показывает практическую эффективность этих методов в решении элитных математических соревнований.
5. Какие перспективы развития методов формальных рассуждений, представленных в статье?
Ответ: будущие исследования будут сосредоточены на сочетании формальных систем с LLM для решения открытых гипотез. Это позволит расширить возможности LLM в области доказательства математических теорем и решения сложных математических задач.