Новый алгоритм сочетает в себе обучение с подкреплением и поиск по дереву Монте-Карло, чтобы показать уникальные уровни математических рассуждений.
Недавно я запустил образовательный информационный бюллетень, посвященный ИИ, у которого уже более 150 000 подписчиков. TheSequence — это информационный бюллетень, ориентированный на машинное обучение, без BS (то есть без шумихи, без новостей и т. д.), чтение которого занимает 5 минут. Цель состоит в том, чтобы держать вас в курсе проектов машинного обучения, научных работ и концепций. Пожалуйста, попробуйте, подписавшись ниже:
Математическое мышление — одна из самых амбициозных целей нового поколения методов искусственного интеллекта (ИИ). В последние месяцы OpenAI сделал важные шаги в этой области, выпустив модель, которая действует как средство доказательства теорем для математической среды Lean. Точно так же AlphaTensor DeepMind смог открыть новые алгоритмы умножения матриц. Всего несколько дней назад Meta AI продемонстрировал свой вклад в эту сложную область глубокого обучения, представив HyperTree Proof Search (HTPS), модель глубокого обучения, которая смогла решить несколько задач Международной математической олимпиады (IMO). Этот метод демонстрирует важные возможности, демонстрирующие, что математические рассуждения определенно возможны с глубокими нейронными сетями.
Проблемы математического мышления и проблемы ИМО для ИИ
Немецкий гениальный математик Карл Фридрих Гаусс называл математику «королевой наук», имея в виду ее влияние на другие дисциплины. Формальная математика является универсальным языком для выражения фундамента многих научных открытий. С точки зрения глубокого обучения математические рассуждения сталкиваются с рядом фундаментальных проблем:
И. Бесконечное пространство действий. Глубокие нейронные сети добились огромного прогресса в таких задачах, как го или многопользовательские игры с большим пространством поиска. Однако формальные математические теоремы часто имеют дело с бесконечным пространством поиска. При доказательстве математических теорем нам предоставляется не конечный и понятный набор действий, а скорее бесконечный набор математических конструкций, которые необходимо создать, чтобы прийти к окончательному доказательству.
II. Отсутствие самостоятельной игры:самостоятельная игра в форме моделей обучения с подкреплением была одной из техник, которая сделала заметные успехи в средах с большим пространством поиска. Однако этот тип техники непрактичен в доказательстве математических теорем. При наличии математического утверждения не всегда есть очевидный способ переформулировать его в более простые промежуточные шаги, которые можно использовать для структурирования формальной стратегии.
Среди области математических рассуждений проблемы ИМО считаются серьезным препятствием для области ИИ. Несколько ведущих лабораторий искусственного интеллекта в мире объединились, чтобы решить грандиозную задачу по созданию моделей глубокого обучения, которые могут решать математические задачи уровня IMO. Задачи IMO считаются высшим уровнем математических соревнований средней школы и требуют не только передовых математических знаний, но и сложных многоэтапных рассуждений.
Поиск с доказательством HyperTree (HTPS)
Как видно из названия, основная идея HTPS Meta AI основана на модели поиска по дереву, аналогичной той, что используется в поисковых системах. Однако HTPS дополняет технику поиска по дереву очень продвинутыми методами глубокого обучения. По определению математическое доказательство теорем работает в неполной среде, поскольку на большинстве шагов окончательная последовательность решения не видна. В результате HTPS необходимо было связать текущее «состояние» доказательства теорем с «неполным» пониманием проблемы. HTPS опирается на модель обучения с подкреплением, связанную с тремя основными помощниками по проверке:
I. Lean: полный язык программирования для доказательства математических теорем.
II. Metamath: язык, который может выражать математические теоремы и проверяемые доказательства.
III. Уравнения. Более простая и выразительная математическая среда, также созданная Meta.
Использование помощника по доказыванию позволяет модели обучения с подкреплением строить пошаговые рассуждения. В конечном итоге модель строит логический граф, в котором текущее состояние представляет собой узел, а каждый возможный следующий шаг — ребро. Используя этот график, HTPS использует трехэтапный алгоритм:
Я. Использование политики поиска для выбора гипердерева с развернутыми слоями узлов.
II. Расширьте выбранные узлы новыми тактиками.
III. Используйте модель обратного распространения для оптимизации узлов гипердерева.
Вы можете увидеть этот алгоритм в действии для уравнения: cos(x) + ex ‹ 1 + 2ex в следующем дереве.
HTPS смог решить несколько проблем IMO с невероятной эффективностью. Meta AI также включил HTPS через плагин Lean Visual Studio Code (VSCode), который позволяет специалистам по данным напрямую взаимодействовать с моделью.
