Наука 22 октября 2026, 20:27 МСК

ИИ на базе Gemini нашёл и формально доказал закономерности для 11 машин Тьюринга

Google DeepMind и Кембриджский университет создали систему на Gemini, которая самостоятельно выявила новые правила поведения 11 машин Тьюринга класса BB(6) и доказала их в Lean 4.

Исследователи занимались задачей Busy Beaver — поиском машины с заданным числом состояний, работающей максимально долго до остановки. Для шестисостоятельных двухсимвольных машин остаются экземпляры, про которые неизвестно, остановятся ли они.

Алгоритмы находят повторяющиеся структуры в симуляциях, Gemini выдвигает гипотезы и строит компактные правила, затем система формирует доказательство, переводит его в формальный вид и проверяет в Lean 4. Для 11 машин ранее не было задокументированного анализа. Для ещё 15 уже изучавшихся машин получены формальные доказательства похожих правил или способы ускорить анализ. По структуре закономерности напоминают системы, связанные с гипотезой Коллатца.

Главный вопрос — останавливаются ли эти машины — остался открытым. Авторы предлагают предварительно относить их к «криптидам» (Cryptids), но это зависит от принятия научным сообществом. Метод пока ограничен закономерностями, похожими на задачи типа Коллатца.

• 11 новых машин класса BB(6) и ещё 15 ранее изученных
• Доказательства проверены в Lean 4
• Вопрос остановки не решён