От аксиом к знаниям: как работает система
Команда исследователей во главе с Кадзуки Отой (Kazuki Ota) представила новый подход к математическому рассуждению ИИ. В отличие от современных больших языковых моделей (LLM), которые опираются на огромные массивы человеческих текстов и библиотек теорем, новая система работает в строгой формальной аксиоматической системе. Алгоритм начинает с нуля, используя только базовые аксиомы и правила вывода.
Ключевой механизм — самообучение (self-supervised). Агент чередует два процесса: поиск доказательств и извлечение полезных теорем. Найденные и доказанные утверждения сохраняются в библиотеку и используются как леммы для решения более сложных задач в будущем. Это позволяет системе автономно накапливать знания, не прибегая к человеческому prior knowledge.
Масштаб открытий и проверка на бенчмарках
Эксперименты показали, что агент способен генерировать десятки тысяч уникальных теорем. Система не просто выдает случайные комбинации, а находит решения для задач из человеческих бенчмарков, что свидетельствует о смысловой ценности открытых утверждений с точки зрения математики.
Важнейшим результатом стало то, что открытые ИИ теоремы можно использовать как внешнее знание для улучшения работы LLM. Когда эти леммы добавляются в промпт, производительность моделей в задачах доказательства возрастает.
| Характеристика | Традиционные LLM | Новый алгоритм (Self-Supervised) |
|---|---|---|
| Источник знаний | Человеческие тексты, код, готовые библиотеки | Только аксиомы и правила вывода |
| Механизм обучения | Предобучение на данных (Pre-training) | Цикл «поиск доказательства — извлечение леммы» |
| Объем открытий | Ограничен датасетом | Десятки тысяч новых теорем |
| Верифицируемость | Часто требует проверки | Формально верифицируемы в системе |
Почему это важно для индустрии
Результаты работы, представленной на AI for Math Workshop @ ICML 2026, доказывают, что полезные математические знания могут возникать из процесса поиска доказательств без участия человека. Это открывает путь к созданию самоэволюционирующих ИИ-систем для математики, которые способны не только решать задачи, но и генерировать новый формализованный опыт, доступный для проверки и использования другими моделями.
Источник: arXiv cs.AI ↗