Традиционно математические исследования включают небольшое число профессиональных математиков, работающих над сложными задачами. Однако я давно считаю, что существует дополнительный способ заниматься математикой, при котором можно работать с широким сообществом людей, склонных к математике, над задачами, которые могут быть не такими глубокими, как те, над которыми традиционно работают, но всё равно представляют математический интерес. Современные технологии, включая искусственный интеллект, больше подходят для такого типа работы.
Примером такого широкого сотрудничества являются проекты «Polymath», в которых интернет-платформы, такие как блоги и вики, использовались для облегчения сотрудничества. Несколько лет спустя в некоторых кругах стали популярны совместные проекты по формализации (например, проект по формализации гипотезы Фремана–Ружи о многочленах Мартона, обсуждавшейся ранее в этом блоге). А в 2024 году я запустил проект «Equational Theories Project» (ETP), сочетающий строгость формализации Lean с «старым добрым искусственным интеллектом» (в форме автоматизированных средств доказательства теорем) для решения более 22 миллионов задач по универсальной алгебре, имеющих ответы «истина» или «ложь».
Новый проект
Мы с Дамеком Дэвисом запускаем новый проект в форме экспериментального конкурса, организованного фондом SAIR (где я являюсь членом правления и который оказывает техническую поддержку и вычислительные ресурсы). Идея этого конкурса, частично вдохновлённая недавней статьёй Хонды, Мураками и Чжана, заключается в том, чтобы измерить, насколько 22 миллиона результатов универсальной алгебры, полученных в ETP, могут быть «переработаны» в краткую, удобочитаемую «шпаргалку», подобную той, которую студент на первом курсе математического факультета может переработать в один лист бумаги, который разрешено принести на экзамен.
Задача 1
Предположим, что — это бинарная операция, такая что для всех . Верно ли, что для всех ?
Такую задачу можно решить либо путём алгебраических преобразований исходного уравнения для вывода целевого уравнения, либо путём поиска контрпримера к целевому уравнению, который всё равно удовлетворяет исходному уравнению. Существует множество методов для достижения любой из этих целей, но такие задачи сложны, а в некоторых случаях даже неразрешимы (подробнее об этом в статье участников ETP). Тем не менее многие из этих задач могут быть решены людьми, автоматизированными системами доказательства теорем или передовыми системами искусственного интеллекта.
Однако, подобно тому, как студент, испытывающий трудности с материалом для математического класса, может лучше сдать экзамен, если ему дадут правильное руководство, оказывается, что такие дешёвые модели могут работать по крайней мере умеренно лучше на этой задаче (с вероятностью успеха около 55–60 %), если им дать правильную подсказку или «шпаргалку».
Конкурс, запущенный сегодня, требует от участников разработать «шпаргалку» (размером не более 10 килобайт), которая может максимально повысить производительность этих моделей при решении вышеуказанных задач с ответами «истина» или «ложь». Мы предоставили «площадку», на которой можно протестировать свою «шпаргалку» (или небольшое количество примеров «шпаргалок») на нескольких дешёвых моделях на общедоступном наборе из 1200 задач (1000 из которых были выбраны случайным образом и довольно просты, вместе с 200 «сложными» задачами, которые были выбраны, чтобы противостоять более очевидным стратегиям решения этих вопросов). Краткое видео, объясняющее, как пользоваться площадкой, можно найти здесь.
Конкурс будет координироваться на этом канале Zulip, где, я надеюсь, будет оживлённая и информативная дискуссия.
SAIR также запустит несколько других математических конкурсов в ближайшие месяцы, которые будут носить более кооперативный характер, чем этот конкретный соревновательный конкурс. Следите за дальнейшими объявлениями.