Исследовательская группа Seed компании ByteDance официально выпустила Seed Prover 1.5, модель, специально разработанную для формальных математических рассуждений. Новая версия знаменует собой значительный скачок в решении задач олимпиадного уровня.
По данным команды, Seed Prover 1.5 сгенерировала полный, компилируемый код доказательства Lean для первых пяти задач Международной математической олимпиады (IMO) 2025 года за 16,5 часов. При преобразовании в систему оценок IMO модель набрала 35 из 42 баллов, что соответствует историческому проходному баллу для получения золотой медали.
По сравнению со своим предшественником, Seed Prover 1.5 демонстрирует существенное улучшение в обработке сложных формальных доказательств. Команда опубликовала технический отчет и объявила о планах открытия доступа к API, приглашая исследователей в области математики и искусственного интеллекта протестировать модель и внести свой вклад в развитие пересечения формальной математики и искусственного интеллекта.
Источник: AI daily
(*) Имейте ввиду: редакции некоторых изданий могут придерживаться предвзятых взглядов в освящении новостей.
8/8
Автор – Pandaily
