Выход за пределы статических задач
Исследователи из Google DeepMind и других лабораторий (Marco Dos Santos, Vivek Veeriah и др.) представили новую агентную пайплайн-систему, способную к автономному математическому открытию. В отличие от предыдущих прорывов ИИ в решении олимпиадных задач или проверке гипотез, эта работа направлена на исследование Busy Beaver (BB) — области, которая фундаментально не вычислима. Поскольку число BB(n) невозможно вычислить для любого n, эта область предоставляет естественную среду для непрерывного исследования через формулирование новых математических conjectures (предположений).
Технологический стек: от паттернов к Lean
Система интегрирует несколько этапов обработки:
- Распознавание паттернов: Анализ выполнения машин Тьюринга.
- Автоматическое конъюрирование: Формулирование гипотез на основе данных.
- Неформальное рассуждение: Использование LLM (на базе Gemini) для построения логических цепочек.
- Формальное доказательство: Верификация результатов в системе Lean.
Результаты: 11 новых «криптовидов»
Автоматизированная система успешно обнаружила и формально верифицировала новые ускорения (accelerations) для 11 машин в классе BB(6). Эти машины были классифицированы как «Криптовиды» (Cryptids) — термин, обозначающий машины, чье выполнение на пустой ленте допускает точное, компактное математическое описание, но вопрос их остановки (halting problem) остается неразрешенным.
| Параметр | Значение / Описание |
|---|---|
| Класс машин | BB(6) (машин Тьюринга с 6 состояниями) |
| Количество открытий | 11 новых ускорений (Collatz-like) |
| Инструмент верификации | Lean (формальная верификация теорем) |
| Статус машин | «Криптовиды» (остановка не доказана, но структура описана) |
| Базовая модель | Google Gemini (агентная пайплайн) |
Значение для науки
Этот результат демонстрирует потенциал автономных ИИ-систем для открытий в фундаментальных областях компьютерных наук, где человеческий интеллект сталкивается с пределами вычислимости. Исследование продвигает анализ «holdout» (недоказанных) случаев в BB(6) и показывает, что ИИ может не просто решать задачи, а формулировать новые вопросы и находить скрытые математические структуры в хаотичных вычислениях.
Источник: arXiv cs.AI ↗