Обновить

Господа, добрый день! Я собираюсь выпустить статью о языке программирования Lean.
Он сочетает в себе два назначения: это одновременно и язык программирования, и средство доказательства теорем. И они помогают друг другу. На языке программирования Lean можно писать тактики, которые помогают упростить доказательства, а при помощи средств доказательства можно гарантировать, что наша программа корректна!

Язык очень молодой, сообществу нужны программисты, а не только математики, чтобы сделать язык готовым к промышленному применению. Сейчас очень не хватает многих прикладных библиотек. Язык то вышел в этом десятилетии! Причём многие из этих библиотек - низко висящие фрукты - их довольно легко написать!

Скажите, о чём бы вы хотели прочитать в моей будущей статье? Какие аспекты вам наиболее интересны? Решение какого-нибудь примера? Или просто обзор языка и его экосистемы? Может быть, рассказ о том, как для написания доказательств используют искусственный интеллект?

Предлагайте свои варианты и задавайте вопросы.

Теги:
Всего голосов 5: ↑5 и ↓0+7
Комментарии4

Как мы запустили Qwen3.8–27B целиком на RTX 5060 8 GB и получили ~30 токенов/с

Наш проект называется ExVRAM Lab. Это открытая исследовательская лаборатория, в которой мы проверяем, насколько большие локальные LLM можно запускать на обычных видеокартах с ограниченным объёмом VRAM, если использовать ultra‑low‑bit quantization, полное размещение весов на GPU и существующие open‑source inference‑технологии.

ExVRAM расшифровывается как Exchange Compute for VRAM. Основная идея проекта — в ряде сценариев выгоднее потратить часть свободной вычислительной мощности GPU на работу с более компактным представлением весов, чем хранить часть модели в оперативной памяти и постоянно передавать данные через PCIe.

Когда мы начинали проект, исходный вопрос был достаточно простой: можно ли запустить dense‑модель примерно на 27 миллиардов параметров на видеокарте всего с 8 ГБ VRAM так, чтобы она не просто «запустилась», а работала полностью на GPU, поддерживала длинный контекст и обеспечивала нормальную интерактивную скорость генерации.

В качестве основной тестовой системы мы используем NVIDIA GeForce RTX 5060 8 GB на архитектуре Blackwell. Основная модель в текущих экспериментах — Qwen3.8–27B.

Сначала результат выглядел не слишком впечатляюще. Модель запускалась, но значительная часть весов оставалась в системной памяти. Около 5,7 GiB весов находилось на GPU, ещё примерно 2,5 GiB — на CPU. Скорость генерации составляла порядка 3,8–5,5 токена в секунду.

При этом сама видеокарта была загружена далеко не полностью.

Это стало одним из первых важных наблюдений проекта. Проблема заключалась не столько в нехватке вычислительной мощности RTX 5060, сколько в том, что часть decoder weights находилась в RAM. Во время autoregressive generation данные приходилось постоянно передавать между CPU и GPU через PCIe.

Как мы запустили Qwen3.8–27B целиком на RTX 5060 8 GB и получили ~30 токенов/с

Публикации