DeepMind нашла закономерности в работе 11 машин Тьюринга и доказала их в Lean 4

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

Машина Тьюринга — это абстрактная модель компьютера: она выполняет инструкции, записывает символы на ленту, двигается по ней и меняет внутреннее состояние. Устройство простое, поведение при этом может быть крайне сложным. Работа шла вокруг задачи Busy Beaver: нужно найти машину с заданным числом состояний, которая до остановки сделает максимальное число шагов. Для машин с шестью состояниями и двумя символами остаются случаи, где даже неизвестно, завершится ли программа.

Система не решала заранее поставленную задачу. Сначала алгоритмы искали повторяющиеся структуры в результатах симуляции машин, затем Gemini на их основе выдвигал гипотезы и строил компактные правила, описывающие поведение программы. После предварительных проверок система формировала доказательство, переводила его в формальный вид и проверяла в Lean 4 — среде, которая строго подтверждает корректность математических рассуждений.

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

Главную загадку этих 11 машин исследователи не решили: останавливаются ли они, неизвестно. Правила точно описывают поведение, но не обязательно позволяют сказать, закончится ли вычисление. Авторы предлагают пока относить такие экземпляры к категории Cryptids — машин, у которых есть компактное математическое описание работы, но открыт вопрос об остановке. Признают ли такую классификацию, зависит от научного сообщества.

Работа показывает переход от ИИ, который решает задачи, поставленные человеком, к системам, способным самостоятельно находить математические структуры и доказывать результат. Ограничение нынешнего подхода в том, что система ищет закономерности, похожие на возникающие в задачах типа Коллатца. Расширение метода на другие виды вычислительного поведения авторы называют направлением дальнейших исследований. Решение принципиально неразрешимых задач таким способом не гарантируется.