AlphaGeometry: Прорыв в автоматическом доказательстве олимпиадных задач по геометрии 0:01
Google DeepMind представила модель AlphaGeometry, специализирующуюся на решении геометрических задач уровня математических олимпиад. Ключевая особенность системы заключается в том, что она способна находить доказательства без использования демонстрационных данных, созданных людьми. По мнению автора видео, Янника Кильхера, это достижение является важным прорывом в компьютерной математике, однако сама технология остается узкоспециализированной и требует выполнения строгих условий для эффективной работы.
Гибридный подход к доказательствам 0:53
AlphaGeometry представляет собой нейросимволическую систему, объединяющую две ключевые составляющие:
- Символьный решатель (prover): занимается дедуктивным выводом на основе имеющихся аксиом и правил.
- Языковая модель (LLM): генерирует идеи для «вспомогательных построений» (auxiliary constructions), необходимых для продвижения в сложных доказательствах.
Сложность геометрии, как отмечает Кильхер, часто заключается в необходимости вводить новые элементы — например, вспомогательные точки, окружности или прямые, которые изначально отсутствуют в условии задачи. Классические системы доказательств не могут эффективно искать такие объекты, так как количество возможных построений практически бесконечно, что создает неразрешимую проблему поиска.
Механика обучения без человеческих данных 8:04
Один из самых примечательных аспектов AlphaGeometry — полное отсутствие человеческих примеров в обучающей выборке. Разработчики создали систему, которая обучается на синтетически сгенерированных данных:
- Генерация примитивов: система случайным образом строит геометрические фигуры, используя ограниченный набор базовых операций (биссектрисы, инцентры, касательные и т.д.).
- Символьная дедукция: после создания конструкции система использует символьный решатель для вывода всех возможных утверждений о ней.
- Обратный путь (traceback): чтобы научить модель предлагать полезные построения, система берет доказанное утверждение и «прослеживает» логический путь назад, выделяя элементы, которые не входили в итоговое условие, но были необходимы для доказательства.
По словам Кильхера, такой подход позволяет модели «понять», какие именно вспомогательные объекты нужно добавлять для решения конкретных задач. Весь процесс напоминает цикл: если текущих данных недостаточно, модель предлагает конструкцию, символьный решатель пытается найти доказательство, и процесс повторяется до успеха.
Результаты и ограничения системы 26:26
В рамках тестирования на 30 олимпиадных геометрических задачах AlphaGeometry успешно решила 25 из них. Кильхер обращает внимание на любопытные детали абляционных исследований:
- Даже при использовании лишь 20% данных или 2% вычислительного бюджета на этапе тестирования, система все равно решает 21 задачу.
- Это, по мнению ведущего, может свидетельствовать о достижении некоего «потолка»: дальнейшее увеличение ресурсов дает лишь маргинальный прирост эффективности.
Читаемость и интерпретируемость 32:04
Важным решением разработчиков стал отказ от использования формальных языков общего назначения (вроде Lean) в пользу специализированного доменного языка. Это дало два преимущества:
- Интерпретируемость: доказательства AlphaGeometry выглядят как шаги, написанные участником олимпиады, что позволяет человеку легко проверить ход мысли модели.
- Эффективность обучения: ограниченный словарь и специфический синтаксис позволяют модели лучше обучаться на имеющемся объеме данных.
В завершение Янник Кильхер задается вопросом, насколько масштабируема эта техника для других математических доменов, где структура фундаментальных элементов не столь жестко ограничена, как в евклидовой геометрии.
