Apple и хеллоуинский брутализм
Apple выпустила короткую презентацию по поводу рутинного выхода очередной серии чипов (M3). Видно, что заготовки были сделаны давно, прогресс идёт по расписанию. Целевой период использования "макбука", учитывая скорость планомерного роста характеристик, примерно 3-5 лет. Думаю, это вдвое больше, чем для аналогичных ноутбуков других производителей. Это плюс.
А минус в самой презентации. Тренд на мрачные декорации, заданный Фейсбуком (обсуждали два года назад), был взят на вооружение и усилен.
Вся презентация проходит на фоне нарочито врезанных фоновых картинок (отслеживание движения камеры не сглаживает, а лишь усиливает искусственность). Персонаж ходит между нарисованной мебели ("вот до чего техника дошла"), но одновременно не дотрагивается до предметов ("а нет, не дошла"), как бы намеренно придавая неловкости всей картинке.
Основной сюжет разворачивается в бетонном бункере "без окон и дверей". В какой-то момент выясняется, что счастливый дом какой-то парочки музыкантов, эпизодически показываемый в ярких оранжевых тонах, стоит посередине всё того же безликого огромного и пустого ангара. Как в суперлаборатории из "Breaking Bad" :)
Понятно, что люди пошутили, хеллоуин, игривая музыка на фоне. Весёлый карнавал в подземном бетонном бункере. Тянет туда людей, что поделать.
Кстати, вот и архитектор Клио в своём последнем посте о том же ведь!
#programming
Apple выпустила короткую презентацию по поводу рутинного выхода очередной серии чипов (M3). Видно, что заготовки были сделаны давно, прогресс идёт по расписанию. Целевой период использования "макбука", учитывая скорость планомерного роста характеристик, примерно 3-5 лет. Думаю, это вдвое больше, чем для аналогичных ноутбуков других производителей. Это плюс.
А минус в самой презентации. Тренд на мрачные декорации, заданный Фейсбуком (обсуждали два года назад), был взят на вооружение и усилен.
Вся презентация проходит на фоне нарочито врезанных фоновых картинок (отслеживание движения камеры не сглаживает, а лишь усиливает искусственность). Персонаж ходит между нарисованной мебели ("вот до чего техника дошла"), но одновременно не дотрагивается до предметов ("а нет, не дошла"), как бы намеренно придавая неловкости всей картинке.
Основной сюжет разворачивается в бетонном бункере "без окон и дверей". В какой-то момент выясняется, что счастливый дом какой-то парочки музыкантов, эпизодически показываемый в ярких оранжевых тонах, стоит посередине всё того же безликого огромного и пустого ангара. Как в суперлаборатории из "Breaking Bad" :)
Понятно, что люди пошутили, хеллоуин, игривая музыка на фоне. Весёлый карнавал в подземном бетонном бункере. Тянет туда людей, что поделать.
Кстати, вот и архитектор Клио в своём последнем посте о том же ведь!
#programming
Как я пользуюсь докером в быту
(Программистская тема, так что всех не интересующихся прошу скиповать.)
Иногда бывает удобно установить что-то не из brew/apt (или аналога), а напрямую из исходников или скачав бинарник. С другой стороны устанавливать все зависимости времени компиляции и времени выполнения в основную систему неудобно, кроме того возможны конфликты между разными версиями библиотек и т.д.
В таких случаях максимально удобно использовать Docker.
Чтобы вручную не вбивать каждый раз кучу параметров docker build/docker run я пришёл к такой схеме:
* В
* В
* Скрипт
* Скрипт
* Скрипт
Директория
Выложил на github: https://github.com/EugZol/docker-run-script
#programming
(Программистская тема, так что всех не интересующихся прошу скиповать.)
Иногда бывает удобно установить что-то не из brew/apt (или аналога), а напрямую из исходников или скачав бинарник. С другой стороны устанавливать все зависимости времени компиляции и времени выполнения в основную систему неудобно, кроме того возможны конфликты между разными версиями библиотек и т.д.
В таких случаях максимально удобно использовать Docker.
Чтобы вручную не вбивать каждый раз кучу параметров docker build/docker run я пришёл к такой схеме:
* В
~/images пишу dockerfile для образа очередной программы, например youtube-dl.dockerfile для youtube-dl* В
~/images/docker-compose.yml добавляю секцию для сборки и теггирования описанного образа* Скрипт
~/images/build-all делает docker-compose build, собирая все образы* Скрипт
~/images/wrap-all для каждого докерфайла создаёт скрипт запуска данного контейнера в ~/bin, вызывая ~/bin/docker-run-script* Скрипт
~/bin/docker-run-scripts вызывает docker run ..., передавая параметры командной строки и подключая текущую директорию внутрь образаДиректория
~/bin добавлена в PATH, в итоге собранными в докере скриптами можно пользоваться как установленными локально (например, запускать youtube-dl-docker как если бы это был установленный youtube-dl).Выложил на github: https://github.com/EugZol/docker-run-script
#programming
Ведутся бесконечные споры о том, надо ли на собеседовании программистов спрашивать алгоритмы.
Есть более насущный вопрос: владение алфавитом.
Конечно в идеале было бы сделать, как это сейчас модно, чтобы не просто пункты меню в случайном порядке были перечислены, но и чтобы их порядок менялся после каждого клика и при этом в каждом проекте был свой.
Это в полной мере подошло бы ценностям Гитлаба типа "больше дел, меньше анализа" и пр.
О дивный мир UX-дизайна!
#programming
Есть более насущный вопрос: владение алфавитом.
Конечно в идеале было бы сделать, как это сейчас модно, чтобы не просто пункты меню в случайном порядке были перечислены, но и чтобы их порядок менялся после каждого клика и при этом в каждом проекте был свой.
Это в полной мере подошло бы ценностям Гитлаба типа "больше дел, меньше анализа" и пр.
О дивный мир UX-дизайна!
#programming
Вкратце о математиках, информатиках и маркетинге
ChatGPT выпустил новую модель, o1, построенную на принципе рекурсивного порождения текстов: модель буквально ведёт сама с собой "внутренний диалог", "думает вслух", пытаясь в итоге получить рациональное построение.
Как и во все предыдущие разы, достигнутый успех, мягко говоря, ограниченный. Забавная и в чём-то правдоподобная модель мышления способна выдать рассуждение на общие вопросы, но сыпется на самых простых задачках из, к примеру, абстрактной алгебры.
Подобное положение вещей укрепляет уже в общем-то устоявшееся впечатление, что большие лингвистические модели это больше о болтовне на свободные темы, чем о решении реальных задач.
С чем смириться, конечно, невозможно.
Для подтягивания роботам математики необходимо (хоть и недостаточно) набрать "математического материала". Буквально следует иметь некое промежуточное формальное представление, не допускающее лишних вольностей и галлюцинаций, в которое можно конвертировать запрос пользователя (математическую задачу, формулировку теоремы и т.п.), и из которого потом снова перевести результат на естественный язык. (Такую работу ИИ как специфического "универсального переводчика" вкратце обсуждали ранее.)
Как на основе подобного формального представления довести качество работы бота до приемлемого уровня (ведь в аналогичной задаче — написание программного кода — ещё и близко об этом говорить не приходится) как-нибудь в будущем разберутся.
Сейчас — нужен сырой материал для обучения.
В таком контексте второе дыхание получают proof assistants — "помощники в доказательстве", такие как Lean.
И на сцену выходят агрессивные проповедники (см. предыдущий пост-введение) с практически буквально следующими лозунгами: деды приватизировали математику, да и вообще люди совершают ошибки, формализуем все теории в Lean!
Целевая аудитория: пассионарные undergraduate students (бакалавры). Ну оно и понятно по слову "деды" в риторике (сам Кевин практически подросток, до 60 ещё два года).
Работа по рутинной формализации всяких давно известных вещей скучная, тупая, безблагодатная и в целом в контексте обучения отдельно взятого математика неоднозначная. А ведь нельзя же просто взять денег у Microsoft на честное развитие проекта, нацеленного на совершенствование ИИ... а кстати, почему нельзя?
Агрессивная риторика, впрочем, неизбежно порождает агрессивных фанбоев. Ну знаете, есть пользователи Apple и есть
По неофициальному мнению некоторых профессионалов в области систем формальных доказательств из числа наших подписчиков, началась вся текущая волна беззастенчивой рекламы с того, что... американцам в более зрелых проектах-аналогах не понравилось название... потому что Coq оно по произношению означает... ну, вы знаете, то самое. Не захотели переименовываться по-хорошему, сейчас значит организуем переезд по-плохому! :)
#mathematics #programming
ChatGPT выпустил новую модель, o1, построенную на принципе рекурсивного порождения текстов: модель буквально ведёт сама с собой "внутренний диалог", "думает вслух", пытаясь в итоге получить рациональное построение.
Как и во все предыдущие разы, достигнутый успех, мягко говоря, ограниченный. Забавная и в чём-то правдоподобная модель мышления способна выдать рассуждение на общие вопросы, но сыпется на самых простых задачках из, к примеру, абстрактной алгебры.
Подобное положение вещей укрепляет уже в общем-то устоявшееся впечатление, что большие лингвистические модели это больше о болтовне на свободные темы, чем о решении реальных задач.
С чем смириться, конечно, невозможно.
Для подтягивания роботам математики необходимо (хоть и недостаточно) набрать "математического материала". Буквально следует иметь некое промежуточное формальное представление, не допускающее лишних вольностей и галлюцинаций, в которое можно конвертировать запрос пользователя (математическую задачу, формулировку теоремы и т.п.), и из которого потом снова перевести результат на естественный язык. (Такую работу ИИ как специфического "универсального переводчика" вкратце обсуждали ранее.)
Как на основе подобного формального представления довести качество работы бота до приемлемого уровня (ведь в аналогичной задаче — написание программного кода — ещё и близко об этом говорить не приходится) как-нибудь в будущем разберутся.
Сейчас — нужен сырой материал для обучения.
В таком контексте второе дыхание получают proof assistants — "помощники в доказательстве", такие как Lean.
И на сцену выходят агрессивные проповедники (см. предыдущий пост-введение) с практически буквально следующими лозунгами: деды приватизировали математику, да и вообще люди совершают ошибки, формализуем все теории в Lean!
Целевая аудитория: пассионарные undergraduate students (бакалавры). Ну оно и понятно по слову "деды" в риторике (сам Кевин практически подросток, до 60 ещё два года).
Работа по рутинной формализации всяких давно известных вещей скучная, тупая, безблагодатная и в целом в контексте обучения отдельно взятого математика неоднозначная. А ведь нельзя же просто взять денег у Microsoft на честное развитие проекта, нацеленного на совершенствование ИИ... а кстати, почему нельзя?
Агрессивная риторика, впрочем, неизбежно порождает агрессивных фанбоев. Ну знаете, есть пользователи Apple и есть
пользователи Apple. В таком же смысле есть пользователи Lean и есть пользователи Lean :)По неофициальному мнению некоторых профессионалов в области систем формальных доказательств из числа наших подписчиков, началась вся текущая волна беззастенчивой рекламы с того, что... американцам в более зрелых проектах-аналогах не понравилось название... потому что Coq оно по произношению означает... ну, вы знаете, то самое. Не захотели переименовываться по-хорошему, сейчас значит организуем переезд по-плохому! :)
#mathematics #programming