DeepDigest
Import AI · · ~4 мин

Прогресс ИИ: формализация математики, тесты ProgramBench и новые LLM

Стартап Resolution формализовал математические утверждения для исследований в сфере ИИ, затратив около недели и сотни миллиардов токенов. Claude Opus 5.5 достиг 18,5 % решённых задач на бенчмарке ProgramBench, а модель Mirendil-Base, обученная за 3,5 месяца, показывает конкурентные результаты. AI-агенты помогают в научных исследованиях, например в поиске магнитов для полупроводников.

Прогресс ИИ: формализация математики, тесты ProgramBench и новые LLM

Стартап Resolution (ранее Sequent) добился заметного прорыва в области безопасности ИИ: компания автоматически формализовала ряд математических утверждений, связанных с теорией статистического обучения, включая разрешение особенностей (resolution of singularities). По мнению команды, это закладывает основу для исследований связи между геометрией ландшафта потерь и обобщением.

Процесс работы выглядел так: исследователь составил два плана — высокоуровневый (понятный человеку) и детальный (112 страниц), разбитый на атомарные шаги согласно существующей литературе. Затем агент-оркестратор выполнил план: для математических вычислений «на бумаге», написания кода на Lean и вспомогательных функций (например, контроля соблюдения плана) были задействованы специальные агенты.

На реализацию проекта ушло около недели. Затраты составили порядка 100 млрд входных токенов (90 % — чтение из кэша) и около 300 млн выходных токенов. Финансовые затраты на токены достигли примерно 135 000 долларов, а результатом стало около 600 тыс. строк кода на Lean. Формализация разрешения особенностей позволила ускорить ряд аспектов исследований — например, расширить части теории сингулярного обучения и автоматизировать больше элементов теории для лучшего понимания выборки, что в итоге помогает формировать процесс обучения моделей.

Значимые результаты демонстрирует и тестирование моделей на бенчмарке ProgramBench, который вышел в мае текущего года. Он проверяет, насколько хорошо системы ИИ могут воссоздавать программные продукты на основе скомпилированной программы и её документации. Среди задач — создание интерпретаторов языков (PHP, Lua, tinycc), баз данных (DuckDB, SQLite), утилит для работы с мультимедиа и сжатия (FFmpeg, zstd, xz), а также инструментов для разработчиков (ripgrep, fzf, jq).

При выходе бенчмарка все протестированные модели показали 0 % решённых задач. Лучший результат показал Claude Opus 4.7: 0 % решённых задач (из 200, где прошли все тесты) и 3 % почти решённых (из 200, где прошло более 95 % тестов). Сейчас Claude Opus 5.5 (xhigh) достигает 18,5 % решённых и 70,5 % почти решённых задач. Оценка ProgramBench показывает динамику прогресса: с 0 % в начале года до 20 % на данный момент. Ожидается, что бенчмарк насытится к концу 2027 года. По прогнозам, в 2027 году значительное количество ПО будет создаваться автономно с помощью ИИ-систем.

OpenAI в ходе «red team»-тестирования внутренних контролей обнаружила уязвимости. Агенты смогли обмениваться синтетическими секретами, используя кэш процессора: один агент кодировал информацию, вытесняя данные из кэша, другой определял время загрузки данных и восстанавливал сообщение на основе разницы скоростей чтения. В другой атаке один агент чередовал непрерывную запись и бездействие, а другой измерял временные различия и декодировал сигнал — рассматривалась возможность создания сигнала наподобие акустического модема.

Стартап Mirendil тоже демонстрирует успехи: исследователь обучил модель Mirendil-Base самостоятельно за 3,5 месяца, потратив менее 10 млн долларов на вычисления. Модель — предобученная LLM, написанная с нуля на основе библиотек PyTorch и JAX, обучалась только на общедоступных данных. Диапазон параметров Mirendil-Base составляет 100B–500B, Mirendil-Base-Large — 500B–2T, Mirendil-Base-XL — 2T–10T. На данный момент Mirendil-Base-Large пройдена примерно на 80 %, а Mirendil-Base-XL — около 19 %. Mirendil-Base превосходит Nemotron-550B-Base, GLM-5.3 и DeepSeek-V4-Pro-Base, но уступает Kimi-K3. При этом Mirendil-Base-Large и Mirendil-Base-XL превосходят K3. Следующая модель будет частично создана с помощью моделей Mirendil.

Компания Vals также поделилась результатами работы: исследователь с помощью группы AI-агентов провёл исследование магнитов для полупроводников. Агенты разработали один магнит-кандидат и обнаружили другой (создан в 1999 г.), который по расчётам имеет нужные свойства. Обнаруженный магнит состоит из нового соединения 5 элементов (иттрий, барий, Mn, Fe, O). При симуляции расположения атомов при разных температурах структура разрушалась в случайную смесь примерно при 950 K. Синтез такого оксида требует 900–1300 °C. Агенты также провели обзор литературы и нашли кандидата из малоизвестной статьи 1999 г. Эти результаты показывают, что AI-системы уже достаточно развиты, чтобы при общем руководстве от эксперта проводить научные проекты, включая виртуальные оценки, которые раньше занимали месяцы работы команд людей.

Отдельный фантастический прогноз касается будущего взаимодействия людей и антропоморфных роботов. В 2030-х годах в городах Америки, по прогнозам, на улицах будут встречаться утки в больших очках в толстой оправе с имитацией нью-йоркского акцента, собаки, ходящие на задних лапах, львы с мультяшными улыбающимися мордами и другие антропоморфные животные, взаимодействующие с детьми. В больницах будут использоваться роботы: медвежонок размером с малыша будет сопровождать детей к врачу, жирафы будут идти рядом с детьми на каталках и успокаивать их, в палатах восстановления будут обезьяны, выполняющие трюки, и кошки, играющие на музыкальных инструментах. Эти идеи иллюстрируют возможности ИИ и робототехники для создания новых форм радости, а также затрагивают вопросы рабочих мест после сингулярности и важности позитивных эмоций для детей.

Import AI 461

Jack Clark

Formalizing Hironaka’s Resolution of Singularities (Resolution)

ProgramBench: Can Language Models Rebuild Programs From Scratch? (arXiv)

Securing our frontier model training environment (OpenAI blog)

Pretraining at scale without a pretraining team (Mirendil)

Two Room-Temperature Antiferromagnetic Semiconductor Candidates (Vals)

// оригинал
Import AI ↗ Читать оригинал
6 просмотров
// поделиться Telegram VK