Партия переходит в эндшпиль: как искусственный интеллект и методы прошлого века обошли золотых медалистов IMO в геометрии
Решение геометрических задач, даже обычной школьной сложности, — процесс довольно творческий. Нужно что-то заметить, где-то проявить интуицию, пробовать разные подходы и придумывать свои. Отсюда возникает два вывода. Первый — раз задача творческая и не всегда понятно, какими именно принципами руководствоваться, значит она прекрасно подходит для искусственного интеллекта. Второй — противоположный, о котором наверняка думали хоть раз все, у кого с геометрией в школе было туго: нужно максимально формализовать решение, найти законы и превратить творческий процесс в набор правил. Как это обычно бывает, лучшим решением оказывается объединение противоположностей. Но обо всём по порядку.
Алгоритмизация
Механистически точный подход к геометрическим задачам — совсем не новая концепция. И заботила она, конечно, не только “двоечников”, как мы написали в первом абзаце. Вопрос сам по себе очень интересный и возникал, как минимум ещё у Лейбница (который пытался механизировать, кажется, вообще всё). После него попыток и подходов было много. Можно упомянуть, например, алгоритм Альфреда Тарского. Вообще он нужен, чтобы устанавливать истинность или ложность любой арифметической формулы первого порядка. Но любую геометрическую задачку можно поместить в декартовы координаты и привести её к нужному виду, а затем решить с помощью алгоритма Тарского. Несмотря на то, что в целом идея понятная, на деле она разрастается до жуткой сложности. Технически применять алгоритм возможно, но слишком уж неэффективно вычислительно.
В компьютерную эпоху классическим подходом стал считаться метод Вэньцзюня У (Wu Wenjun). Он изначально нацеливался именно на геометрические задачи и именно на возможность компьютерной реализации. Его метод 1978 года заключается в следующем: точки на плоскости определяются как упорядоченные пары чисел в фиксированном поле, затем устанавливается словарь, который переводит геометрическое соотношения в алгебраические выражения. Например для четырех точек А1, А2, А3 и А4 определяются пары чисел (x,y). Соотношение параллельности А1А2 и А3А4 можно выразить уравнением (х1-х2)(у3-у4)-(х3-х4)(у1-у2) = 0. Для любой геометрической задачи определяются фиксированные и нефиксированные точки, а затем записывается система уравнений, соответствующих задаче. Чтобы доказать правдивость какого-либо утверждения, его нужно привести к полиному из введёных переменных, а затем сравнить с нулем по модулю всех записанных соотношений. Если сравнимость выполняется, то утверждение справедливо (У доказал необходимость и достаточность этого условия).
Метод У справляется не только с простыми школьными задачами. В одиночку он достигает уровня среднего участника международной математической олимпиады (IMO) и долгое время оставался в этом state-of-the-art.
Искусственный интеллект
Сместить метод У с этого пьедестала (очень ненадолго, но об этом позже) удалось в конце прошлого года исследователям из DeepMind. Тогда представили AlphaGeomtery (статья, блог, код), которая решила 25 из 30 олимпиадных задач. Этот показатель обходит среднего серебряного медалиста (22,9), но всё ещё отстаёт от золотого (25,9).
Внутри AlphaGeometry объединили языковую модель и дедуктивный модуль символьных вычислений. Свой гибридный подход создатели назвали нейросимвольным. Языковая модель отвечает за “творческую” часть — предлагает потенциально полезные новые построения, а символьные вычисления основаны на формальной логике и используют свод правил.
На входе у AlphaGeometry сама задачка и её чертеж. Модуль символьных вычислений выводит новые заключения из тех данных, что есть. Если к решению прийти не удалось, то языковая модель предлагает новое построение (например, провести высоту треугольника). С этими новыми данными снова работает рациональный модуль и так пока решение не найдется.
Нужно ещё добавить, что помимо реализации решения AlphaGeometry синтезировали 100 миллионов примеров — случайных чертежей и всех возможных геометрических соотношений в них. Авторы также создали сет из 30 геометрических задач из реальных олимпиад с 2000 года. AlphaGeometry решила 25 из них. Все решения проверил золотой медалист Эван Чен:
“Представляется, что компьютер будет решать геометрические задачи методом грубой силы в системе координат: тонны скрупулезных алгебраических вычислений. Но AlphaGeometry не такая. Она использует классические правила геометрии, с углами и треугольниками так же, как это делают люди”.
Синтез
Но всё-таки AlphaGeometry делает это чуть хуже, чем люди. Точнее, чем умнейшие люди, завоевавшие золотые медали на IMO.
Следующий логический шаг сделали в IIIT Hyderabad, Тюбингенском университете и Кэмбридже. Авторы решили, что несмотря на прорыв AlphaGeometry, метод У рано сбрасывать со счетов (статья, код). Ведь сам по себе метод У может решить 15 задач (тут есть расхождения с авторами из DeepMind, там утверждалось что по методу У получается решить только 10 из 30 задач. Однако, это в любом случае ниже среднего “бронзового” уровня). Вместе с базой данных дедуктивных выводов (DD на графике ниже) и геометрическими соотношениями между углами, сторонами и расстояними между ними (AR) метод решает всего лишь на 4 задачи меньше, чем AlphaGeometry. К тому же, так получается решить 2 задачи, которые AG оказались не по силам. И это на обычном CPU, тратя не более 5 минут на одну задачу.
Авторы просто реализовали метод У на JGEX (Java Geometry Expert) — программе для геометрических вычислений, вручную переведя 30 олимпиадных задач в подходящий формат, а затем соединили с другими методами.
Чисто символьные вычисления (Wu+DD+AR) дают результат в 21 решённую задачу, который совпадает с AlphaGeometry до файнтюнинга. Чистый метод У на обычном ноутбуке с 16GB RAM и процессором AMD Ryzen 7 5800H решил 14 задач за 5 секунд и еще одну задачу за 3 минуты. А новый state-of-the-art — комбинация Wu и AlphaGeometry — наконец обошёл человека (точнее, умнейших из нас) — 27 решенных задач, против 25,9 у среднего золотого медалиста.
Задачи из IMO часто сравнивают с эндшпилем, когда доступно лишь небольшое число маневров, из которых как-то нужно реализовать преимущество. И играть этот эндшпиль, искусственный интеллект будет вместе с “грубой силой”.