Forwarded from Machinelearning
🔥 AlphaProof Nexus: формальные доказательства начинают превращаться в инженерный пайплайн
Google DeepMind показали AlphaProof Nexus - систему, которая автономно закрыла 9 открытых задач Эрдёша, часть из которых висела десятилетиями. По оценке авторов, стоимость решения одной задачи составила всего несколько сотен долларов.
Кроме этого, система доказала 44 открытые гипотезы из OEIS, закрыла 15-летний вопрос в алгебраической геометрии и нашла новый алгоритмический параметр в оптимизационной теории, который раньше не был описан людьми.
Модель генерирует идеи и фрагменты доказательств, а Lean проверяет каждый логический шаг через компилятор. Если доказательство некорректно, оно просто не проходит проверку. Не нужен рецензент, который вручную ищет дыру в рассуждении.
Базовый агент, который просто чередует генерацию LLM и обратную связь от компилятора, смог повторить все 9 успешных решений задач Эрдёша. Более сложная версия с эволюционным поиском и reinforcement learning дала заметный выигрыш только на самых тяжёлых случаях.
Чем сильнее становятся foundation models, тем чаще простые циклы «сгенерировал - проверил - исправил» начинают догонять специализированные архитектуры.
Отличие от неформального подхода к математическим доказательствам принципиальное. Модель часто придумывала несуществующие леммы, ссылалась на «известные результаты» и пыталась спрятать сложность задачи в вспомогательное утверждение. В обычном текстовом доказательстве такие ошибки легко пропустить. Lean отсекает их сразу.
Ещё один неожиданный эффект: агент находил неточности в формализациях уже существующих математических утверждений. То есть он работал не только как решатель, но и как диагностический инструмент для самой постановки задачи.
Успехи пока сосредоточены там, где библиотека Lean уже достаточно зрелая: комбинаторика, теория чисел, оптимизация. Задачи, где нужно строить большой пласт новой теории, всё ещё далеко не закрыты. И большинство задач Эрдёша система не решила.
Та же схема подходит для кодигша, спецификаций, верификации протоколов, компиляторов, криптографии.
Формальная проверка отсекает галлюцинации.
Модель может придумать лемму или сослаться на несуществующий результат, но Lean это не пропустит.
https://arxiv.org/html/2605.22763v1
@ai_machinelearning_big_data
Google DeepMind показали AlphaProof Nexus - систему, которая автономно закрыла 9 открытых задач Эрдёша, часть из которых висела десятилетиями. По оценке авторов, стоимость решения одной задачи составила всего несколько сотен долларов.
Кроме этого, система доказала 44 открытые гипотезы из OEIS, закрыла 15-летний вопрос в алгебраической геометрии и нашла новый алгоритмический параметр в оптимизационной теории, который раньше не был описан людьми.
Модель генерирует идеи и фрагменты доказательств, а Lean проверяет каждый логический шаг через компилятор. Если доказательство некорректно, оно просто не проходит проверку. Не нужен рецензент, который вручную ищет дыру в рассуждении.
Базовый агент, который просто чередует генерацию LLM и обратную связь от компилятора, смог повторить все 9 успешных решений задач Эрдёша. Более сложная версия с эволюционным поиском и reinforcement learning дала заметный выигрыш только на самых тяжёлых случаях.
Чем сильнее становятся foundation models, тем чаще простые циклы «сгенерировал - проверил - исправил» начинают догонять специализированные архитектуры.
Отличие от неформального подхода к математическим доказательствам принципиальное. Модель часто придумывала несуществующие леммы, ссылалась на «известные результаты» и пыталась спрятать сложность задачи в вспомогательное утверждение. В обычном текстовом доказательстве такие ошибки легко пропустить. Lean отсекает их сразу.
Ещё один неожиданный эффект: агент находил неточности в формализациях уже существующих математических утверждений. То есть он работал не только как решатель, но и как диагностический инструмент для самой постановки задачи.
Успехи пока сосредоточены там, где библиотека Lean уже достаточно зрелая: комбинаторика, теория чисел, оптимизация. Задачи, где нужно строить большой пласт новой теории, всё ещё далеко не закрыты. И большинство задач Эрдёша система не решила.
Та же схема подходит для кодигша, спецификаций, верификации протоколов, компиляторов, криптографии.
Формальная проверка отсекает галлюцинации.
Модель может придумать лемму или сослаться на несуществующий результат, но Lean это не пропустит.
https://arxiv.org/html/2605.22763v1
@ai_machinelearning_big_data
🔥5❤3👍3
NVIDIA официально опубликовала Skills, которые они используют для своих ИИ-агентов.
Прямо сейчас у них есть Skills для:
→ автоматического анализа и суммирования видео
→ создания голосовых агентов в реальном времени
→ обучения и улучшения LLM
→ ускорения моделей, чтобы они работали намного быстрее
→ систем RAG, подключенных к документам и данным
→ агентов, работающих в изолированных безопасных средах
→ оптимизации логистики и маршрутизации с помощью GPU
→ программирования и вычислений на CUDA
Некоторые из самых интересных:
• TensorRT-LLM → экстремальное ускорение LLM
• NeMo-RL → продвинутое обучение агентов
• Video Search → автоматический поиск и суммирование видео
Кроме того, они совместимы с:
→ Claude Code
→ OpenAI Codex
→ Cursor
https://github.com/NVIDIA/skills
Прямо сейчас у них есть Skills для:
→ автоматического анализа и суммирования видео
→ создания голосовых агентов в реальном времени
→ обучения и улучшения LLM
→ ускорения моделей, чтобы они работали намного быстрее
→ систем RAG, подключенных к документам и данным
→ агентов, работающих в изолированных безопасных средах
→ оптимизации логистики и маршрутизации с помощью GPU
→ программирования и вычислений на CUDA
Некоторые из самых интересных:
• TensorRT-LLM → экстремальное ускорение LLM
• NeMo-RL → продвинутое обучение агентов
• Video Search → автоматический поиск и суммирование видео
Кроме того, они совместимы с:
→ Claude Code
→ OpenAI Codex
→ Cursor
https://github.com/NVIDIA/skills
🔥7👍1🥰1
Основатель DeepSeek перевел весь код с NVIDIA на Huawei: зачем он это сделал и что теперь будет с китайским ИИ
Лян Вэньфэнг, основатель DeepSeek, потратил месяцы на полный перенос кодовой базы DeepSeek с чипов NVIDIA на Ascend от Huawei. Не потому что нужно было что-то исправить, а потому что он решил доказать: китайский ИИ может работать без американского железа.
DeepSeek уже показал отличные результаты на чипах NVIDIA до санкций. У компании было рабочее решение, но Вэньфэнг пошел другим путем. Проект занял месяцы, потребовал огромных ресурсов и задержал выпуск новой версии модели. Но результат стоил того.
Что получилось на выходе:
- DeepSeek полностью работает на чипах Huawei Ascend без потери качества
- Доказано, что чипы Huawei способны тянуть полноценные ИИ-нагрузки
- Другие китайские ИИ-компании теперь имеют реальный повод перейти с NVIDIA на Huawei
- Большая часть зависимости от американских поставщиков чипов убрана
Вэньфэнг нес огромное давление, сроки сдвинулись, команда работала без гарантий что выйдет рабочее решение. Но он довел дело до конца и доказал: китайская ИИ-индустрия может строить свой собственный стек, не завися от того, дадут ли следующую партию поставок через Тихий океан.
Лян Вэньфэнг, основатель DeepSeek, потратил месяцы на полный перенос кодовой базы DeepSeek с чипов NVIDIA на Ascend от Huawei. Не потому что нужно было что-то исправить, а потому что он решил доказать: китайский ИИ может работать без американского железа.
DeepSeek уже показал отличные результаты на чипах NVIDIA до санкций. У компании было рабочее решение, но Вэньфэнг пошел другим путем. Проект занял месяцы, потребовал огромных ресурсов и задержал выпуск новой версии модели. Но результат стоил того.
Что получилось на выходе:
- DeepSeek полностью работает на чипах Huawei Ascend без потери качества
- Доказано, что чипы Huawei способны тянуть полноценные ИИ-нагрузки
- Другие китайские ИИ-компании теперь имеют реальный повод перейти с NVIDIA на Huawei
- Большая часть зависимости от американских поставщиков чипов убрана
Вэньфэнг нес огромное давление, сроки сдвинулись, команда работала без гарантий что выйдет рабочее решение. Но он довел дело до конца и доказал: китайская ИИ-индустрия может строить свой собственный стек, не завися от того, дадут ли следующую партию поставок через Тихий океан.
❤38👏18🔥8🤮2🤨1
38 лет считалось, что для разреженных графов алгоритм Дейкстры почти упёрся в потолок.
Логика выглядела железно:
- Дейкстра упорядочивает вершины по расстоянию
- сортировка имеет нижнюю границу O(n log n)
- значит, кратчайшие пути быстрее искать нельзя
Но группа из 5 исследователей показала, что это ограничение можно обойти.
Идея в том, чтобы не просто «ускорить очередь с приоритетами», а смешать подход Дейкстры с динамическим программированием в стиле Беллмана-Форда. Алгоритм делит множество вершин, сжимает frontier и не тратит время на полную сортировку там, где она не нужна.
Результат:
Это первое улучшение для направленных разреженных графов со времён Fibonacci heap в 1987 году.
Tsinghua, Stanford, Max Planck. 17 страниц, которые ломают старое интуитивное объяснение про «Дейкстру быстрее нельзя».
Логика выглядела железно:
- Дейкстра упорядочивает вершины по расстоянию
- сортировка имеет нижнюю границу O(n log n)
- значит, кратчайшие пути быстрее искать нельзя
Но группа из 5 исследователей показала, что это ограничение можно обойти.
Идея в том, чтобы не просто «ускорить очередь с приоритетами», а смешать подход Дейкстры с динамическим программированием в стиле Беллмана-Форда. Алгоритм делит множество вершин, сжимает frontier и не тратит время на полную сортировку там, где она не нужна.
Результат:
O(m log^(2/3) n)Это первое улучшение для направленных разреженных графов со времён Fibonacci heap в 1987 году.
Tsinghua, Stanford, Max Planck. 17 страниц, которые ломают старое интуитивное объяснение про «Дейкстру быстрее нельзя».
🔥17❤9👍4🤣1🗿1
Проблема новичков в том, что они учат Python кусками: синтаксис, пару задач, немного теории - и потом не понимают, как собрать из этого реальный проект.
Этот курс закрывает именно этот разрыв. Здесь вы не просто смотрите уроки, а учитесь писать код, разбирать ошибки и собирать рабочие решения на практике.
Внутри:
- Python с нуля
- много практики без сухой теории
- реальные задачи и проекты
- автоматизация рутины
- работа с файлами, данными и API
- понятная логика программирования
- современная разработка с ИИ
- отдельный блок по вайбкодингу
Вайбкодинг это нормальный навык 2026 года и вас научат- правильно ставить задачу, проверять код, понимать результат и быстрее доводить проект до рабочего состояния.
48 часов скидка 60%: https://stepik.org/course/288218/
Please open Telegram to view this post
VIEW IN TELEGRAM
😭2❤1👍1🥰1💩1🫡1
Forwarded from Machinelearning
Media is too big
VIEW IN TELEGRAM
Компания изменила механизм управления rate limits для своего ИИ-агента. На тарифах Go, Plus, Pro и Business теперь можно накапливать сбросы лимитов и активировать их вручную при пиковых нагрузках. Ранее таймеры обнулялись автоматически.
На старте все подписчики получают 1 бесплатный сброс. Дополнительно запущена двухнедельная реферальная программа: клиенты на Plus и Pro могут пригласить до 3 коллег. После первого запроса от нового пользователя обе стороны получают по дополнительному сбросу в резерв.
По неофициальным данным, обновление связано с конкуренцией с Anthropic и подготовкой к снижению цен на токены для корпоративных клиентов.
OpenAI в сети Х
Серверные ARM-процессоры Vera, спроектированные для инференса автономных ИИ-агентов, стали доступны для китайских компаний. Первые поставки ожидаются в августе.
Один из локальных облачных провайдеров уже заказал более 300 серверов на базе Vera для пилотного запуска в зарубежных дата-центрах. По предварительным оценкам, стоимость одного чипа превысит $20 000, а стойка на 256 процессоров обойдется в $10 млн.
Ставка на CPU стала ответом на заморозку поставок H200. В отличие от GPU, процессоры несут меньше санкционных рисков. Массовый переход китайских компаний на новые чипы теперь зависит от адаптации программных экосистем под ARM-архитектуру.
reuters.com
Китайский техногигант представил терминального агента MiMo Code на базе OpenCode. Инструмент под лицензией MIT решает проблему потери контекста в задачах из сотен последовательных шагов.
В слепом A/B-тестировании на 474 репозиториях агента сравнили со связкой Claude Code и Sonnet. На коротких дистанциях зафиксирован паритет, но в задачах длиннее 200 шагов решение Xiaomi обошло конкурента в 65% случаев.
Архитектура MiMo Code опирается на бесконечные логические сессии. Субагент регулярно сохраняет промежуточные состояния на диск, а при исчерпании лимита токенов сессия перезапускается, загружая накопленные данные в новое окно. Память разделена на 4 уровня: от коротких локальных заметок до постоянных фактов проекта.
Установка доступна через менеджер пакетов NPM или Bash-скрипты.
xiaomi.com
Согласно иску, группа Outsider Enterprise разработала 131 инструмент для потоковой генерации копий сайтов Google, YouTube и госструктур США. За две недели Android-пользователи получили 2,5 млн сообщений, содержащих 1 млн фишинговых ссылок. Инфраструктура координировалась через Telegram.
Google выступает в суде совместно с ФБР и телеком-операторами AT&T, T-Mobile и Verizon. Истцы требуют судебного запрета для создания правового механизма, который позволит оперативно блокировать домены и замораживать счета сети.
Размер ущерба по делу не раскрывается.
blog.google
Nature Medicine опубликовал исследование, которое показало, что универсальные LLM превосходят профильные клинические ИИ-инструменты.
В слепом тестировании (12 врачей, 1800 реальных запросов) Gemini 3.1 Pro и GPT-5.2 набрали 97,4% и 94,2% точности соответственно. Результаты спецсистем OpenEvidence и UpToDate Expert AI составили около 80%.
Авторы объясняют отставание профильных решений сильной зависимостью от RAG - нерелевантная литература и ошибки интеграции снижают качество генерации. Универсальные модели выигрывают за счет масштаба, кросс-доменного обучения и механизмов логического вывода.
Медицинские системы также продемонстрировали операционные проблемы. OpenEvidence выдавал хаотичные ответы, а UpToDate Expert AI отклонил 19% запросов из-за жестких фильтров безопасности. Частота галлюцинаций базовых LLM не превысила показатели профильных аналогов.
Авторы рекомендуют клиникам проводить независимое тестирование ИИ-продуктов перед внедрением.
nature.com
@ai_machinelearning_big_data
#news #ai #ml
Please open Telegram to view this post
VIEW IN TELEGRAM
❤2👍1🔥1
🍺 В этот день 150 лет назад родился Уильям Сили Госсет.
Всю карьеру он проработал пивоваром в Guinness и занимался задачей, которую учебники почти не трогали: как делать выводы по крошечным выборкам — например, по четырём участкам ячменя или небольшой партии хмеля.
Статистика того времени в основном исходила из больших выборок, поэтому Госсет фактически изобрёл статистику для малых.
Guinness запрещала сотрудникам публиковаться после того, как один из них слил коммерческие секреты. Компания также не хотела, чтобы конкуренты знали: пиво там варят с помощью науки.
Поэтому, когда Госсет в 1908 году опубликовал свой метод, он подписался псевдонимом: Student.
Каждое клиническое испытание, лабораторный эксперимент и A/B-тест, где сегодня используют t-test, опирается на работу Student.
Одна из самых известных фамилий в статистике - ненастоящая.
Всю карьеру он проработал пивоваром в Guinness и занимался задачей, которую учебники почти не трогали: как делать выводы по крошечным выборкам — например, по четырём участкам ячменя или небольшой партии хмеля.
Статистика того времени в основном исходила из больших выборок, поэтому Госсет фактически изобрёл статистику для малых.
Guinness запрещала сотрудникам публиковаться после того, как один из них слил коммерческие секреты. Компания также не хотела, чтобы конкуренты знали: пиво там варят с помощью науки.
Поэтому, когда Госсет в 1908 году опубликовал свой метод, он подписался псевдонимом: Student.
Каждое клиническое испытание, лабораторный эксперимент и A/B-тест, где сегодня используют t-test, опирается на работу Student.
Одна из самых известных фамилий в статистике - ненастоящая.
❤27👍7🔥4🍾3
Альберт Эйнштейн однажды сказал:
Анри Пуанкаре спросил:
Эйнштейн ответил:
Пуанкаре улыбнулся и сказал:
Эйнштейн заинтересовался:
Пуанкаре ответил:
Этот обмен остроумно показывает разницу во взглядах двух великих умов: физика ищет важное в реальности, математик — истину внутри важного.
«Знаешь, Анри, я начинал с математики, но в итоге ушёл в физику».
Анри Пуанкаре спросил:
«Почему?»
Эйнштейн ответил:
«Потому что я мог отличать истинные утверждения от ложных, но не мог понять, какие из них действительно важны».
Пуанкаре улыбнулся и сказал:
«Забавно, Альберт. А я начинал с физики, но в итоге выбрал математику».
Эйнштейн заинтересовался:
«И почему ты сделал такой выбор?»
Пуанкаре ответил:
«Потому что я не мог понять, какие из важных фактов на самом деле истинны».
Этот обмен остроумно показывает разницу во взглядах двух великих умов: физика ищет важное в реальности, математик — истину внутри важного.
❤24👍9🔥5💩2