Math and ML stuff

AlphaGeometry от DeepMind . Разбираемся подробно.

AlphaGeometry способна к математическому ризонингу в эвклидовой геометрии на плоскости, на уровне призеров международной олимпиады по геометрии IMO. С этой же задачей GPT-4 справляется с успехом 0%. AlphaGeometry работает как гибрид 2-х парадигм: символьной дедукции и нейросетей. Общий пайплайн вывода выглядит так:

1. Подаем на вход текст задачи: предпосылка и цель, в доменно специфичном языке (DSL)
2. LLM на основе предпосылок генерирует вспомогательную (magic) конструкцию и передаёт в символьный движок.
3. Символьный движок на основе пошагово/аксиоматических методов выполняет механическую дедукцию и предлагает решение.
4. Если решение не правильное, снова отправляем LLM для создания дополнительной новой magic construction.
5. И так в цикле, пока решение не будет найдено.

Компоненты и методология

1.Символьный движок, соединяющий дедукцию и алгебраический вывод (deduction algebraic reasoning - DDAR): берет за основу механические, захардкоженные правила вывода, например: "E середина отрезка AB, F середина AC, то EF параллельно BC". Они давно известны и аккуратно систематизированы в 2000 г. Далее, расширяем эти правила с помощью операций над углами, отношениями, расстояниями между точками и арифметикой с константами - это алгебраическая составляющая движка. Сам по себе этот движок без нейронных компонент показывает эффективность чуть ниже бронзовых медалистов IMO и решает 15 из 30 задач.

2. Генерация синтетических теорем и доказательств. Синтетический датасет доказательств для обучения LLM модели собирается следующим образом: стартуем с предпосылок Р, генерируем направленный ациклический граф (DAG) логического вывода с помощью символьного движка, а затем фиксируем один из узлов N и идем по дереву назад (обратная трассировка) для идентификации подграфа зависимостей G(N), необходимого для геометрического вывода от минимального кол-ва выбранных посылок P (листьев) к выбранному узлу-выводу N, получаем датасет пар: <теорема: листья P и узел N> <подграф-доказательство G(N)>

После отсева изморофных док-в остается 100 млн пар <теорема-доказательство>, длины док-в распределяются от 1 до 247 шагов, средняя длина 60 при средней длины док-ва человеком в IMO - 50 шагов. Среди полученных док-в есть также заново переизобретенные хорошо известные. Стоит отметить, что метод док-в у символьных движков отличается от метода у систем компьютерной алгебры (а их точность 10/30 задач на IMO).

3. Обучение LLM. Структура <P, N, G (N)> сериализуется в текстовую строку <предпосылка> <вывод> <доказательство>. Обучаясь на таких последовательностях символов, языковая модель эффективно учится генерировать доказательство, обусловливая предпосылки и выводы теоремы. Архитектура модели проста - Трансформер с 12 слоями, 8 головами, со скромным 151 млн параметров и длиной контекста 1024 токена обучается всего лишь на 4-х GPU V100. На полученном в п.2 датасете обучают LLM, точность 21/30 задач.
Но это еще не всё.

4. Magic construction. У существующих дедуктивных решений генерации доказательств есть одно ограничение: они плохо справляются, когда требуется предложить нестандартное решение с введением новых понятий. Ключевой момент у AlphaGeometry для генерации доказательств - это предложение magic construction, т.е. введения новых вспомогательных конструкций (exogenous term). Для этого дополняем датасет следующим трюком: берем предпосылки, от которых результат N зависит, но они не входят в минимальный набор Р, и переносим их в доказательство. Тюнинг LLM на этом небольшом дополнении датасета (9 млн) заставляет генеративную модель "строить" новые предпосылки в самом док-ве и повышает точность до 23/30 задач.

В итоге, AlphaGeometry как нейро-символьная система, работающая в цикле, решает 25/30 задач в IMO, золотой медалист 26/30. Говоря про фронтиры применимости за пределами школьной геометрии, то для успешного обобщения AlphaGeometry на другие домены, требуется база дедуктивных выводов и формализация домена, что для многих областей не очень развито, поэтому перспектива сомнительная.

www.tgoop.com/junkyardmathml/157

3.2K viewsedited  Jan 21, 2024 at 08:51

AlphaGeometry от DeepMind . Разбираемся подробно.

AlphaGeometry способна к математическому ризонингу в эвклидовой геометрии на плоскости, на уровне призеров международной олимпиады по геометрии IMO. С этой же задачей GPT-4 справляется с успехом 0%. AlphaGeometry работает как гибрид 2-х парадигм: символьной дедукции и нейросетей. Общий пайплайн вывода выглядит так:

1. Подаем на вход текст задачи: предпосылка и цель, в доменно специфичном языке (DSL)
2. LLM на основе предпосылок генерирует вспомогательную (magic) конструкцию и передаёт в символьный движок.
3. Символьный движок на основе пошагово/аксиоматических методов выполняет механическую дедукцию и предлагает решение.
4. Если решение не правильное, снова отправляем LLM для создания дополнительной новой magic construction.
5. И так в цикле, пока решение не будет найдено.

Компоненты и методология

1.Символьный движок, соединяющий дедукцию и алгебраический вывод (deduction algebraic reasoning - DDAR): берет за основу механические, захардкоженные правила вывода, например: "E середина отрезка AB, F середина AC, то EF параллельно BC". Они давно известны и аккуратно систематизированы в 2000 г. Далее, расширяем эти правила с помощью операций над углами, отношениями, расстояниями между точками и арифметикой с константами - это алгебраическая составляющая движка. Сам по себе этот движок без нейронных компонент показывает эффективность чуть ниже бронзовых медалистов IMO и решает 15 из 30 задач.

2. Генерация синтетических теорем и доказательств. Синтетический датасет доказательств для обучения LLM модели собирается следующим образом: стартуем с предпосылок Р, генерируем направленный ациклический граф (DAG) логического вывода с помощью символьного движка, а затем фиксируем один из узлов N и идем по дереву назад (обратная трассировка) для идентификации подграфа зависимостей G(N), необходимого для геометрического вывода от минимального кол-ва выбранных посылок P (листьев) к выбранному узлу-выводу N, получаем датасет пар: <теорема: листья P и узел N> <подграф-доказательство G(N)>

После отсева изморофных док-в остается 100 млн пар <теорема-доказательство>, длины док-в распределяются от 1 до 247 шагов, средняя длина 60 при средней длины док-ва человеком в IMO - 50 шагов. Среди полученных док-в есть также заново переизобретенные хорошо известные. Стоит отметить, что метод док-в у символьных движков отличается от метода у систем компьютерной алгебры (а их точность 10/30 задач на IMO).

3. Обучение LLM. Структура <P, N, G (N)> сериализуется в текстовую строку <предпосылка> <вывод> <доказательство>. Обучаясь на таких последовательностях символов, языковая модель эффективно учится генерировать доказательство, обусловливая предпосылки и выводы теоремы. Архитектура модели проста - Трансформер с 12 слоями, 8 головами, со скромным 151 млн параметров и длиной контекста 1024 токена обучается всего лишь на 4-х GPU V100. На полученном в п.2 датасете обучают LLM, точность 21/30 задач.
Но это еще не всё.

4. Magic construction. У существующих дедуктивных решений генерации доказательств есть одно ограничение: они плохо справляются, когда требуется предложить нестандартное решение с введением новых понятий. Ключевой момент у AlphaGeometry для генерации доказательств - это предложение magic construction, т.е. введения новых вспомогательных конструкций (exogenous term). Для этого дополняем датасет следующим трюком: берем предпосылки, от которых результат N зависит, но они не входят в минимальный набор Р, и переносим их в доказательство. Тюнинг LLM на этом небольшом дополнении датасета (9 млн) заставляет генеративную модель "строить" новые предпосылки в самом док-ве и повышает точность до 23/30 задач.

В итоге, AlphaGeometry как нейро-символьная система, работающая в цикле, решает 25/30 задач в IMO, золотой медалист 26/30. Говоря про фронтиры применимости за пределами школьной геометрии, то для успешного обобщения AlphaGeometry на другие домены, требуется база дедуктивных выводов и формализация домена, что для многих областей не очень развито, поэтому перспектива сомнительная.

BY Math and ML stuff