Ex-Google, OpenAI создали лаборатории по синтезу и анализу материалов с ИИ
Стартап Periodic Labs(о них писали тут) рассказал как роботизированные лаборатории ставят эксперименты и генерируют свежие данные, а модели учатся на этих данных, а потом подсказывают, что экспериментировать дальше
Их основной продукт сегодня - модель Neon, созданная на основе Kimi K2.6, которую дообучили на данных из собственных физических лабораторий
На их внутреннем бенчмарке модель превосходит GPT-6 Astra и Claude Fable 5.1 на основной научной задаче при меньших вычислительных затратах: 1.300 GPU H200
С помощью Neon они автоматизировали анализ рентгеновской дифракции (XRD)
Раньше на один сложный образец уходили часы работы учёного, а сейчас Neon делает все сама
Periodic Labs хотят научить не только разбирать результаты, но и управлять научными проектами: придумывать процедуры синтеза и решать, какие эксперименты запускать следующими
Их цель - наука на каждый час GPU
И у них есть актив - данные, которые производит физическая лаборатория
Стартап Periodic Labs(о них писали тут) рассказал как роботизированные лаборатории ставят эксперименты и генерируют свежие данные, а модели учатся на этих данных, а потом подсказывают, что экспериментировать дальше
Их основной продукт сегодня - модель Neon, созданная на основе Kimi K2.6, которую дообучили на данных из собственных физических лабораторий
На их внутреннем бенчмарке модель превосходит GPT-6 Astra и Claude Fable 5.1 на основной научной задаче при меньших вычислительных затратах: 1.300 GPU H200
С помощью Neon они автоматизировали анализ рентгеновской дифракции (XRD)
Раньше на один сложный образец уходили часы работы учёного, а сейчас Neon делает все сама
Periodic Labs хотят научить не только разбирать результаты, но и управлять научными проектами: придумывать процедуры синтеза и решать, какие эксперименты запускать следующими
Их цель - наука на каждый час GPU
И у них есть актив - данные, которые производит физическая лаборатория
Periodic
Building Labs that Learn – Periodic Labs
Introducing Periodic Neon, a 1T parameter model that we post-trained to analyze experimental results and deployed to our physical labs. This is a step towards putting autonomous discovery into the hands of scientists.
Так, кажется, все, кто мог, уже написали TypeSafe
И восторги от простых пользователей и журналистов, и "а что тут нового-то?" от прожжённых ML-щиков
Почему это интересно? Потому что в центре стоит System 1, т.е. тот факт, что модель модель встраивать в процессы реального времени
Т.е. заходит на территорию Моделей Мира с необычной стороны
Причём для обыденных массовых ынтерпрайз задач, которые сейчас выполняются LLM'и
Гениальность тут в том, что ребята нашли задачу, про которую все AI автоматизаторы плакали, кололись, но продолжали жрать LLM и выкатили для неё хорошо продуманное решение с кучей примеров и готовых работ
Даёшь больше моделей без авторегресионной генерации текста
И восторги от простых пользователей и журналистов, и "а что тут нового-то?" от прожжённых ML-щиков
Почему это интересно? Потому что в центре стоит System 1, т.е. тот факт, что модель модель встраивать в процессы реального времени
Т.е. заходит на территорию Моделей Мира с необычной стороны
Причём для обыденных массовых ынтерпрайз задач, которые сейчас выполняются LLM'и
Гениальность тут в том, что ребята нашли задачу, про которую все AI автоматизаторы плакали, кололись, но продолжали жрать LLM и выкатили для неё хорошо продуманное решение с кучей примеров и готовых работ
Даёшь больше моделей без авторегресионной генерации текста
typesafe.ai
Home - TypeSafe AI
TypeSafe AI is an AI lab building machine-native intelligence infrastructure for automation, designed to make decisions within software. Try our first System One Model, Jev, in early access.
«Учить надо не вычислениям, а моделированию» — о письме филдсовских лауреатов
25 лауреатов медали Филдса опубликовали письмо о будущем математики
Без живых математиков оборвётся человеческая цепочка передачи знания
Похожие проблемы ждут все интеллектуальные профессии
Вместо текущего результата, когда математика рассматривается как инструмент для вычислений, нужно обучать математике как инструменту моделирования — ситуаций деятельности и окружающего мира
Классическое обучение через теоремы и задачники обесценивается
В отношении математики этот процесс начался в США ещё в 1970-е, с массовым распространением калькуляторов
По меркам России больше половины выпускников американских школ сегодня фактически не знают математику
Самая большая глупость — делать то же самое и надеяться на другой результат
Тем, кто действительно берёт на себя ответственность за образовательный результат, необходимо изучать существующие практики, обмениваться опытом, включаться в сообщества
Нужно решать задачи, готового решения которых, еще не существует
25 лауреатов медали Филдса опубликовали письмо о будущем математики
Без живых математиков оборвётся человеческая цепочка передачи знания
Похожие проблемы ждут все интеллектуальные профессии
Вместо текущего результата, когда математика рассматривается как инструмент для вычислений, нужно обучать математике как инструменту моделирования — ситуаций деятельности и окружающего мира
Классическое обучение через теоремы и задачники обесценивается
В отношении математики этот процесс начался в США ещё в 1970-е, с массовым распространением калькуляторов
По меркам России больше половины выпускников американских школ сегодня фактически не знают математику
Самая большая глупость — делать то же самое и надеяться на другой результат
Тем, кто действительно берёт на себя ответственность за образовательный результат, необходимо изучать существующие практики, обмениваться опытом, включаться в сообщества
Нужно решать задачи, готового решения которых, еще не существует
Ответка от математиков к OpenAI прилетела - задача тысячелетия не решена, по которой OpenAI отчитались, что решили
Группа из 3-х специалистов по математической гидродинамике:Питер Константин, Принстон, Михаэла Игнатова, Темпл, и Влад Викол, Курантовский институт при NYU опубликовали ответный анализ на громкое заявление OpenAI, что задача тысячелетия Навье-Стокса решена
8 сентября OpenAI опубликовала препринт своего решения, в котором заявила, что доказала возможность образования сингулярности (разрыва/«взрыва» решений) за конечное время для трехмерных уравнений Навье-Стокса при наличии некоторой гладкой внешней силы
Математики в своей работе доказали, что «взрыв» у OpenAI происходит не из-за физических свойств самой жидкости, а из-за крайне специфической внешней силы, которой ученые OpenAI подталкивали поток
Это похоже на то, как если бы систему раскачивали искусственно созданными микро толчками
Ученые доказали, что если сделать эту внешнюю силу естественной и гладкой или вообще её убрать, то никакого «взрыва» не будет, вязкость жидкости легко гасит все возмущения
Таким образом OpenAI не решила задачу тысячелетия
Группа из 3-х специалистов по математической гидродинамике:Питер Константин, Принстон, Михаэла Игнатова, Темпл, и Влад Викол, Курантовский институт при NYU опубликовали ответный анализ на громкое заявление OpenAI, что задача тысячелетия Навье-Стокса решена
8 сентября OpenAI опубликовала препринт своего решения, в котором заявила, что доказала возможность образования сингулярности (разрыва/«взрыва» решений) за конечное время для трехмерных уравнений Навье-Стокса при наличии некоторой гладкой внешней силы
Математики в своей работе доказали, что «взрыв» у OpenAI происходит не из-за физических свойств самой жидкости, а из-за крайне специфической внешней силы, которой ученые OpenAI подталкивали поток
Это похоже на то, как если бы систему раскачивали искусственно созданными микро толчками
Ученые доказали, что если сделать эту внешнюю силу естественной и гладкой или вообще её убрать, то никакого «взрыва» не будет, вязкость жидкости легко гасит все возмущения
Таким образом OpenAI не решила задачу тысячелетия
Anthropic готовятся выпускать новую модель, которая составит конкуренцию Astra
Сейчас тестирует безопасность модели, и выйти она совсем скоро.
Прошла всего неделя с момента, когда настаивали на замедлении прогресса AI…
Сейчас тестирует безопасность модели, и выйти она совсем скоро.
Прошла всего неделя с момента, когда настаивали на замедлении прогресса AI…
This media is not supported in your browser
VIEW IN TELEGRAM
Digit от Agility Robotics устраивается в формованном отсеке, специально приспособленном под форму его тела
Робот держит в руках свой собственный зарядный кабель — так, как инженеру было удобно его держать
Вся сцена удивительно человечна, и как бы показывает дальнейшее направление и специализацию робототехники
Роботы на складах обычно запихиваются в какой-нибудь уголок без малейшего внимания к их внешнему виду
Здесь же явно кто-то специально спроектировал это так, чтобы оно интересно смотрелось и на home movie
Робот держит в руках свой собственный зарядный кабель — так, как инженеру было удобно его держать
Вся сцена удивительно человечна, и как бы показывает дальнейшее направление и специализацию робототехники
Роботы на складах обычно запихиваются в какой-нибудь уголок без малейшего внимания к их внешнему виду
Здесь же явно кто-то специально спроектировал это так, чтобы оно интересно смотрелось и на home movie
«Astra действительно достигла чего-то такого, что заставляет меня сказать: ладно, я думаю, это вполне разумно назвать AGI»
Год назад «AGI» было словом на будущее, а теперь президент OpenAI использует его в настоящем времени, и уже говорит о том, чтобы его замедлить
Год назад «AGI» было словом на будущее, а теперь президент OpenAI использует его в настоящем времени, и уже говорит о том, чтобы его замедлить
This media is not supported in your browser
VIEW IN TELEGRAM
166.700 нейронов из мозга самца дрозофилы учат пару силиконовых губ, стальной каркас, силиконовый язык, ряд моторов под челюстью и микрофон, направленный прямо в рот, без единого динамика где-либо, говорить
Воздух проталкивается через искусственные голосовые связки, моторы сгибают губы, а микрофон улавливает каждый звук, который они издают
Если тон сбивается, моторы корректируются перед следующей попыткой
Никто не программировал слова: он находит каждую форму губ методом проб и ошибок и использует старые звуки, чтобы угадывать новые
Младенцы учатся говорить точно так же: лепечут, слушают, исправляют, повторяют
Новое здесь — мозг в углу экрана, с 166.700 нейронами и 125.000.000 синапсов, упакованными в нечто меньше макового семечка
Ученые потратили 10 лет, чтобы отобразить каждый провод, и на работу ушло 44 года человеческого труда
Самцы дрозофил уже поют: они жужжат одним крылом, чтобы ухаживать за самкой, и она слышит песню через свои антенны
Эта песня никогда раньше не имела рта
Обученный линейный считыватель превращает его всплески в слова, а рот делает остальное
Человеческому детёнышу понадобилось 86.000.000.000 нейронов и 12 месяцев, чтобы сказать «мама»
Воздух проталкивается через искусственные голосовые связки, моторы сгибают губы, а микрофон улавливает каждый звук, который они издают
Если тон сбивается, моторы корректируются перед следующей попыткой
Никто не программировал слова: он находит каждую форму губ методом проб и ошибок и использует старые звуки, чтобы угадывать новые
Младенцы учатся говорить точно так же: лепечут, слушают, исправляют, повторяют
Новое здесь — мозг в углу экрана, с 166.700 нейронами и 125.000.000 синапсов, упакованными в нечто меньше макового семечка
Ученые потратили 10 лет, чтобы отобразить каждый провод, и на работу ушло 44 года человеческого труда
Самцы дрозофил уже поют: они жужжат одним крылом, чтобы ухаживать за самкой, и она слышит песню через свои антенны
Эта песня никогда раньше не имела рта
Обученный линейный считыватель превращает его всплески в слова, а рот делает остальное
Человеческому детёнышу понадобилось 86.000.000.000 нейронов и 12 месяцев, чтобы сказать «мама»
Все, что нужно знать о развитии AML сегодня: CEO Shopify переделал винный погреб в серверную
В холодильнике для вина теперь охлаждаются GPU: по виду там как минимум Dell Pro Max с GB300, RTX PRO 2000, 16TB NVMe и Dual 400GbE
Можно запустить GLM
В холодильнике для вина теперь охлаждаются GPU: по виду там как минимум Dell Pro Max с GB300, RTX PRO 2000, 16TB NVMe и Dual 400GbE
Можно запустить GLM
Пифагора знают все, и большинство полагает, что Пифагор был первым, кто доказал эту теорему, но на самом деле, вавилоняне использовали так называемые "теоремы Пифагора" еще за 1000 лет до его рождения
Они даже записали эту теорему на табличке, теперь известной как "Плимптон 322"
Они даже записали эту теорему на табличке, теперь известной как "Плимптон 322"
Forwarded from ARI MENSA
В Vals AI запустили 10 агентов Claude Opus 5.5, которые за 15 часов и 733 сообщения разработали алгоритм C-HD для поиска кратчайших путей в ориентированных графах
Для графов с определённой плотностью сложность снизилась с O(n log n) у Дейкстры до O(n log¹¹⁄¹² n). Корректность и оценка времени работы формально подтверждены доказательством в Lean
Но это пока теоретический результат
Алгоритм не тестировали на крупных реальных графах, константы велики, а улучшение действует только в ограниченном диапазоне входных данных
Главное здесь другое: группа агентов смогла самостоятельно разработать алгоритм и подготовить его формальное доказательство всего за 15 часов
https://www.vals.ai/blogs/faster-shortest-path-algorithm
Для графов с определённой плотностью сложность снизилась с O(n log n) у Дейкстры до O(n log¹¹⁄¹² n). Корректность и оценка времени работы формально подтверждены доказательством в Lean
Но это пока теоретический результат
Алгоритм не тестировали на крупных реальных графах, константы велики, а улучшение действует только в ограниченном диапазоне входных данных
Главное здесь другое: группа агентов смогла самостоятельно разработать алгоритм и подготовить его формальное доказательство всего за 15 часов
https://www.vals.ai/blogs/faster-shortest-path-algorithm
У Сенеки есть притча о том, как один богатый римлянин купил рабов, которые выучили наизусть Гомера и других классиков, чтобы брать их с собой на пиры и там выглядеть умным
На что один из его друзей заметил ему, что можно купить ещё и борцов, чтобы выглядеть сильным
На что один из его друзей заметил ему, что можно купить ещё и борцов, чтобы выглядеть сильным
Claude помог ускорить собственный интерфейс втрое за две недели
Anthropic рассказала, как команда вместе с Claude внесла более 3.000 изменений в claude.ai и десктопное приложение - без пользовательских инцидентов и откатов
Результаты по 75-му перцентилю:
— Готовность сайта к вводу: 3.1 → 0.55 секунды
— Загрузка облачной сессии Cowork: 2.6 → 0.73 секунды
— Запуск десктопного приложения: 6.3 → 3.3 секунды
Всё координировали в Slack: одновременно шло более 150 тредов
Claude находил узкие места, создавал бенчмарки, готовил исправления и проверял метрики после выпуска
Каждое изменение одобрял человек
Среди находок — 6.900 React-хуков и 900 подписок, участвовавших в обработке каждого нажатия клавиши, и лишний вызов
Чтобы ускорения сохранялись, в CI добавили проверки: изменение, увеличивающее число инструкций на контролируемом участке, не проходит
Ускорили загрузку, навигацию и отрисовку интерфейса
Заявленные «3×» относятся именно к этим сценариям
https://claude.dev/blog/how-we-made-claude-ai-faster/
Anthropic рассказала, как команда вместе с Claude внесла более 3.000 изменений в claude.ai и десктопное приложение - без пользовательских инцидентов и откатов
Результаты по 75-му перцентилю:
— Готовность сайта к вводу: 3.1 → 0.55 секунды
— Загрузка облачной сессии Cowork: 2.6 → 0.73 секунды
— Запуск десктопного приложения: 6.3 → 3.3 секунды
Всё координировали в Slack: одновременно шло более 150 тредов
Claude находил узкие места, создавал бенчмарки, готовил исправления и проверял метрики после выпуска
Каждое изменение одобрял человек
Среди находок — 6.900 React-хуков и 900 подписок, участвовавших в обработке каждого нажатия клавиши, и лишний вызов
location.reload(), вызывавший полмиллиона скрытых перезагрузок в деньЧтобы ускорения сохранялись, в CI добавили проверки: изменение, увеличивающее число инструкций на контролируемом участке, не проходит
Ускорили загрузку, навигацию и отрисовку интерфейса
Заявленные «3×» относятся именно к этим сценариям
https://claude.dev/blog/how-we-made-claude-ai-faster/
claude.dev
How we made claude.ai 3x faster in two weeks / claude.dev
Inside our performance sprint: the benchmarks Claude built, the loop each Slack thread ran, and the guardrails that let us ship 3,000 changes safely.
This media is not supported in your browser
VIEW IN TELEGRAM
Фуга в стиле Баха, от Клод Опус 5.5
Последовательность круга квинт, начинающаяся на 1:13, неплоха
Взаимодействие голосов естественно
Последовательность круга квинт, начинающаяся на 1:13, неплоха
Взаимодействие голосов естественно
Warum ich allein bin
Nicht, weil die Menschen mir zuwider sind
Der Seele braucht es Weite, nicht Gedräng
Die Welt zu schauen bis auf ihren Grund, ward Stille mir gegeben auf dem Gang
Im stillen Raum findet der Geist sein Haus, wo fremder Lärm die Spuren nicht verwirrt
Ich prüfe, was ich tat, in eigner Ruh, wie Wind das Laub am Wasser neu entwirrt
Nicht braucht der Stimmen unablässger Fluss
Ich fülle selbst den Tag mit stiller Zeit: mit Buch und Werk, mit Schaffen, oder bloß mit Sinnen lang unter der Sternenweit
Der andern Urteil bleibt ein Wind am Tor
Nicht jeder Ruf verdient, dass ich ihn hör
Nicht jedes Wort gehört der Seele Ohr
Wahl ward mein Schritt und wachsam mein Gehör
So tritt der Wandrer fort vom lauten Tor und findet in sich selbst die ganze Welt
Nur dort, wo keine fremde Schranke stört, wird ihm die klarste Antwort zugestellt
Nicht, weil die Menschen mir zuwider sind
Der Seele braucht es Weite, nicht Gedräng
Die Welt zu schauen bis auf ihren Grund, ward Stille mir gegeben auf dem Gang
Im stillen Raum findet der Geist sein Haus, wo fremder Lärm die Spuren nicht verwirrt
Ich prüfe, was ich tat, in eigner Ruh, wie Wind das Laub am Wasser neu entwirrt
Nicht braucht der Stimmen unablässger Fluss
Ich fülle selbst den Tag mit stiller Zeit: mit Buch und Werk, mit Schaffen, oder bloß mit Sinnen lang unter der Sternenweit
Der andern Urteil bleibt ein Wind am Tor
Nicht jeder Ruf verdient, dass ich ihn hör
Nicht jedes Wort gehört der Seele Ohr
Wahl ward mein Schritt und wachsam mein Gehör
So tritt der Wandrer fort vom lauten Tor und findet in sich selbst die ganze Welt
Nur dort, wo keine fremde Schranke stört, wird ihm die klarste Antwort zugestellt
У формальных методов плохая репутация
Много греческих букв
Мало людей
Длинные доказательства
Кажется, что где-то в закрытом подвале сидят специалисты по Coq, Lean и Isabelle, разговаривают о зависимых типах и не пускают внутрь нормальных инженеров
Это впечатление заслуженно
Формальные системы долго были дорогими по входу: требовали времени, хорошей логической подготовки и готовности терпеливо объяснять машине то, что человеку кажется само собой разумеющимся
Но именно здесь происходит важный сдвиг
Не в том, что формализация внезапно стала лёгкой
А в том, что вокруг неё появилась нормальная образовательная среда
Например, Natural Number Game — это интерактивная игра, в которой человек осваивает доказательства в Lean на утверждениях о натуральных числах
Не через чтение монографии на тысячу страниц, а через последовательность задач и обратную связь от системы Этот формат уже стал распространённой точкой входа в университетское преподавание Lean, а исследователи отдельно изучают, как студенты строят доказательства в такой среде
Но самое важное здесь даже не Lean
Самое важное — смена педагогической оптики
Формальное доказательство перестаёт быть финальным ритуалом для человека, который уже выучил всю математику
Оно становится тренажёром мышления
Система не принимает фразу «ну тут очевидно»
Не поддаётся на уверенный тон
Не угадывает, что имел в виду автор
Но показывает: вот место, где у тебя есть пробел
Для студента это иногда неприятнее, чем замечание преподавателя
Преподаватель может понять, куда ты клонишь. Lean не обязан понимать
Он требует, чтобы мысль была выражена так, чтобы её можно было проверить
Любой человек, который учился программировать, проходил через похожий опыт
Компилятор сначала кажется придирчивым бюрократом
Потом выясняется, что он не вредничает, а защищает от ошибок, которые в большом проекте стоят гораздо дороже, чем пять минут мимолётного раздражения
Доказательный ассистент делает то же самое для математического рассуждения
Он не делает человека умнее автоматически
Он не заменяет понимание
Но он не позволяет подменить понимание интонацией
Конечно, нельзя обещать студентам, что после нескольких лабораторных работ они будут формализовать теоремы уровня современной общей алгебры или верифицировать ядро операционной системы
Зато после нескольких хорошо поставленных задач можно получить важнейшую привычку: сначала договориться, что именно утверждается, а уже потом доказывать, программировать и спорить
И эта привычка нужна не только математикам
Она нужна аналитику, который пишет требования Разработчику, который проектирует протокол. Исследователю, который строит модель Руководителю, который принимает решение на основании данных
И, особенно, человеку, который хочет отличать правдоподобный ответ от обоснованного
Формальные системы не обещают избавить нас от сложностей
Они делают сложность видимой
В образовании это не недостаток, а редкая честность
Много греческих букв
Мало людей
Длинные доказательства
Кажется, что где-то в закрытом подвале сидят специалисты по Coq, Lean и Isabelle, разговаривают о зависимых типах и не пускают внутрь нормальных инженеров
Это впечатление заслуженно
Формальные системы долго были дорогими по входу: требовали времени, хорошей логической подготовки и готовности терпеливо объяснять машине то, что человеку кажется само собой разумеющимся
Но именно здесь происходит важный сдвиг
Не в том, что формализация внезапно стала лёгкой
А в том, что вокруг неё появилась нормальная образовательная среда
Например, Natural Number Game — это интерактивная игра, в которой человек осваивает доказательства в Lean на утверждениях о натуральных числах
Не через чтение монографии на тысячу страниц, а через последовательность задач и обратную связь от системы Этот формат уже стал распространённой точкой входа в университетское преподавание Lean, а исследователи отдельно изучают, как студенты строят доказательства в такой среде
Но самое важное здесь даже не Lean
Самое важное — смена педагогической оптики
Формальное доказательство перестаёт быть финальным ритуалом для человека, который уже выучил всю математику
Оно становится тренажёром мышления
Система не принимает фразу «ну тут очевидно»
Не поддаётся на уверенный тон
Не угадывает, что имел в виду автор
Но показывает: вот место, где у тебя есть пробел
Для студента это иногда неприятнее, чем замечание преподавателя
Преподаватель может понять, куда ты клонишь. Lean не обязан понимать
Он требует, чтобы мысль была выражена так, чтобы её можно было проверить
Любой человек, который учился программировать, проходил через похожий опыт
Компилятор сначала кажется придирчивым бюрократом
Потом выясняется, что он не вредничает, а защищает от ошибок, которые в большом проекте стоят гораздо дороже, чем пять минут мимолётного раздражения
Доказательный ассистент делает то же самое для математического рассуждения
Он не делает человека умнее автоматически
Он не заменяет понимание
Но он не позволяет подменить понимание интонацией
Конечно, нельзя обещать студентам, что после нескольких лабораторных работ они будут формализовать теоремы уровня современной общей алгебры или верифицировать ядро операционной системы
Зато после нескольких хорошо поставленных задач можно получить важнейшую привычку: сначала договориться, что именно утверждается, а уже потом доказывать, программировать и спорить
И эта привычка нужна не только математикам
Она нужна аналитику, который пишет требования Разработчику, который проектирует протокол. Исследователю, который строит модель Руководителю, который принимает решение на основании данных
И, особенно, человеку, который хочет отличать правдоподобный ответ от обоснованного
Формальные системы не обещают избавить нас от сложностей
Они делают сложность видимой
В образовании это не недостаток, а редкая честность
Промпт → Агенты → Делегирование → Оркестровка → Автономные системы
Создать → Разделить → Оркестрировать → Отправить
Создать → Разделить → Оркестрировать → Отправить