BFS-Prover

ByteDance Doubao (Seed) открыла BFS-Prover 25 февраля 2025 года. Это не универсальный чат-бот, а исследовательская система автоматического доказательства теорем: языковая модель предлагает шаги формального доказательства, а система поиска и Lean 4 проверяют, принимаются ли эти шаги формальным помощником доказательств.

Формальные доказательства

Каждый шаг проверяется Lean 4

Задача системы — переводить математическое утверждение и ход решения в формальный код. Компилятор Lean проверяет корректность каждого шага, поэтому оценка доказательства отличается от субъективного качества обычного текстового ответа. Такой подход полезен для исследовательских задач, где важна формальная проверка, но требует знаний языка Lean и инструментов доказательства.

Best-First Search

Поиск продолжает наиболее перспективную ветвь

Вместо более сложных схем на основе Monte Carlo Tree Search команда использовала оптимизированный поиск по приоритету. BFS-Prover сочетает языковую модель, выбор тактик, оценку промежуточных состояний и обратную связь Lean. Дополнительно применяются итеративное обучение и отбор задач, чтобы сосредоточивать обучение на теоремах, которые не решаются простым поиском.

Результат MiniF2F

Заявленный авторами показатель — 72,95%

В сообщении ByteDance указано, что BFS-Prover набрала 72,95% на тестовой части MiniF2F. Это показатель конкретной версии и экспериментальных вычислительных условий разработчика; он не означает, что система доказывает произвольные математические утверждения или заменяет экспертную проверку постановки задачи.

Открытая модель и применение

Для исследовательской среды, а не бытового чата

ByteDance опубликовала техническую статью и веса актуальной карточки ByteDance-Seed/BFS-Prover-V1-7B. Чтобы повторить эксперимент, потребуется поддерживаемая версия модели, среда Lean 4 и ресурсы для поиска. Точная конфигурация и лицензия доступны в карточке репозитория; открытая модель предназначена прежде всего для исследований формальных методов и автоматического доказательства.

Связанные модели и разработчик

Другие публикации команды ByteDance Seed

Seed Prover 1.5 · Seed-Thinking-v1.5 · Seed1.6 Thinking · Seed-OSS · ByteDance Seed в Вики Futuretools

Первичные источники

Анонсы, карточки и репозитории разработчика

анонс открытой системы BFS-Prover · техническая статья BFS-Prover · актуальная карточка открытой модели BFS-Prover