«Апостериори»: Искусственный интеллект впервые самостоятельно открыл математические теоремы без помощи человеческих знаний
Новости науки и технологий
Поддержите «Эхо», если вы не в России
Исследователи из Токийского университета и японского института RIKEN разработали систему искусственного интеллекта, которая способна создавать новые математические теоремы, начиная только с набора аксиом и правил вывода. В отличие от большинства современных ИИ-систем для решения математических задач, она не использовала готовые библиотеки теорем, учебники или примеры человеческих доказательств.
Сегодня многие модели искусственного интеллекта уже умеют решать сложные математические задачи. Например, большие языковые модели могут создавать доказательства на естественном языке, а специализированные системы способны работать с формальными доказательствами в таких средах, как Lean. Однако обычно такие системы опираются на огромный объём знаний, созданных людьми: математические тексты, программный код или базы уже доказанных теорем. Это затрудняет ответ на вопрос, может ли ИИ самостоятельно развивать математическое знание, начиная только с фундаментальных правил.
В новом исследовании учёные проверили эту идею на очень простой, но полностью формальной математической системе – системе аксиом Гильберта для классической логики высказываний. Она состоит всего из трёх аксиом и одного правила вывода – Modus Ponens. Это правило позволяет получить утверждение Y, если уже доказаны утверждения X и X → Y. Любое доказательство в такой системе можно проверить строго и однозначно.
Работа алгоритма напоминает процесс обучения через собственные открытия. Сначала система случайно исследовала пространство возможных доказательств. Если в процессе поиска она получала новую формулу, которая следовала из аксиом, эта формула считалась новой теоремой.
Затем найденные утверждения использовались как новые цели для поиска и как примеры для обучения самой системы.
Кроме того, исследователи добавили механизм отбора наиболее полезных открытий. Система сохраняла не все найденные формулы, а только те, которые были достаточно общими и при этом сложными для повторного доказательства. Такие теоремы превращались в новые леммы – готовые строительные блоки, которые можно было использовать при доказательстве следующих утверждений.
В результате за несколько поколений система построила собственную библиотеку математических знаний. После шести циклов обучения в библиотеку было добавлено 38 новых теорем, которые стали частью процесса доказательства. Общее количество найденных системой теорем достигло десятков тысяч.
Но главный вопрос заключался не в количестве найденных формул, а в том, имеют ли они реальную математическую ценность. Поэтому авторы проверили систему на 30 задачах из классического учебника по математической логике. Автоматически найденные теоремы позволили решить около 30% этих задач, что показывает: система обнаруживала не просто случайные истинные утверждения, а некоторые полезные математические структуры.
Исследователи также проверили, смогут ли эти открытия помочь другим моделям искусственного интеллекта. Они передали найденные теоремы большим языковым моделям в качестве дополнительных лемм. В результате точность построения формальных доказательств у нескольких моделей выросла. Это означает, что математические знания, найденные одной системой, могут использоваться другой системой как внешний источник информации.
При этом авторы подчёркивают, что до настоящего математического творчества человека пока ещё далеко. Эксперимент проводился только в одной небольшой логической системе, и неизвестно, сможет ли такой подход работать в более сложных областях – например, в теории множеств, алгебре или математическом анализе.
Тем не менее работа показывает новый возможный путь развития математического искусственного интеллекта: системы могут не только использовать созданные людьми знания, но и постепенно расширять собственную формальную базу знаний, сохраняя при этом возможность строгой проверки каждого открытия.