ИССЛЕДОВАНИЕ · RESEARCH · #2178
Агентный пайплайн на базе Gemini автономно обнаружил и формально проверил в Lean новые ускорения для 11 машин Busy Beaver (BB(6))
В препринте arXiv:2610.22603v1 описан агентный пайплайн на базе Gemini, объединяющий распознавание паттернов, автоматическую генерацию гипотез, неформальное рассуждение и формальное доказательство в Lean для автономного поиска компактных, похожих на Коллатца ускорений шагов исполнения машин Тьюринга. Система нашла и формально проверила новые ускорения для одиннадцати машин BB(6), которые авторы предварительно пометили как «Cryptids» — машины с точными компактными описаниями, но с нерешённым вопросом останова.
КЛЮЧЕВЫЕ ТЕЗИСЫ
- В препринте arXiv:2610.22603v1 описан агентный пайплайн на базе Gemini, объединяющий распознавание паттернов, автоматическую генерацию гипотез, неформальное рассуждение и формальное доказательство в Lean для автономного поиска компактных, похожих на Коллатца ускорений шагов исполнения машин Тьюринга.
- Система нашла и формально проверила новые ускорения для одиннадцати машин BB(6), которые авторы предварительно пометили как «Cryptids» — машины с точными компактными описаниями, но с нерешённым вопросом останова.
- Демонстрирует, что автономные ИИ, сочетающие рассуждения LLM и формальную верификацию, могут делать новые формально проверенные открытия в невычислимой, открытой математической области (Busy Beaver).
ПОЧЕМУ ЭТО ВАЖНО
Демонстрирует, что автономные ИИ, сочетающие рассуждения LLM и формальную верификацию, могут делать новые формально проверенные открытия в невычислимой, открытой математической области (Busy Beaver).