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

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

Юхуай Ву (Yuhuai Wu) из компании Google и его коллеги использовали нейронную сеть под названием Codex, созданную исследовательской компанией OpenAI. Она была обучена на большом количестве текстовых и программных данных из Интернета и может быть использована программистами для создания работоспособного кода.

Языки доказательств имеют сходство с языками программирования, поэтому исследователи решили проверить, сможет ли Codex формализовать банк из 12,5 тыс. задач по математике для средней школы. Данная нейронная сеть смогла перевести четверть всех задач в формат, совместимый с программой для решения формальных задач на основе доказательств под названием Isabelle. По словам Ву, многие из неудачных переводов были результатом того, что система не понимала определенных математических концепций: "Если показать модели пример, объясняющий эту концепцию, она быстро ее усвоит".

Чтобы проверить эффективность этого процесса автоформализации, команда исследователей применила Codex к набору задач, которые уже были формализованы людьми. Codex создала свои собственные формальные версии этих задач, а специалисты использовали другой ИИ под названием MiniF2F для решения обеих версий.

Автоматически формализованные задачи повысили процент успеха MiniF2F с 29% до 35%, что говорит о том, что Codex лучше справилась с формализацией этих задач, чем человек.

Это небольшое улучшение, но Ву говорит, что работа специалистов является лишь доказательством концепции. "Если цель состоит в том, чтобы обучить машину, способную решать математические задачи на том же уровне, что и лучшие специалисты, то автоматическая формализация, похоже, является очень важным путем к этому", – говорит Ву.

По словам одного из членов команды – Альберта Цзяна (Albert Jiang) из Кембриджского университета, – дальнейшее повышение коэффициента успешности позволит искусственному интеллекту конкурировать с людьми-математиками. "Если мы достигнем 100%, мы определенно создадим искусственный интеллект, способный выиграть золотую медаль Международной математической олимпиады", – говорит он, имея в виду главный приз на одном из ведущих математических соревнований.

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

Способность такой машины к рассуждениям может также сделать ее подходящей для задач проверки в самых разных областях. "Вы можете проверить, выполняет ли программа именно то, что вы от нее требуете, или проверить аппаратные чипы, так что это может найти применение в алгоритмах финансовой торговли и проектировании оборудования", – говорит Цзян.

По словам Янг-Хуи Хэ (Yang-Hui He) из Лондонского института математических наук, такая возможность использования машин для поиска новой математики является захватывающей, но настоящая сложность будет заключаться в использовании модели в математических исследованиях, большая часть которых написана в LaTeX – системе компьютерной верстки. "Мы используем LaTeX только потому, что в нем удобно печатать, но в каком-то смысле это естественный язык, у него свои правила", – говорит Хэ.

Пользователи могут задавать в LaTeX свои собственные функции и символы, которые могут использоваться только в одной математической работе, что может оказаться сложным для нейронной сети, обученной только на обычном тексте, считает Хэ.

Алекс Уилкинс