AlphaGeometry [2024] - ещё один пример дружбы поиска и нейросети, но не совсем

В предыдущих Alpha-работах, основанных на AlphaZero, мы встречали комбинацию нейросети и символьного поиска / поиска по дереву, в которой нейросеть отвечала за более удачный порядок перебора. Здесь баланс их взаимодействия смещён в сторону именно поиска. ML тут является важной, но не настолько ключевой компонентой, давайте разберёмся, почему.

В задачах по геометрии есть набор утверждений в качестве условия - заданы такие-то треугольники, окружности и т.д., и нужно доказать какое-то утверждение про заданные объекты. Для конструирования доказательств используется набор правил. На основе него работает не-ML-ный "symbolic deduction engine", пытающийся решить задачу. Сам по себе он уже решает 14/30 задач, что довольно круто для перебора. Это показывает, что наши мозги плохо заточены под геометрические задачи.

Ещё 11 задач приносит как раз ML, но как? В геометрических задачах часто используются "дополнительные конструкции" при решении - это когда мы сами вводим какой-то вспомогательный объект в задачу, который используется в доказательстве. Модель научили генерировать дополнительные конструкции, которые потом будет использовать символьный движок.

Отдельной программой сэмплировали наборы изначальных условий, для них генерировали доказательства всевозможных утверждений про заданные объекты, получился огромный датасет. Для конкретного доказанного факта смотрели - какие изначальные условия являются необязательными для него? Эти условия и будут размечены, как дополнительные конструкции. Далее на этом обучили LLM на их генерацию.

Думаю, что генерация огромного датасета синтетических задач станет основой создания нейросетевого математика. С нетерпением жду, когда её адаптируют под негеометрический домен. Однако, это не единственное, что сейчас нас останавливает от доказательства того, что P != NP, если такого математика вообще получится создать с помощью вручную спроектированного алгоритма.

@knowledge_accumulator