Maxwell от doubleAI: ИИ переписывает бинарный код на лету и формально доказывает эквивалентность
Maxwell: A new kind of model that sits between code and hardware
doubleAI представила Maxwell — первую модель исполнения кода (CEM), которая работает между программой и железом. Пока код выполняется, Maxwell находит узкие места, генерирует новый бинарный код под конкретную машину и формально доказывает, что замена семантически эквивалентна оригиналу. Исходники не меняются. На демо обработка данных ускорилась в 38 раз, инференс — в 4,25 раза, а генерация 4K-видео в LTX-2.5 — почти вдвое.
Любое и всё мышление происходит до выполнения программы, но абсолютно никакого — во время или после.
- epsylon
На этой странице много заявлений и так мало технических деталей.
Как была выполнена формализация Python? Какой фреймворк формальных доказательств вы используете?
Как вы воспроизводите оптимизации в нескольких экземплярах / запусках программы? (поскольку исходный код не меняется... предполагая, что вы не выполняете одну и ту же работу снова и снова?)
Какая видимость, отслеживание и логирование есть для фактически выполняющегося кода? Отладка — чрезвычайно важная часть создания программного обеспечения, особенно если под ним демон постоянно подменяет бинарный код. Даже если рекомпилятор идеален (а он не будет), пользовательский код никогда не идеален.
Почему супероптимизация и видимость данных не выводятся обратно на уровень исходного кода? Это кажется расточительством.
- gavinray
Это было гораздо более захватывающе, чем я ожидал.
Домашняя страница не очень хорошо объясняет, на что мы смотрим:
Похоже, это комбинация двух вещей:
1) Формализация языка Python
2) LLM, которая подключается к работающим программам и на лету заменяет код на поведенчески эквивалентный, но с лучшей производительностью во время выполнения, найденный с помощью супероптимизации и затем проверенный с помощью правил формализации
Это блестяще, и задним числом это одна из тех вещей в духе «не могу поверить, что никто до этого не додумался».
- mccoyb
Скажу, что мне нравится идея:
- верификация
- супероптимизация, специализированная для конкретного куска аппаратного обеспечения
- исправление бинарников во время их выполнения
всё отлично
Тем не менее, от текста на этом сайте у меня возникают странные ощущения. Маленькие фразы и заявления, которые, похоже, предназначены для маркетинговых целей, но смешивают вещи с четким техническим значением запутанным образом.
Например: я посмотрел видео («модель выполнения кода должна быть правильной каждый раз»), которое неявно сообщает что-то вроде «модель не может галлюцинировать»... конечно, агентная LM по-прежнему вероятностна, но она обернута инструментами верификации (чтобы рассуждать о семантической эквивалентности) и, вероятно, дообучена, чтобы хорошо использовать эти инструменты.
Это кажется мне смешением модели и обвязки, предназначенным для маркетингового эффекта (вроде: «она не галлюцинирует»), но которое явно является нелепым заявлением (скатываясь по наклонной: любая обвязка, которая исправляет ошибки при неправильных вызовах инструментов, тоже может быть «моделью, которая не делает ошибок»)
Еще: «самоулучшающийся код»
это ведь не совсем так? Самоулучшающийся код был бы кодом, который запускает себя и улучшает себя. Это код, который запускаю я, а Maxwell наблюдает и улучшает... нет?
Связанное: мне не нравится использование слова «модель» в вышеупомянутых обсуждениях на сайте. Мы теперь хотим называть всё «моделью»? Может ли кто-нибудь изобрести новую передовую «модель», дообучив агентную LM с инструментами?
Еще, скажем, […]