Система, созданная учеными из Пекинского университета, использует два основных компонента: Rethlas, рассуждающий агент на естественном языке, и Archon, агент формализации. Rethlas обращается к поисковой системе Matlas для изучения стратегий решения, имитируя мыслительный процесс математика. Когда Rethlas находит потенциальное доказательство, Archon с помощью другой поисковой системы, LeanSearch, преобразует его в проект для интерактивного доказательства теорем Lean 4 — языка программирования с библиотекой из сотен тысяч теорем.

Ключевое отличие нового инструмента от предыдущих нейросетей для решения математических задач в том, что он не нуждается в пристальном надзоре со стороны человека, сообщает Independent. «От человека-оператора не требовалось никакого математического суждения», сообщили ученые, хотя они обнаружили, что могут ускорить процесс, если направлять работу системы Archon будет математик.

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

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

В феврале Google DeepMind представила ИИ Aletheia, построенный на базе модели Gemini Deep Think. «Алетейя» специализируется на математике и впервые смогла автономно решить несколько открытых, то есть до сих пор нерешенных математических задач.