72 subscribers
8 photos
1 video
8 files
178 links
Machine learning
Download Telegram
TRIBE (Trimodal Brain Encoder) с 1.000.000.000 параметров — первая сеть, обученная предсказывать реакции мозга на стимулы в разных модальностях, кортикальных областях и у разных людей

Модель объединяет предварительно обученные представления нескольких базовых моделей:

- текстовой (Llama 3.2),
- аудио (Wav2Vec2-BERT от Seamless)
- видео (V-JEPA 2), чтобы предсказывать пространственно-временные отклики мозга (fMRI) на фильмы, собранные в рамках проекта Courtois NeuroMod (80 часов на каждого испытуемого)

Команда разработчиков модели FAIR’s Brain & AI
заняла 1-е место на соревновании по моделированию мозга Algonauts 2025

Код
Данные
Lean 4 — это интерактивный помощник по доказательствам, где математика пишется как код, а машина проверяет каждое определение и шаг рассуждения

Учебник Mathematics in Lean учит формализовывать задачи на понятном «языке доказательств»: от элементарной теории чисел до анализа и меры

За спиной — большая библиотека Mathlib и активное сообщество в чате Lean Zulip, так что вы не останетесь одни

Книга задумана как «живой» учебник внутри VS Code

Открываете Lean, печатаете определения и леммы, а в правой панели сразу видите цели и подсказки от системы

Практика — в центре: каждый раздел сопровождается файлом с примерами и упражнениями, их удобно править прямо в редакторе и тут же смотреть реакцию Lean (вплоть до простых экспериментов вроде
#eval "Привет, мир!")

Старт простой: ставите Lean 4 и VS Code, клонируете репозиторий mathematics_in_lean, открываете папку MIL и работаете в своей копии, чтобы безболезненно подтягивать обновления

Внутри — аккуратная структура по главам, текстовые подсказки и готовые решения в отдельной папке для самопроверки
Документацию удобно вызывать прямо из редактора через команду «Lean 4: Docs»

Если не хочется настраивать среду локально, всё запускается в облаке через Gitpod: открыли проект — и можно учиться с телефона или любого ноутбука
Учебник ещё развивается, поэтому время от времени стоит обновлять репозиторий — материалы пополняются

https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html
Anthropic и OpenAI дают доступ к своим самым последним Ml

Это сильно повлияет на институт государства
Это большой культурный шифт

Государство становится программным обеспечением, которое может работать без людей, которые сегодня находятся внутри и уже не имеют ценности
SuperNeuro_A_Fast_and_Scalable_Simulator_for_Neuromorphic_Computing.pdf
448.4 KB
SuperNeuro для больших сетей точечных спайковых нейронов

Сотрудники
Ок-Риджской национальной лаборатории (англ. Oak Ridge National Laboratory) [1] Министерства энергетики США разрабатывают собственный композитный симулятор спайковых нейронных сетей SuperNeuro [2] (реально состоящий из двух концептуально различных симуляторов - MAT и ABM), способный быстро работать на нейроморфном "железе" (в частности, на условном FPGA-нейропроцессоре NeuroCoreX [3] их собственной разработки)

Основными конкурентами
SuperNeuro, который, по заявлению разработчиков (см. прилагаемую статью), в разы превосходит их по скорости, выступают "европейские" нейросимуляторы NEST and Brian2

[1]:
https://www.ornl.gov/
[2]:
https://github.com/ORNL/superneuro
[3]:
https://github.com/ORNL/NeuroCoreX
DL-модель TRIBE (Trimodal Brain Encoder) для предсказания fMRI-реакций человеческого мозга на предъявляемые стимулы, причем стимулы могут быть в трёх разных форматах - как текст, аудио или видео

PS: Своеобразная симуляция 3D клеточного (точнее,
воксельного) автомата?
Сразу вспомнилась книга
"A New Kind of Science" (2002) Стивена Вольфрама
Формула Лейбница — взятие производной по параметру определенного интеграла

Очень полезная практически (например, если надо продифференцировать автокорреляционную функцию, заданную на конечном интервале)
К сожалению, далеко не все профильные студенты знают/помнят эту формулу, поэтому рекомендую разобраться с её выводом и выучить наизусть, как правила дифференцирования
Merge Labs и Neuralink поможет человечеству избежать вымирания, с помощью технологий обьеденив с машинами так хорошо, что симбиоз мозгов с Ml далеко превзойдет Ml без мозгов

https://blog.samaltman.com/the-merge
(оригинал:
https://medium.com/wordsthatmatter/merge-now-430c6d89d1fe )
The Merge
Sam Altman
December 7, 2017

(Как известно, в 2015 году Олтмен (Альтман) и Маск стали сооснователями OpenAI, но в 2018 Маск ушел из компании)

История понятия "сингулярность" в этом контексте:

TechCrunch,
пресказывая материал FT, в котором упоминается этот блогпост. также утверждает, что понятие "сингулярности" появилось в одноименном романе итальянского писателя Дино Буццати (Dino Buzzati) еще в 1960
Впрочем, википедия подсказывает, что The Singularity - это название английского издания 2025 (!) года, а первый перевод на английский, вышедший в 1962м, назывался Larger than Life
По-итальянски роман назывался Il grande ritratto.
Пишут, что The term singularity, today used as shorthand to indicate the historical moment in which artificial intelligence will surpass human capacities to the point that it will revolutionize human life as we know it, can be dated back to the 1980s, well after the publication of this novel
Про технологическую сингулярность можно
прочитать, что модель самоулучшающегося интеллекта предложил в 1965 году, а о возможной опасности взрывного саморазвития суперинтеллекта предупреждали впоследствии уже Стивен Хокинг и другие ученые
Что же касается слияния человеческого и машинного интеллекта, эта идея, скорее, связана с Курцвейлом, который еще 20 лет назад выпустил книгу The Singularity Is Near
В его понимании, которое с тех пор не изменилось, сингулярность -- это не свмодеятельность машин, а результат слияния слияние человеческого мозга с облаком, будет достигнуто не через инвазивные электроды, а через "наноботы", которые смогут входить в мозг через капилляры - см., напр., его
интервью Гардиан этого года


Financial Timed сообщили, что и Сэм поддерживает стартап Merge Labs, который будет делать интерфейс мозг-компьютер для слияния человека и Ml:

Merge Labs — это
стартап, разрабатывающий интерфейсы мозг-компьютер, причём компания хочет привлечь уже $250.000.000 инвестиций при оценке в $850.000.000

Большая часть инвестиций поступит от венчурного подразделения OpenAI

Об этом
проекте тут

Альтман, как сооснователь и CEO OpenAI, будет числиться соучредителем Merge Labs вместе с Алексом Бланией, CEO проекта World, также поддерживаемого OpenAI, но не будет участвовать в операционной деятельности компании

Merge Labs планирует развивать нейротехнологии с использованием Ml
О том как индустрия сейчас развивается, читайте
тут

О том, что нейроинтерфейсы + Ml - это новый большой тренд,
здесь

https://www.ft.com/content/04484164-724e-4fc2-92a2-e2c13ea639bd
Sam Altman challenges Elon Musk with plans for Neuralink rival
12.08.2025
13 августа, в 1861 году родился Чезаре Бурали-Форти — итальянский математик, работавший вместе с Джузеппе Пеано, автор одного из первых и самых известных парадоксов в теории множеств, который стал настоящим испытанием для идей Георга Кантора

Хотя его имя сегодня встречается реже, чем Кантора или Рассела, именно он первым показал, что бесконечность может быть не просто большой, а… слишком большой, чтобы существовать

Парадокс Бурали-Форти начинается с попытки построить «множество всех ординалов» — особых чисел, которые обобщают понятие порядка для бесконечных последовательностей

Кантор показал, что такие числа можно сравнивать и упорядочивать

Но если собрать все ординалы вместе, получится новый ординал, который должен быть больше любого из них

И тут возникает логический сбой: этот «самый большой ординал» не может принадлежать множеству всех ординалов, потому что он больше любого его элемента — и всё рушится

Этот парадокс стал тревожным звонком для математиков конца XIX века: сама идея «множества всех» оказалась опасной

Он предвосхитил кризис в основах математики и подтолкнул развитие более строгих аксиоматических систем, в которых подобные «слишком большие» множества больше нельзя было строить