Ааа, это прекрасно! Поскольку в Навье-Стоксе я глубоко не разбираюсь, мой самый большой консёрн был по поводу того, как они получили Lean код, подтверждающий доказательство, и как быть уверенным, что этот код строго соответствует текстовому доказательству (а код был сгенерён уже после, отдельным процессом). И вот, кажется, он не соответствует (но саму статью пока не читал): https://arxiv.org/abs/2610.08144 To demonstrate the effect of this result we provide several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean `verifications'. These include OpenAI's announced Navier-Stokes proof. In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.
gonzo-обзоры ML статей
Авторы: Гриша Сапунов, ранее руководитель разработки Яндекс-Новостей, ныне CTO Intento. Области интересов: AI/ML/DL, биоинформатика. Лёша Тихонов, ранее аналитик в Яндексе, автор Автопоэта, Нейронной Обороны... Области интересов: discrete domain, NLP, RL.
-
-
-
-
-
Вторая статья про законы скейлинга для зацикленных трансформеров (первая тут). Теперь с MoE. Scaling Laws for Looped Mixture of Experts Yanbei Chen, Anirudh Goyal, Raghuraman Krishnamoorthi Paper: https://arxiv.org/abs/2609.40316 Review: https://arxiviq.substack.com/p/scaling-laws-for-looped-mixture-of Code: N/A Model: N/A ЧТО сделали: Вывели Loop Scaling Laws — фреймворк, который совместно моделирует глубину рекуррентных циклов и разреженность Mixture-of-Experts (MoE) наряду с числом параметров и объёмом данных предобучения. Закон заменяет неограниченный рост эффективной ёмкости на функцию с насыщением, зависящую от разреженности. ЧТО получили: Ограниченная формула предсказывает лосс на отложенных тестах рекуррентности до 16 проходов с RMSE 0.0100 (против 0.2847 у линейной модели и 0.0480 у степенного закона). При равных затратах 1.5E22 FLOPs модель LoopMoE с 0.3B активных (1.3B всего) параметров и 5 проходами сопоставима с нерекуррентной MoE вдвое большего размера (0.6B активных, 2.9B всего) на GSM8K (41.2% против 42.9%) и BIG-Bench Hard (31.8% против 29.8%). ПОЧЕМУ это важно: Закон позволяет математически оптимизировать число активных весов, количество экспертов и глубину рекуррентности под жёсткие лимиты памяти устройств. Однако выигрыш в параметрической эффективности заметен в основном на задачах на рассуждение и проседает на тестах широкого кругозора. Скейлить тут: https://t.me/gonzo_ML_podcasts/4826
-
Готовятся к математикам с вилами. И не только. "Many AI industry insiders told Axios they believe a major event will occur in the next six to 12 months." https://www.axios.com/2026/10/09/ai-companies-day-after-major-attack
-
-
-
-
-
Любопытное про изменение законов скейлинга для looped моделей. Завтра ещё одну статью про это бахну. How Model Growth, Recursion, and Boundary Operators Influence Scaling Exponents Zixi Chen, Akshay Vegesna, Samip Dahal, Andrew Gordon Wilson Статья: https://arxiv.org/abs/2609.19107 Ревью: https://arxiviq.substack.com/p/how-model-growth-recursion-and-boundary Код: https://github.com/qlabs-eng/scaling-exponents ЧТО сделали: Исследовали, способны ли архитектурные изменения менять показатель степени в законах скейлинга предобучения, а не только константу. В pre-norm трансформерах изолировали граничную нормализацию, рекуррентные циклы и поэтапный рост глубины. Для каждого семейства авторы подобрали индивидуальные оптимальные по вычислениям режимы обучения. ЧТО получили: Архитектурные модификации действительно меняют показатель степени γ. У базового трансформера γ = 0.111. Добавление граничного оператора увеличивает показатель до γ = 0.114 (множитель вычислений 1.25x при 10^20 FLOPs — метрика, показывающая, во сколько раз больше вычислительного бюджета потребовалось бы стандартному бейзлайну, чтобы достичь точно такого же валидационного лосса, какой демонстрирует исследуемая модель), рост со связанными весами даёт γ = 0.116 (1.36x), а с независимыми весами — γ = 0.117 (1.55x). При экстраполяции до 1.23x10^21 FLOPs модель на 7.4B с независимым ростом показала точность 0.3865 на бенчмарке DCLM CORE из 22 задач, догнав GPT-3 13B с затратами вычислений примерно в 20 раз меньше. ПОЧЕМУ это важно: Прирост эффективности предобучения масштабируется вместе с объёмом вычислений, а не остаётся фиксированным сдвигом. Однако рост модели с независимыми весами требует динамического выделения памяти прямо посреди обучения. Двигать экспоненты тут: https://t.me/gonzo_ML_podcasts/4825
-
-
-
-
-
-
-
Что если дать модели возможность переписывать контекст? Так чтобы она работала с ним как с файлом? Простая и гениальная идея, не понимаю, почему её раньше никто не довёл в таком виде. Сплошные профиты: многие вещи из контекста не нужны после того как получен результат, запросто можно урезать лишнее ненужное и сэкономить вычислений. Да, после точки редактирования летят KV-кеши, но для неизменившейся части можно быстро пересчитать RoPE эмбеддинги и не делать полный prefill. Эта часть вообще потенциально много где полезна. Зачётная работа, респект авторам! Context Language Models Rulin Shao, Shannon Zejiang Shen, Junjie Oscar Yin, Yuetai Li, Minheng Wang, Hamish Ivison, Radha Poovendran, Nathan Lambert, Teng Xiao, Mike Lewis, Wen-tau Yih, Luke Zettlemoyer, Pang Wei Koh Paper: https://arxiv.org/abs/2609.37725 Review: https://arxiviq.substack.com/p/context-language-models Code: https://github.com/facebookresearch/context-language-models ЧТО сделали: Предложили подход Context Language Models (CLM): контекст агента хранится как редактируемый файл на диске. Модель сама читает, сжимает и переписывает его командами Bash и Python вместо внешних эвристик суммаризации. Чтобы правки в середине контекста не заставляли заново вычислять KV-кэш, авторы создали патч для SGLang — Suffix Cache Reuse (SCR), который сохраняет и перемещает кэшированные активации суффикса. ЧТО получили: В режиме zero-shot модель Qwen3.6-27B с CLM достигла точности 59.4% на BrowseComp-Plus (относительный прирост 11.4% по сравнению с 53.3% у суммаризации в духе Codex) при снижении FLOPs на 21.5%. На Software World модель показала ускорение на 65% выше при том же объёме вычислений. Пошаговый GRPO поднял точность Qwen3.5-9B с 28.8% до 42.5%, сократив FLOPs на 12%. ПОЧЕМУ это важно: Прямой доступ на запись в собственный контекст избавляет от хрупких эвристик сжатия при долгой работе агента. Однако из-за слабого ощущения размера контекста модели пока требуется внешнее напоминание о расходе токенов. Переписывать контекст здесь: https://t.me/gonzo_ML_podcasts/4824
-
-
- Older posts