2 августа OpenAI опубликовала результаты работы внутренней версии своей следующей модели Astra — так компания впервые официально раскрыла название следующего крупного семейства. Система решила десять открытых задач в области математики и теоретической информатики, над которыми исследователи работали как минимум десять лет, а в большинстве случаев — значительно дольше.
Задачи охватывают шесть направлений: высокоразмерная геометрия, теория кодирования, теория групп, квантовая сложность вычислений, криптография на решетках и экстремальная комбинаторика. Главный результат — первая в истории явная конструкция несофической группы, существование которой математики обсуждали с 1999 года, когда Михаил Громов ввел само понятие софичности. Это открытие может продвинуть исследования в фундаментальной теории групп.
Все десять доказательств верифицированы в системе Lean 4, сочетающей язык программирования и инструмент проверки теорем. На GitHub опубликованы 249-страничный манускрипт и машиночитаемые сертификаты по каждому из результатов — такой подход исключает ошибки при ручной записи и позволяет независимо проверить каждый шаг рассуждений.
По оценке OpenAI, на поиск всех решений ушло около 2000 долларов по тарифам API. Математик Томас Блум из Манчестерского университета назвал итоги «большой новостью» и отметил, что по значимости они превосходят майскую публикацию о контрпримере к гипотезе о единичных расстояниях. Впрочем, он призвал не воспринимать происходящее как замену людям-математикам: системы ИИ опираются на десятилетия наработок математического сообщества.
Задачи из премии тысячелетия OpenAI пока серьезно не атаковала, однако планирует продолжать эксперименты в этом направлении. Компания также обещает опубликовать подробную техническую документацию по Astra.
Ранее мы сообщали, что ИИ OpenAI опроверг гипотезу Эрдеша 1946 года — это стало первым автономным решением центральной задачи комбинаторной геометрии.
Источник новости: hi-tech.mail.ru
