Плейбой-конструктор

- «Существуют легендарные примеры компьютерных доказательств, которые длиннее, чем Википедия. Это не тот случай: речь идет о очень кратком, человекоподобном решении.»

Доказательство AlphaGeometry 2 включало построение окружности вокруг другой точки и использование этой окружности для доказательства общего ответа. «Сначала наш эксперт не совсем понял, зачем вообще была построена эта точка, но после изучения решения стало ясно, что оно действительно объединяет множество треугольников, и решение оказалось весьма элегантным», — сказал Луонг.

Руководитель проекта AlphaGeometry 2, Тханг Луонг, описал результат как аналог знаменитого «хода 37» в исторической победе DeepMind в Го, когда ИИ сделал ход, о котором ни один человек бы не подумал, и выиграл.

Стала ли AlphaGeometry прорывом в ИИ? (речь идет о первой версии - kvisaz)

Команда разработчиков AlphaGeometry создала инструмент, названный ею DD+AR (если мне не изменяет память, это расшифровывается как Deductive Database + Algebraic Relations), который, по сути, вычисляет все равенства углов и соотношений, которые можно вывести из условий многократным применением описанных выше инструментов. DD+AR получает из переданных ему условий равенства углов и соотношений, вычисляет при помощи тривиального загона в угол все возможные следующие из них равенства углов, проверяет по приведённым выше критериям, какие из них подразумевают наличие циклических четырёхугольников или подобных треугольников, вычисляет из этого новые равенства углов, и повторяет процесс до того момента, пока невозможно будет найти новые соотношения углов.

То есть самая главная хитрость заключается в том, что в DD+AR вообще не используется НИКАКОГО ИИ! (Разумеется, тут можно погрузиться в философские рассуждения о том, что же такое ИИ. Я имею в виду, что DD+AR — это просто традиционный детерминированный алгоритм, который можно было реализовать ещё тогда, когда только появились компьютеры.)

Создав систему, способную строить новые точки, её естественным образом можно скомбинировать с DD+AR. Сначала мы выполняем DD+AR. Если он пришёл к решению, проверяем его. Если нет, строим новую точку, попросив об этом LLM, а затем снова выполняем DD+AR. Если он пришёл к решению, проверяем его. Если нет, добавляем новую точку. Намылить, смыть и повторить. Вот и всё, что делает AlphaGeometry.

Но что же это значит в конечном итоге? Что меня теперь не удивляет то, на что способна AlphaGeometry? Напротив, по-прежнему удивляет, но когда я понял, как работает AlphaGeometry, причина моего удивления поменялась. Меня, как бывшего олимпиадника, больше всего удивляет, что DD+AR, то есть многократное использование циклических четырёхугольников и подобных треугольников, гораздо эффективнее, чем я думал. Дело в том. что мы, живые «решающие устройства», не решаем большинство задач при помощи «DD+AR». В определённой степени мы пробуем, но в случае, если долго не находим ни одного циклического четырёхугольника или пары подобных треугольников, сдаёмся и переходим к более сложным техникам: используем понятие степени точки относительно окружности, проективную геометрию, инверсию и так далее. AlphaGeometry научила меня тому, что на удивление часто существует решение DD+AR, скрывающееся под тонким слоем всего двух-трёх дополнительных точек, а чаще всего не нужно и этого! (Если вы знакомы с теми, как устроены олимпиады, то для вас станет хорошим примером P4 с ММО 2013 года. Я был на ММО, где была представлена эта задача, и с тех пор многократно использовал её как пример задачи на уроках. Во всех известных мне стандартных решениях на чертёж добавлялась одна конкретная точка. Когда я увидел в Файле, что AlphaGeometry решила задачу вообще без добавления новой точки, то есть DD+AR добился успеха в первом раунде, меня это очень удивило. Оказалось, что на чертеже есть подобие треугольников, решающее задачу, и за все эти годы я его не заметил!)