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/6109
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/6109

View MORE
Open in Telegram


Telegram | DID YOU KNOW?

Date: |

"The result is on this photo: fiery 'greetings' to the invaders," the Security Service of Ukraine wrote alongside a photo showing several military vehicles among plumes of black smoke. After fleeing Russia, the brothers founded Telegram as a way to communicate outside the Kremlin's orbit. They now run it from Dubai, and Pavel Durov says it has more than 500 million monthly active users. 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. On Telegram’s website, it says that Pavel Durov “supports Telegram financially and ideologically while Nikolai (Duvov)’s input is technological.” Currently, the Telegram team is based in Dubai, having moved around from Berlin, London and Singapore after departing Russia. Meanwhile, the company which owns Telegram is registered in the British Virgin Islands. There was another possible development: Reuters also reported that Ukraine said that Belarus could soon join the invasion of Ukraine. However, the AFP, citing a Pentagon official, said the U.S. hasn’t yet seen evidence that Belarusian troops are in Ukraine.
from us


Telegram Data Secrets
FROM American