Новости

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Новый отчет мудрости

Редактор: Редакционный отдел

[Введение в новую мудрость] Только что новейшая математическая модель Google DeepMind завоевала серебряную медаль математической олимпиады IMO! Он не только решил 4 из 6 вопросов с высшим баллом, что всего в 1 балле от золотой медали, но и решил 4-й вопрос всего за 19 секунд. Качество и скорость решения задачи ошеломили судей-людей, выставивших оценки. .

AI завоевал серебряную медаль математической олимпиады IMO!

Только что компания Google DeepMind объявила, что настоящие вопросы Международной математической олимпиады этого года были созданы ее собственной системой искусственного интеллекта.

Среди них AI не только успешно выполнил 4 из 6 вопросов, но и получил за каждый вопрос полную оценку, что эквивалентно наивысшему баллу серебряной медали – 28 баллов.

Этот результат отделяет всего 1 балл от золотой медали!

Из 609 участников только 58 завоевали золотые медали.

В официальном соревновании участники-люди будут отправлять свои ответы в два сеанса, каждый раз с ограничением по времени в 4,5 часа.

Интересно, что на ответ на один из вопросов ИИ потребовалось всего несколько минут, а вот на остальные вопросы ушло три полных дня, что можно назвать серьёзным тайм-аутом.

На этот раз большой вклад внесли две системы искусственного интеллекта — AlphaProof и AlphaGeometry 2.

Важный момент: 2024 год ИМО не указан в данных обучения этих двух ИИ.

Скотт Ву, один из основателей инженера по искусственному интеллекту Девина (трехкратного золотого медалиста IOI), посетовал: «Когда я был ребенком, олимпиады были всем, что у меня было, я никогда не думал, что всего 10 лет спустя их заменит ИИ. . решено».

В этом году конкурс IMO включает шесть конкурсных вопросов, касающихся алгебры, комбинаторики, геометрии и теории чисел. Шесть путей составляют четыре, давайте почувствуем уровень ИИ——

Способность ИИ к математическому мышлению шокирует профессора

Мы все знаем, что предыдущий ИИ был ограничен в решении математических задач из-за ограничений в возможностях рассуждения и обучающих данных.

Два ИИ-игрока, появившиеся сегодня вместе, нарушили это ограничение. они соответственно--

- AlphaProof, новая система формальных математических рассуждений, основанная на обучении с подкреплением.

- AlphaGeometry 2, система решения геометрических задач второго поколения.

Ответы, данные двумя искусственными интеллектами, оценивались в соответствии с правилами известных математиков профессора Тимоти Гауэрса (золотой медалистки ИМО и медалиста Филдса) и доктора Джозефа Майерса (двукратного золотого медалиста ИМО и председателя Комитета по отбору вопросов ИМО 2024 года). .

В конце концов, AlphaProof правильно решила две задачи по алгебре и одну задачу по теории чисел. Одну из самых сложных задач в этом году на IMO AlphaGeometry 2 решили задачи по геометрии.

Есть только две задачи комбинаторной математики, которые не решены.

Профессор Тимоти Гауэрс также был глубоко шокирован во время процесса выставления оценок:

То, что программа смогла найти такое неочевидное решение, действительно впечатляет и превосходит все мои ожидания, учитывая нынешний уровень техники.

AlphaProof

AlphaProof — это система, способная доказывать математические утверждения на формальном языке Lean.

Он сочетает в себе предварительно обученную модель большого языка с алгоритмом обучения с подкреплением AlphaZero, который научился освоить шахматы, сёги и го.

Ключевое преимущество формальных языков состоит в том, что их можно формально проверить на доказательствах, включающих математические рассуждения. Однако их применение в машинном обучении ограничено из-за очень ограниченного объема соответствующих данных, написанных людьми.

Напротив, подходы, основанные на естественном языке, несмотря на доступ к большим объемам данных, могут давать правдоподобные, но неправильные промежуточные шаги рассуждения и решения.

Чтобы преодолеть эту проблему, исследователи Google DeepMind доработали модель Gemini для автоматического перевода формулировок задач на естественном языке в формальные утверждения, создав большую библиотеку, содержащую формальные задачи различной сложности, тем самым построив мост между двумя взаимодополняющими областями.

При решении проблемы AlphaProof генерирует варианты решения и доказывает или опровергает их, осуществляя поиск возможных этапов доказательства в Lean.

Каждое найденное и проверенное доказательство используется для усиления языковой модели AlphaProof, чтобы она могла решать более сложные проблемы в будущем.

Чтобы обучить AlphaProof, исследователи доказали или опровергли миллионы вопросов, охватывающих широкий спектр трудностей и математических тем, за несколько недель до и во время соревнований.

Во время соревнований они также применили цикл обучения, усиливая доказательства самостоятельно созданных вариантов задачи конкуренции, пока не было найдено полное решение.

Инфографика цикла обучения с подкреплением AlphaProof: около миллиона неформальных математических задач переводятся формальной сетью на формальный математический язык, а затем постепенно обучается с использованием алгоритма AlphaZero, ища доказательства или опровержения этих проблем; , для решения более сложных задач

АльфаГеометрия 2

AlphaGeometry 2, обновленная версия AlphaGeometry, представляет собой нейронно-символическую гибридную систему, обученную с нуля на основе языковой модели Gemini.

Основываясь на на порядок больше синтетических данных, чем предыдущее поколение, он может решать более сложные геометрические задачи, включая уравнения, связанные с движением объектов, углами, пропорциями, расстояниями и т. д.

Кроме того, он оснащен символическим движком, который на два порядка быстрее своего предшественника. При возникновении новых проблем он использует новый механизм обмена знаниями, который позволяет использовать расширенные комбинации различных деревьев поиска для решения более сложных проблем.

До участия в IMO в этом году AlphaGeometry 2 уже добилась больших успехов: она смогла решить 83% задач по геометрии IMO за последние 25 лет, в то время как первое поколение могло решить только 53%.

В этом IMO скорость AlphaGeometry 2 шокировала всех — в течение 19 секунд после получения формального вопроса она решила вопрос 4!

Вопрос 4 требует доказательства того, что сумма ∠KIL и ∠XPY равна 180°. AlphaGeometry 2 рекомендует построить точку E на линии BI так, чтобы ∠AEB=90°.Точка E помогает определить середину L треугольника AB, образуя множество подобных пар треугольников, таких как ABE ~ YBI и ALE ~ IPC, тем самым доказывая вывод.

Процесс решения проблем ИИ

Стоит отметить, что эти вопросы сначала будут вручную переведены на формальный математический язык, а затем переданы ИИ.
П1

Вообще говоря, первый вопрос (P1) в каждом тесте IMO относительно прост.

Пользователи сети сказали: «P1 требует только школьных знаний по математике, и игроки-люди обычно завершают его в течение 60 минут».

Первый вопрос IMO 2024 в основном исследует свойства действительного числа α и требует найти действительное число α, удовлетворяющее определенным условиям.

ИИ дал правильный ответ — α — четное целое число. Итак, как именно на него ответить?

На первом этапе решения проблемы ИИ сначала выдвинул теорему о том, что левое и правое множества равны.

Набор слева означает, что все действительные числа α, которые удовлетворяют условиям, для любого положительного целого числа n, n могут делить ⌊i*α⌋ от 1 до n, набор справа означает, что существует целое число k, k равно; четное число, а действительное число α равно k.

Следующее доказательство делится на два направления.

Сначала докажите, что множество справа является подмножеством (простым направлением) множества слева.

Затем докажите, что множество слева является подмножеством множества справа (сложное направление).

До конца кода ИИ придумал ключевое уравнение ⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋), используя это уравнение, чтобы доказать, что α должно быть четное число.

Наконец, DeepMind суммировал три аксиомы, на которые ИИ опирается при решении проблем: propext, Classical.choice и Quot.sound.

Ниже приведен полный процесс решения проблем P1: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html.

П2

Второй вопрос исследует связь между парой натуральных чисел (a, b), которая включает в себя свойство наибольшего общего делителя.

Ответ, который решил ИИ:

Теорема состоит в том, что для пары натуральных чисел (a, b), удовлетворяющей определенным условиям, ее набор может содержать только (1,1).

В следующем процессе решения проблемы стратегия доказательства, принятая ИИ, заключается в том, чтобы сначала доказать, что (1,1) удовлетворяет заданным условиям, а затем доказать, что это единственное решение.

Докажите, что (1,1) является окончательным решением, используя g=2, N=3.

Покажите, что если (a,b) — решение, то ab+1 должно делить g.

В этом процессе ИИ использовал для рассуждений теорему Эйлера и свойства модульных операций.

Наконец, докажите, что a=b=1 — единственно возможное решение.

Ниже приведен полный процесс решения проблем P2: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html.

П4

P4 — это вопрос геометрического доказательства, требующий доказательства конкретного соотношения геометрических углов.

Как упоминалось выше, AlphaGeometry 2 выполнила это за 19 секунд, установив новый рекорд.

В зависимости от данного решения, как и в случае с AlphaGeometry первого поколения, языковая модель автоматически генерирует вспомогательные точки во всех решениях.

В доказательстве при отслеживании всех углов используется метод исключения Гаусса, а d(AB)−d(CD) равно дирекционному углу от AB до CD (по модулю π).

В процессе решения задачи ИИ будет вручную отмечать пары подобных треугольников и конгруэнтных треугольников (отмечены красным).

Далее следуют шаги по решению задачи AlphaGeometry, которая завершается использованием «метода повторного противоречия».

Сначала используйте Lean, чтобы формализовать утверждения, которые необходимо доказать, и визуализировать геометрическую конструкцию.

Основные этапы доказательства заключаются в следующем.

Полный процесс решения проблемы см. на рисунке ниже: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html.

П6

Шестой вопрос ИМО — «конечный босс», который исследует свойства функций и требует доказательства конкретных выводов о рациональных числах.

ИИ решает, c=2.

Давайте сначала посмотрим на формулировку теоремы, которая определяет свойства «функции Акваэсуля» и заявляет, что для всех таких функций набор значений f(r)+f(-r) имеет не более 2 элементов.

Стратегия доказательства состоит в том, чтобы сначала доказать, что для любой функции Акваэсуля множество значений f(r)+f(-r) состоит не более чем из 2 элементов. Затем постройте специальную функцию Акваэсуля так, чтобы f(r)+f(-r) имело ровно два разных значения.

Докажите, что когда f(0)=0, f(x)+f(-x) принимает не более двух разных значений, и докажите, что не существует акваэсуловой функции f(0)≠0.

Постройте функцию f(x)=-x+2⌈x⌉ и докажите, что она является функцией Акваэсуля.

Наконец, докажите, что для этой функции f(-1)+f(1) =0 и f(1/2)+f(-1/2)=2 — два разных значения.

Ниже приведен полный процесс решения проблемы: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html.

Вы можете решать математические задачи на олимпиаде, но сможете ли вы сказать, какой из них больше: 9,11 или 9,9?

Эндрю Гао, исследователь из Стэнфордского университета и компании Sequoia, подтвердил важность этого прорыва в области искусственного интеллекта.

Ключевым моментом является то, что в обучающий набор не включены последние тестовые вопросы IMO. Это важно, поскольку показывает, что ИИ может решать новые, невидимые проблемы.

Более того, геометрические задачи, успешно решаемые с помощью ИИ, всегда считались чрезвычайно сложными из-за особенностей используемого пространства (требующих интуитивного мышления и пространственного воображения).

Джим Фан, старший научный сотрудник Nvidia, опубликовал длинную статью, в которой говорится, что большие модели — это загадочные существа.

Они могут завоевывать серебряные медали на математических олимпиадах и часто допускают ошибки в вопросах типа «Какое число больше: 9,11 или 9,9?»

Не только Близнецы, но и ГПТ-4о, Клод-3,5 и Лама-3 не могут ответить на 100% правильно.

Обучая модели ИИ, мы исследуем обширные области, выходящие за рамки нашего собственного интеллекта.В процессе мы обнаружили очень странную область — экзопланету, похожую на Землю, но полную странных долин.

Это кажется необоснованным, но мы можем объяснить это с помощью распределения обучающих данных:

AlphaProof и AlphaGeometry 2 обучены формальным доказательствам и символьным механизмам, специфичным для предметной области. В какой-то степени они лучше решают специализированные олимпиадные задачи, хотя и построены на базе LLM общего назначения. Обучающий набор GPT-4o смешан с большим количеством данных кода GitHub, которые могут значительно превышать математические данные. Среди версий программного обеспечения «v9.11 > v9.9» может серьезно исказить распределение данных. Поэтому эта ошибка в некоторой степени понятна.

Глава разработчиков Google заявил, что модели, способные решать сложные математические и физические задачи, — это ключевой путь к AGI, и сегодня мы сделали еще один шаг на этом пути.

Другие пользователи сети сказали, что на этой неделе было слишком много информации.

Использованная литература:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

https://x.com/DrJimFan/status/1816521330298356181