Telegram Group & Telegram Channel
Google релизнули Alpha Geometry 2: модель решает задачи по геометрии на уровне золотого медалиста Международной Математической Олимпиады

Первая версия Alpha Geometry вышла практически ровно год назад, и относительно нее новая версия сильно прокачалась: если предшественница решала 54% всех задач по геометрии с IMO 2000-2024, то AG2 справляется с 84%. Это, если что, на 84% больше, чем результат o1 👽

При этом AG2 не совсем нейросеть. Это нейро-символьная система. То есть AG2 объединяет в себе и LLM, и символьные строгие методы для вычислений и доказательств. В общих чертах AG2 потрошится на три основных составляющих:

1. Зафайнтюненная Gemini, которой скормили 300 млн теорем. Модель анализирует текст задачи и диаграммы и как бы интуитивно намечает решение: подсказывает, какие свойства фигур могут быть полезны, какие теоремы могут пригодиться и так далее. Она также служит своеобразным энкодером и формализует текст задачи в доменный язык, который умеет воспринимать символьный модуль.

2. Символьный движок DDAR2, в который сгружаются все результаты Gemini. Он берет на себя доказательства по строгим правилам геометрии и проверку и расширение предложенных LM решений с помощью дедукции. В новый DDAR добавили поддержку сложных геометрических конструкций, а также умение работать с "двойными" точками (такие возникают в куче примеров, наверное все помнят со школы задачи вида "докажите, что такая-то точка пересечения лежит на такой-то окружности").

А еще по сравнению с DDAR1 DDAR2 сильно ускорили с помощью C++ реализации и оптимизированного перебора вариантов решений. Раньше все работало на брутфорсе, а сейчас алгоритм переделали и сложность уменьшилась с 𝑂(𝑁⁸) до 𝑂(𝑁³), что увеличило скорость решения в 300 раз!

3. Ну и финальное: деревья поиска SKEST. Это как раз та самая оптимизация. Классические деревья предлагают как бы один шаг решения за раз. А в SKEST мы пробуем несколько вершин разом: это присходит за счет параллельного запуска нескольких деревьев, которые могут делиться между собой найденными стратегиями.

Плюсом ко всему, Alpha Geometry 2 даже умеет автоматически строить к своим решениям рисунки. К сожалению, демо пока не выложили, зато доступна статья.
Please open Telegram to view this post
VIEW IN TELEGRAM
Please open Telegram to view this post
VIEW IN TELEGRAM



group-telegram.com/data_secrets/6110
Create:
Last Update:

Google релизнули Alpha Geometry 2: модель решает задачи по геометрии на уровне золотого медалиста Международной Математической Олимпиады

Первая версия Alpha Geometry вышла практически ровно год назад, и относительно нее новая версия сильно прокачалась: если предшественница решала 54% всех задач по геометрии с IMO 2000-2024, то AG2 справляется с 84%. Это, если что, на 84% больше, чем результат o1 👽

При этом AG2 не совсем нейросеть. Это нейро-символьная система. То есть AG2 объединяет в себе и LLM, и символьные строгие методы для вычислений и доказательств. В общих чертах AG2 потрошится на три основных составляющих:

1. Зафайнтюненная Gemini, которой скормили 300 млн теорем. Модель анализирует текст задачи и диаграммы и как бы интуитивно намечает решение: подсказывает, какие свойства фигур могут быть полезны, какие теоремы могут пригодиться и так далее. Она также служит своеобразным энкодером и формализует текст задачи в доменный язык, который умеет воспринимать символьный модуль.

2. Символьный движок DDAR2, в который сгружаются все результаты Gemini. Он берет на себя доказательства по строгим правилам геометрии и проверку и расширение предложенных LM решений с помощью дедукции. В новый DDAR добавили поддержку сложных геометрических конструкций, а также умение работать с "двойными" точками (такие возникают в куче примеров, наверное все помнят со школы задачи вида "докажите, что такая-то точка пересечения лежит на такой-то окружности").

А еще по сравнению с DDAR1 DDAR2 сильно ускорили с помощью C++ реализации и оптимизированного перебора вариантов решений. Раньше все работало на брутфорсе, а сейчас алгоритм переделали и сложность уменьшилась с 𝑂(𝑁⁸) до 𝑂(𝑁³), что увеличило скорость решения в 300 раз!

3. Ну и финальное: деревья поиска SKEST. Это как раз та самая оптимизация. Классические деревья предлагают как бы один шаг решения за раз. А в SKEST мы пробуем несколько вершин разом: это присходит за счет параллельного запуска нескольких деревьев, которые могут делиться между собой найденными стратегиями.

Плюсом ко всему, Alpha Geometry 2 даже умеет автоматически строить к своим решениям рисунки. К сожалению, демо пока не выложили, зато доступна статья.

BY Data Secrets








Share with your friend now:
group-telegram.com/data_secrets/6110

View MORE
Open in Telegram


Telegram | DID YOU KNOW?

Date: |

As the war in Ukraine rages, the messaging app Telegram has emerged as the go-to place for unfiltered live war updates for both Ukrainian refugees and increasingly isolated Russians alike. He said that since his platform does not have the capacity to check all channels, it may restrict some in Russia and Ukraine "for the duration of the conflict," but then reversed course hours later after many users complained that Telegram was an important source of information. "Russians are really disconnected from the reality of what happening to their country," Andrey said. "So Telegram has become essential for understanding what's going on to the Russian-speaking world." "There are a lot of things that Telegram could have been doing this whole time. And they know exactly what they are and they've chosen not to do them. That's why I don't trust them," she said. Some privacy experts say Telegram is not secure enough
from es


Telegram Data Secrets
FROM American