Главное

  • Intern-S2 прошла полный цикл работы: от анализа литературы и поиска идей до проверки логических шагов.
  • Две группы исследователей Пекинского университета формализовали доказательство с помощью системы SHEAF.
  • Шанхайская лаборатория ИИ планирует превратить этот процесс в многоразовый модуль для научных исследований.

Как модель участвовала в доказательстве

Intern-S2 разработала Шанхайская лаборатория ИИ, разработчик большой языковой модели. Её использовали как научного помощника.

Модель изучила профильную научную литературу и разделила утверждение на отдельные задачи. Затем она параллельно проверяла разные варианты доказательства и искала возможные решения.

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

Учёные дорабатывали структуру доказательства и принимали ключевые решения. Они также давали модели обратную связь для дальнейшего поиска.

Что удалось доказать

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

Задача долгое время оставалась нерешенной. В проекте её также рассматривали как проверку способности ИИ работать с математическими рассуждениями.

Формализацией доказательства занялись две группы исследователей Пекинского университета. Они использовали собственную систему SHEAF для проверки доказательства в формальном виде.

В ходе проекта Intern-S2 прошла весь рабочий цикл вместе с исследователями. Китайские учёные впервые решили математическую задачу мирового уровня с помощью нейросети местной разработки.

ИИ хотят использовать в других исследованиях

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

Платформа объединяет модель Intern-S2, агентов ИИ, данные и настоящее экспериментальное оборудование. Модель должна проверять разные этапы научного поиска в реальных исследованиях.

В одном из проектов такая платформа уже помогла сократить цикл разработки в электрохимическом синтезе с 5-10 до 1-2 лет. Авторы считают, что подход можно применять в физике, химии, биологии и смежных областях.

Ранее OpenAI заявила о решении задачи о существовании и гладкости решений уравнений Навье и Стокса. Компания также заявила более чем о 100 других открытых математических задачах.

Эти заявления вызвали споры среди учёных. Двадцать пять лауреатов Филдсовской премии предупредили о рисках для математических исследований.

Позднее исследователи обнаружили расхождения между текстовым доказательством OpenAI и его формализованной версией.

Подробности: 3DNews