# Янник Кильхер об AlphaGeometry: «Прорыв в геометрии без участия людей»

Источник: https://www.youtube.com/watch?v=ZNK4nfgNQpM
Канал: Yannic Kilcher
Опубликовано: 21.01.2024

---

## AlphaGeometry: Прорыв в автоматическом доказательстве олимпиадных задач по геометрии
[[JUMP:0:01]]

Google DeepMind представила модель AlphaGeometry, специализирующуюся на решении геометрических задач уровня математических олимпиад. Ключевая особенность системы заключается в том, что она способна находить доказательства без использования демонстрационных данных, созданных людьми. По мнению автора видео, Янника Кильхера, это достижение является важным прорывом в компьютерной математике, однако сама технология остается узкоспециализированной и требует выполнения строгих условий для эффективной работы.

### Гибридный подход к доказательствам
[[JUMP:0:53]]

AlphaGeometry представляет собой нейросимволическую систему, объединяющую две ключевые составляющие:

1.  **Символьный решатель (prover):** занимается дедуктивным выводом на основе имеющихся аксиом и правил.
2.  **Языковая модель (LLM):** генерирует идеи для «вспомогательных построений» (auxiliary constructions), необходимых для продвижения в сложных доказательствах.

Сложность геометрии, как отмечает Кильхер, часто заключается в необходимости вводить новые элементы — например, вспомогательные точки, окружности или прямые, которые изначально отсутствуют в условии задачи. Классические системы доказательств не могут эффективно искать такие объекты, так как количество возможных построений практически бесконечно, что создает неразрешимую проблему поиска.

### Механика обучения без человеческих данных
[[JUMP:8:04]]

Один из самых примечательных аспектов AlphaGeometry — полное отсутствие человеческих примеров в обучающей выборке. Разработчики создали систему, которая обучается на синтетически сгенерированных данных:

*   **Генерация примитивов:** система случайным образом строит геометрические фигуры, используя ограниченный набор базовых операций (биссектрисы, инцентры, касательные и т.д.).
*   **Символьная дедукция:** после создания конструкции система использует символьный решатель для вывода всех возможных утверждений о ней.
*   **Обратный путь (traceback):** чтобы научить модель предлагать полезные построения, система берет доказанное утверждение и «прослеживает» логический путь назад, выделяя элементы, которые не входили в итоговое условие, но были необходимы для доказательства.

По словам Кильхера, такой подход позволяет модели «понять», какие именно вспомогательные объекты нужно добавлять для решения конкретных задач. Весь процесс напоминает цикл: если текущих данных недостаточно, модель предлагает конструкцию, символьный решатель пытается найти доказательство, и процесс повторяется до успеха.

### Результаты и ограничения системы
[[JUMP:26:26]]

В рамках тестирования на 30 олимпиадных геометрических задачах AlphaGeometry успешно решила 25 из них. Кильхер обращает внимание на любопытные детали абляционных исследований:

*   Даже при использовании лишь 20% данных или 2% вычислительного бюджета на этапе тестирования, система все равно решает 21 задачу.
*   Это, по мнению ведущего, может свидетельствовать о достижении некоего «потолка»: дальнейшее увеличение ресурсов дает лишь маргинальный прирост эффективности.

### Читаемость и интерпретируемость
[[JUMP:32:04]]

Важным решением разработчиков стал отказ от использования формальных языков общего назначения (вроде Lean) в пользу специализированного доменного языка. Это дало два преимущества:

*   **Интерпретируемость:** доказательства AlphaGeometry выглядят как шаги, написанные участником олимпиады, что позволяет человеку легко проверить ход мысли модели.
*   **Эффективность обучения:** ограниченный словарь и специфический синтаксис позволяют модели лучше обучаться на имеющемся объеме данных.

В завершение Янник Кильхер задается вопросом, насколько масштабируема эта техника для других математических доменов, где структура фундаментальных элементов не столь жестко ограничена, как в евклидовой геометрии.