Новая архитектура для ATP
Команда Matěj Kripner и Milan Straka представила OpenProver, систему автоматического доказательства теорем (ATP), работающую на базе больших языковых моделей. В отличие от простых генераторов, OpenProver использует архитектуру Planner-Worker-Verifier, вдохновленную системой Aletheia. Эта структура позволяет декомпозировать сложные математические задачи на параллельные задачи, решаемые агентами-рабочими (Workers).
Whiteboard и Repository
Ключевая особенность системы — управление контекстом через два компонента:
- Whiteboard (Доска): компактный блок заметок, поддерживаемый агентом-планировщиком (Planner).
- Repository (Репозиторий): неограниченное хранилище промежуточных результатов, позволяющее накапливать знания в процессе поиска доказательства.
Интерактивный режим и верификация
OpenProver полностью открыт и поддерживает автоматическую формальную верификацию сгенерированных доказательств через Lean 4. Система предлагает интерактивный терминальный интерфейс, позволяющий человеку контролировать и направлять процесс поиска, что усиливает синергию «человек-ИИ».
Результаты на ProofNet
Авторы провели количественные эксперименты на датасете ProofNet, сравнив OpenProver с простым базовым подходом. Использование формальной верификации позволило провести точные ablation-эксперименты, подтвердив эффективность предложенной архитектуры.
| Характеристика | OpenProver | Базовый подход (Baseline) |
|---|---|---|
| Архитектура | Planner-Worker-Verifier | Прямая генерация |
| Lean 4 (автоматическая) | Отсутствует/Ручная | |
| Интерактивность | Да (терминал) | Нет |
| Датасет для оценки | ProofNet | ProofNet |
Работа принята к публикации на конференции CICM 2026 (19th Conference on Intelligent Computer Mathematics). Исходный код системы доступен в открытом доступе.
Источник: arXiv cs.AI ↗