The OpenNET Project / Index page

[ новости /+++ | форум | теги | ]

Mistral опубликовал Leanstral, AI-модель для вайб-кодинга с формальной верификацией

17.03.2026 10:48 (MSK)

Компания Mistral AI представила большую языковую модель Leanstral, нацеленную на использование для разработки приложений (вайб-кодинга) и оптимизированную для формальной верификации кода. Предполагается, что Leanstral может применяться для создания AI-ассистентов, позволяющих не просто генерировать код, но и гарантировать отсутствие в нём ошибок.

Leanstral стала первой открытой моделью, поддерживающей язык программирования Lean 4 и связанный с ним инструментарий для проверки математических доказательств. Lean 4 предоставляет возможности для математического доказательства корректности кода и его соответствия спецификации, что в контексте вайб-кодинга позволяет подтвердить, что сгенерированный AI-моделью код делает именно то, что задумано.

Модель охватывает 119 миллиардов параметров (6.5 млрд активируемых параметров на токен), учитывает контекст в 256 тысяч токенов и опубликована под лицензией Apache 2.0. Загружаемый архив с Leanstral занимает 121 ГБ и пригоден для использования на локальных системах. Для локального запуска могут применяться библиотеки vllm, transformers и SGLang.

Среди прочего модель может применяться для вайб-разработки в открытом агенте mistral-vibe, а также интегрироваться с инструментарием Aeneas для верификации кода на языке Rust. В качестве входных параметров принимается текст и изображения, на выходе выдаётся только текст. Поддерживается анализ содержимого изображений.

Для оценки возможностей AI-моделей с учётом качества проведения формальной верификации кода и написания математических доказательств разработан новый набор тестов FLTEval. В проведённых тестах модель Leanstral ощутимо обогнала существующие открытые модели Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B и GLM5 744B-A40B, показала сходные результаты с моделями Claude Haiku 4.5 и Claude Sonnet 4.6 от компании Anthropic, но отстала от модели Claude Opus 4.6. В частности, модель Opus набрала 39.6 баллов, а Leanstral - 21.9 при одном проходе и 31.9 при 16 проходах. При этом затраты при использовании Opus составили 1650 долларов, а Leanstral - $18 при одном проходе и $290 при 16 проходах. Модель Haiku набрала 23 балла при затратах $184, а модель Sonnet - 23.7 при затратах $549.



  1. Главная ссылка к новости (https://mistral.ai/news/leanst...)
  2. OpenNews: Mistral AI опубликовал Devstral, большую языковую модель для работы с кодом
  3. OpenNews: Организация OSI выработала критерии открытости AI-систем
  4. OpenNews: Оценка влияния вайб-кодинга на экосистему открытого ПО
  5. OpenNews: Переписывание кода при помощи AI для перелицензирования открытых проектов
  6. OpenNews: Компания SUSE открыла AI-модель для анализа лицензионной чистоты кода
Лицензия: CC BY 3.0
Короткая ссылка: https://opennet.ru/65005-mistral
Ключевые слова: mistral, ai, vibe
При перепечатке указание ссылки на opennet.ru обязательно


Обсуждение (105) Ajax | 1 уровень | Линейный | +/- | Раскрыть всё | RSS
  • 1.1, Аноним (1), 11:31, 17/03/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Кто пользуется подобным, какое железо нужно, чтобы запустить? Сам использую qwen code, было бы интересно запускать всё локально
     
     
  • 2.4, Аноним (4), 11:38, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    >Leanstral-2603  121 GB

    https://huggingface.co/mistralai/Leanstral-2603/tree/main
    Дорогое.

     
     
  • 3.6, Джон Титор (ok), 11:41, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –7 +/
    Замечу что из описания следует что русский язык оно не поддерживает
     
     
  • 4.42, Аноним (4), 13:09, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +10 +/
    На кириллице кодите ? Что не комментарий от вас, то откровение.
     
     
  • 5.45, aname (ok), 13:19, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +4 +/
    1C
     
     
  • 6.67, Аноним (4), 16:09, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +3 +/
    вайб-кодинг 1С ? К такому я ещё не готов.
     
     
  • 7.101, Джон Титор (ok), 20:37, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +5 +/
    Зря
     
  • 5.59, Аноним (59), 15:22, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/
    Дык он из будущего. Он знает.
     
     
  • 6.98, Джон Титор (ok), 20:34, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    В статье ссылка: https://huggingface.co/mistralai/Leanstral-2603

    Там в файле Readme все написано. Вы ведь английский знаете?

    p.s. я тоже знаю, но терпеть не могу.

     
  • 6.99, Джон Титор (ok), 20:36, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    На всякий случай выпишу, а то не найдете:
    Leanstral offers these capabilities:

    Multilingual: Supports English, French, Spanish, German, Italian, Portuguese, Dutch, Chinese, Japanese, Korean, and Arabic

     
  • 4.73, Аноним (73), 16:27, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Поддерживает.
     
     
  • 5.119, Джон Титор (ok), 09:37, 18/03/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Поддерживает.

    Может вы спросите у этого ИИ? https://chat.mistral.ai/chat

    > Какая ты модель? Какие языки поддерживаешь?
    >> Я — Le Chat, помощник на основе искусственного интеллекта, созданный Mistral AI. Поддерживаю множество языков, включая украинский, русский, английский, французский, испанский, немецкий и многие другие.
    > На сайте в документации: https://huggingface.co/mistralai/Leanstral-2603 указано что ты поддерживаешь много языков, но русского там нет
    >> Давай разберёмся: модель Leanstral-2603 — это специализированный кодовый агент от Mistral AI, предназначенный для работы с Lean 4 (языком доказательств и формальной верификации). Она оптимизирована для формальных доказательств, работы с математическими объектами и спецификациями программного кода, а не для общения на естественных языках. Поэтому в её документации не упоминаются языки вроде русского, английского или украинского — она просто не предназначена для этого
    >> Я же, как Le Chat, — это универсальная языковая модель, которая поддерживает множество естественных языков, включая русский, украинский, английский и другие. Если у тебя есть вопросы по программированию, математике или просто общение — спрашивай!
    > То Leanstral-2603 не поддерживает русский или поддерживает?
    >> Модель Leanstral-2603 — это специализированный кодовый агент для работы с Lean 4, она не предназначена для общения на естественных языках, включая русский. Её основная задача — помощь в формальных доказательствах и работе с математическими объектами, а не поддержка разговорных языков

     
  • 3.56, подчиняйся свободе GPL (?), 14:45, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Естественно. Придется Core 2 Duo апгрейдить. А это дорого. На макарошки не хватит
     
  • 2.5, Джон Титор (ok), 11:39, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –4 +/
    Тут главное видеокарта и её объем памяти. Лучше брать все что выше 16Гб и NVidia. Можно конечно и под других производителей адаптировать, а некоторые сразу поддерживают, но чаще всего для этого придется потанцевать с бубном. Можно все немного ускорить заморозив код и скомпилировать пайтон, но правки придется делать. Процессор хороший тоже не помешал бы, бывает что-то слетает и если протанцевали с бубном под не ту видеокарту под которую оно сделано, то можно настроить переход на процессор, но это в 10 раз дольше выполнение.
     
     
  • 3.87, Аноним (87), 19:31, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    >Лучше брать все что выше 16Гб и NVidia.

    А дешевле - ровно 16 гигабайт или ниже и не nvidia.

     
     
  • 4.104, Джон Титор (ok), 20:40, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    А дешевле можно, но даже ради учебы - пустая трата времени. Генерировать будет, но медленно. И текст, и картинки. Можно вообще на CPU или оптимизированные модели. Но лучше это время потратить с умом или воспользоваться сервисами.
     
  • 2.12, Аноним (4), 11:59, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Чтоб хоть как-то запустилось 128 Гб DDR5 ОЗУ.
    Или можно одну NVIDIA H200.
     
     
  • 3.34, Аноним (34), 12:56, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    > Чтоб хоть как-то запустилось

    И выдало хоть какие-то результаты.

     
  • 3.106, Джон Титор (ok), 20:41, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/
    А оно хоть Doom запустит?
     
  • 2.13, Аноним (13), 12:02, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –4 +/
    Нужно было интересоваться до взлета цен на память. Купить максимум во все слоты по 32гб = 128гб. Да любая видяха пойдет. Я на интегрированной 8700G. Но модели 30-60гб юзаю (q6). Квен3-кодер-30b полюбился. Главная проблема - научиться общаться с ии. Придется слова учиться подбирать и вычищать промпт от "помогающих" инструкций. Модели от devstral ужасны. Европа загнила. Фантасмагорический язык они придумали, а компилятор или интерпретатор существует? Короче он нам и нафиг не нужон Ленстрал ваш. Вайбкодинг не существует, это протокол.
     
     
  • 3.29, Аноним (29), 12:50, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Вообще-то максимум для DDR5 4x48 Gb, но нужна поддержка процом и мамой.
     
  • 3.57, Аноним (4), 14:51, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +2 +/
    То замёрзла, то загнила, то ли дело у нас!
     
  • 3.126, Джон (?), 12:34, 18/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    GPT OSS даже 20b дает во все щели убогому квен, а так квен самые слабые модели.
     
  • 2.14, Андрей (??), 12:02, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Вообще чем мощнее тем лучше, дальше по убыванию скорости генерации:
    1) "вся модель должна влезть в VRAM" ->
    2) "Часть модели влазит в VRAM, остальная часть помещается в RAM" ->
    3) "Часть модели в VRAM, часть в RAM, часть в SSD swap(В случае MoE моделей на ура)
    4) "Вся модель в RAM"
    5) "Часть в RAM, часть в SWAP"

    Короче дальше думаю ясно, по итогу ключевое наверное ограничение, это чтобы на базу и плотные слои(или активируемую часть экспертов) хватало по минимуму VRAM + RAM, тогда потыкать в разумных пределах можно любую модель, в противном случае - суета. На удивление для себя обнаружил(хотя и ожидал), что в ноут 8VRAM + 32RAM вполне влезла 80B MoE q6 модель, да ещё и работает на ~4 т/с, что вполне годно и по качеству и по скорости для автономной LLM, если бы ещё заморочится и переупорядочить экспертов(в пользу самых востребованных) и поколдовать с матричками активации, то так вообще космос будет.

     
     
  • 3.83, Аноним (4), 17:40, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/
    А дальше уже всё будет ограниченно самим чипом, контроллером памяти и даже самой моделью:
    https://signal65.com/wp-content/uploads/2025/03/chart01.webp
     
  • 2.17, Джон Титор (ok), 12:06, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +3 +/
    В моделях как правило есть ещё B параметры B биллионы, миллиарды Параметры ... большой текст свёрнут, показать
     
     
  • 3.54, booksy (?), 14:34, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Всё чётко разложил. Что посоветуете на бюджет до 4500-5000 евро? Интересно именно кодинг и эта новая модель выглядит многообещающей.
     
     
  • 4.71, Аноним (4), 16:22, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    https://www.google.com/search?q=&hl=ru&aep=22&udm=50
     
  • 4.82, Аноним (82), 17:36, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    > Что посоветуете на бюджет до 4500-5000 евро?

    Openrouter. И найти работу.

     
     
  • 5.128, Джон (?), 12:36, 18/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Кому этот хлам в 2026 сдался? Уже вагон сервисов с оплатой по сбп и дешевле раза в 2 бгггг
     
  • 4.127, Джон (?), 12:35, 18/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    routerai(dot)ru и кими к2,5
     
  • 2.18, geth (?), 12:09, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    На HF народ квантует. Пишут что:
    Performance
    On 2x RTX 4090 (48GB VRAM) + 192GB RAM with Q4_K_M:

    ~34 tokens/s generation speed
    Model splits between GPU and system RAM automatically with -fit on
    Т.е. 8 битное квантование будет примерно в 2 раза медленнее. А цены на 4090 и 5090 уточняйте у поставщиков, советую обращать внимание на китайцев с 48 Гб VRAM.

     
     
  • 3.70, Аноним (4), 16:18, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Вредный совет, сколько уже людей обожглись на всяких PELADN и т.д.
    Все эти подвальные рефабы с неизвестным ресурсом. Так что себе этих мутантов можете купить, но советовать другим это такое...
     
     
  • 4.72, geth (?), 16:23, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Уговорили, тогда покупайте H200, делов на 30 минут.
     
     
  • 5.108, Ванька с огорода (?), 21:35, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    не H200 конечно, но всяко дешевле чем nvidia или mac - https://www.kickstarter.com/projects/tiinyai/tiiny-ai-pocket-lab
     
     
  • 6.109, Аноним (4), 21:57, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Есть сомнения в дешевизне т.к. его не получится подключать к дешманским ноутам.
    В дешёвых ноутах нет Thunderbolt 3/4.
     
  • 3.92, Аноним (92), 19:42, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > квантует

    Квантизация сильно ухудшает умственные возможности моделей. Даже если в бенчмарках заявляется о потери 1% производительности, на деле же там все 50%. Проверено лично на собственном проекте, тестируя fp4 и fp8 варианты одной модели.

     
  • 2.21, Джон Титор (ok), 12:18, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Данные свежие, март 2026 Строю большую сводную таблицу по тирам Тир 0 8212 ... большой текст свёрнут, показать
     
     
  • 3.60, Аноним (59), 15:28, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Спасибо!
     
     
  • 4.65, Аноним (4), 16:07, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Вы тоже самое можете спрашивать из чатов, как он и сделал:
    1) https://www.google.com/search?q=&hl=ru&aep=22&udm=50
    2) https://www.perplexity.ai
     
  • 4.96, Джон Титор (ok), 20:28, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    > Спасибо!

    Имей в виду что знания ИИ обновляются раз в год. Поэтому модели реально можно посмотреть более новые когда купите железо и поэксперементировать может оно поддерживает что-то лучше чем предложило ИИ. Даже не взирая на то что оно поискало свежую информацию, все-равно стоит самому поискать, может найдете для себя что-то лучше.

     
  • 4.97, Джон Титор (ok), 20:31, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    > Спасибо!

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

     
  • 2.66, Аноним (66), 16:08, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Чтобы нормально работать вся модель должна влазьть в VRAM, а RAM брать в дваразы больше: RAM = 2 * VRAM.

    Важно скорость работы VRAM и вычислительная способность видяхи в int8/s - больше значит лучше.


    В топовую видяху, сабжевая модель в память уже не влазит:
    Nvidia RTX PRO 6000 Workstation Edition Blackwell; 96GB DDR7 ECC; 1024 TOPS (Int8); -600W; PCI-E 5.0 x16

     
     
  • 3.69, Аноним (4), 16:12, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    NVIDIA H200
     
     
  • 4.77, Аноним (66), 17:12, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    > NVIDIA H200

    Посмотрел спеки на H200 NVL:
    VRAM - 141GB
    int8 - 3.3 PFLOPS (така видяшка и в TOP500 может попасть)
    VRAM HBM3E- 4.8TB/s

    Видяшку можно дробить аж на 7 мелких виртуальных

    Или можно объединять вплоть до 8 видеокарт в одну большую виртуальную:
    2- or 4-way NVIDIA NVLink bridge: 900GB/s per GPU
    PCIe Gen5: 128GB/s

     
     
  • 5.80, Аноним (4), 17:26, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    >така видяшка и в TOP500 может попасть

    Ну нет, там совсем другая точность. В топовых кластерах тысячи таких H200 установлено помимо CPU.

     
  • 3.117, vibecoder (?), 06:39, 18/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Никто не использует видеокарты вне дата-центров для запуска LLM. У нас в компании разорились на три Mac Studio и гоняем GLM-5 с очень приличной скоростью инференса.
     
     
  • 4.118, Аноним (118), 08:50, 18/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Сравни скорость памяти и скорость вычислений int8 Для запуска чужой готовой мод... большой текст свёрнут, показать
     
     
  • 5.121, Аналоговнет (-), 10:03, 18/03/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Он прав. Мак ты всегда продаш по очень ликвидной цене. А вот твоё б\у GPU нафиг никому не нужно, к тому же специализированное типа H200.

    > Для запуска чужой готовой модели мощностей современных CPU хватит

    С какой скоростью? Простите, но вы глупость пишете, особенно в контексте использования в компании с более чем двумя программистами одновременно и без квантизации.

     
     
  • 6.124, Аноним (124), 11:00, 18/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    CPU сегодня от видях не сильно отстаёт:
    Intel® Xeon® 6980P Processor
    504M Cache, 2.00 GHz; FCLGA7529; P Cores 48 + E Cores 80, MRDIMM(8800MT/s), PCI-E 5.0 96; 3nm; 500W; 12460$

    По скорости вычислений int8:
    Xeon® 6980P = 2/3 * RTX PRO 6000 Workstation Edition

     
     
  • 7.125, Аноним (-), 11:12, 18/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    > CPU сегодня от видях не сильно отстаёт:

    Память, шина и прочие бутылочные горлышки учитываются в вашем расчёте?

     
     
  • 8.131, Аноним (131), 17:19, 18/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Да учитывается Xeon 174 6980P - производительность в 838 TOPS int8 подтвержде... большой текст свёрнут, показать
     
  • 5.122, Аналоговнет (-), 10:05, 18/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    P.S. Вдогонку, обучать и тюнить модель выгоднее на облачном сервисе, где ты арендуешь топовые GPU для этой цели с почасовой оплатой. Свою покупать под это дело - глупость.
     
  • 2.68, nagual (ok), 16:10, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Вообще железо нужно мощьное, но облачный сервис всегда будет дешевле, + скидки + акции + пробные периоды на новые модели.
     
  • 2.107, Анонисссм (?), 21:08, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    >какое железо нужно, чтобы запустить

    "запустить" любой ПК с 128ГБ ОЗУ без ГПУ.
    я например на арендованных топовых райзенах с 128ГБ тестирую gpt-oss 120b и qwen-coder 122b. неспешно, но вполне быстро что-то колбасит. лично меня качество кода не устраивает и у моделей на 80ГБ. облачный sonnet/opus лучше, чтобы там в тестах не рисовали

     

  • 1.2, Джон Титор (ok), 11:34, 17/03/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    > В проведённых тестах модель Leanstral ощутимо обогнала существующие открытые модели Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B и GLM5 744B-A40B, показала сходные результаты с моделями Claude Haiku 4.5 и Claude Sonnet 4.6 от компании Anthropic, но отстала от модели Claude Opus 4.6.

    О, это уже не плохо. Sonnet 4 уже хорош, а 4.5 немного лучше. 4.6 там не особо то и сильно лучше. Если проверять что оно пишет, то 4.5 уже отличная помощь.

     
  • 1.8, Аноним (-), 11:48, 17/03/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +8 +/
    > AI-модель для вайб-кодинга с формальной верификацией

    Хихи, маркетологи нынче зажигают на тему взаимоисключающих параграфов.

     
     
  • 2.10, Аноним (10), 11:53, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    > Хихи, маркетологи нынче зажигают на тему взаимоисключающих параграфов.

    А где противоречие? Модель просто обучили в том числе на ошибках Aeneas.
    Модель выдает код, агент запускает верификатор, тот выдает какие-то ошибки, которые модель обрабатывает и исправляет код. После этого верификатор запускается повторно.
    Обычный close loop.

     
     
  • 3.15, Аноним (15), 12:03, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    В итоге, модель научится писать код, проходящий конкретный верификатор. А вовсе не нормально работающий
     
     
  • 4.16, Аноним (16), 12:06, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > В итоге, модель научится писать код, проходящий конкретный верификатор.
    > А вовсе не нормально работающий

    Если "не нормально работающий" код проходит ваш верификатор... то проблема в верификаторе.
    Потому что сам факт прохождения верификации должен давать гарантии соответствия спецификации.

     
     
  • 5.20, Хрю (?), 12:17, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +3 +/
    Вся проблема, что написать полностью правильную верификацию на код, не проще чем этот код написать 😃 Т.е. одну сложность заменили на другую 😃
     
     
  • 6.27, Аноним (-), 12:46, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/
    вот только сначала тебе в норме надо было написать и код верификации, и код под нее

    а сейчас надо написать верификацию, код нейробратан напишет

    не одну "сложность заменили на другую", а уполовинили сложность

     
     
  • 7.28, Хрю (?), 12:50, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Сейчас верификацию на код пишут, мягко скажем очень редко, и в мегакритикал системах, потому что это тяжёлая, сложная и очень затратная операция с малым колвом спецов по теме и небольшим колвом специального ПО. Гораздо проще и дешевле тупо написать код и облажить его тестами.
     
     
  • 8.32, Аноним (-), 12:55, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    тогда о чем разговор у нас нет верификатора, потому мы хотим, чтобы модель, зат... текст свёрнут, показать
     
     
  • 9.38, Хрю (?), 13:03, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Разговор про то что дешевле и лучше не стало, а просто одну сложность написание... текст свёрнут, показать
     
     
  • 10.40, Аноним (-), 13:05, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Дак стало или нет А там, где писали верификацию, стало легче или нет Или раз н... текст свёрнут, показать
     
     
  • 11.46, Хрю (?), 13:42, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Верификацию пишут для всяких контроллеров и т п критикал вещей, там не только н... текст свёрнут, показать
     
     
  • 12.63, Аноним (-), 16:03, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    я очень рад, что ты признаешь, что есть сферы, где верификация очень важна это н... большой текст свёрнут, показать
     
  • 8.37, Аноним (37), 13:02, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    облАжить тестами - это зачЁт ... текст свёрнут, показать
     
  • 7.30, Аноним (30), 12:51, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    > не одну "сложность заменили на другую", а уполовинили сложность

    Нюанс в том, что 99% 6ыdlo-кодеров никогда в жизни не писали спецификаций.
    Максимум смотрели в AC в задачке, которые выдавил из себе менеджер, и где-то в голове прикидывали эджкейсы. Ну, могли еще комментарий в коде оставить "вот тут может произойти такая х..., поэтому делаем так-то"

     
     
  • 8.35, Аноним (-), 12:56, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    вот то же самое тогда о чем разговор у нас нет верификатора, потому мы хотим, ч... текст свёрнут, показать
     
     
  • 9.47, aname (ok), 13:45, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –2 +/
    Анонимные эксперты с опеннета хотят, чтоб за них всё делала нейрослопть, а они с... текст свёрнут, показать
     
     
  • 10.94, Аноним (92), 20:02, 17/03/2026 Скрыто ботом-модератором     [к модератору]
  • +1 +/
     
     
  • 11.103, aname (ok), 20:39, 17/03/2026 Скрыто ботом-модератором     [к модератору]
  • +/
     
  • 4.51, Аноним (51), 13:51, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > В итоге, модель научится писать код, проходящий конкретный верификатор

    По-моему, ты путаешь формальную верификацию со статическим анализом. Формальная верификация не зависит от "конкретного верификатора", ибо код либо математически корректен, либо нет. Если один верификатор пропускает код, который второй верификатор посчитал некорректным - значит, в первом верификаторе баг.

     
  • 3.39, Аноним (34), 13:03, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    > ошибки, которые модель обрабатывает и исправляет код. После этого верификатор запускается повторно

    Но есть нюанс: процесс не обязан сходиться. Практика применения ИИ показывает, что 1+1 нейроslop ещё может научиться складывать, а более сложное - постоянно в ошибках.

     
     
  • 4.48, aname (ok), 13:46, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/
    Что значит "не обязан сходится"?

    Практика применения ИИ показывает, что от людей ИИ тупеет, и какие выводы из этого сделаем?

     
     
  • 5.55, Аноним (34), 14:37, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    С такими вопросами - к математикам, но они от ИИ тупеют, от того самого, который отупел.
     
     
  • 6.58, Аноним (58), 15:19, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    //www.youtube.com/watch?v=JHEO7cplfk8

    Вот наглядное пособие, приглядитесь по внимательней и сделайте вывод в качестве чего используется в данном контексте ЫЫ?

     
  • 4.64, Аноним (64), 16:06, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/
    >Но есть нюанс: процесс не обязан сходиться

    Какой процесс у тебя там не сходится? Верификация должна гарантировать соответствие спецификации. Всё. Сдается мне, что ты не в курсе, что такое верификация.
    >1+1 нейроslop ещё может научиться складывать, а более сложное - постоянно в ошибках

    А, ты и про ИИ не в курсе. Понятно всё.

     
     
  • 5.81, Аноним (34), 17:35, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Чем отличается верификация от имплементации - тебе надо рассказывать?
     
     
  • 6.114, anonymos (?), 03:51, 18/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Мне надо.
    Расскажи, будь ласка )
     
  • 4.93, Аноним (92), 19:58, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    > Практика применения ИИ показывает, что 1+1 нейроslop ещё может научиться складывать, а более сложное - постоянно в ошибках.

    Да вы батенька бред несете. Ну или ваша "практика" это модели из 2023 года.

     

  • 1.11, Аноним (11), 11:59, 17/03/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    Нейрослоп вышел на новый уровень.
     
     
  • 2.41, Аноним (34), 13:08, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Вангуется очередное повышение цен на память в 2 раза.
     
  • 2.44, Аноним (4), 13:13, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Ими кстати ASML заинтересовались:
    https://www.asml.com/en/news/press-releases/2025/asml-mistral-ai-enter-strateg
     
  • 2.90, Аноним (92), 19:35, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Нейрослоп

    Слоп остался в 2023 году. Нынче нейронка в большинстве случаев генерирует более качественный код, чем человек. Другое дело, что полностью ей доверять нельзя и все равно нужно руками потом переписывать (в 90% случаев - упрощать её Ынтерпрайзные паттерны).

     

  • 1.22, Аноним (22), 12:20, 17/03/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +4 +/
    > позволяет подтвердить, что сгенерированный AI-моделью код делает именно то, что задумано

    Осталось теперь подтвердить, что описанное в спецификации - это именно то, что и было задумано

     
     
  • 2.49, aname (ok), 13:48, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    Ну если условные "вы" не способны написать спецификации, то тут не только нейрослопть бессильна, тут даже у медицины на этом полномочия всё.
     
     
  • 3.62, Аноним (58), 15:32, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    > Ну если условные "вы" не способны написать спецификации, то тут не только
    > нейрослопть бессильна, тут даже у медицины на этом полномочия всё.

    //www.youtube.com/watch?v=JHEO7cplfk8

    Ну вот, чем, по вашему, тут занята ЫЫ?

     
     
  • 4.78, aname (ok), 17:13, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    >> Ну если условные "вы" не способны написать спецификации, то тут не только
    >> нейрослопть бессильна, тут даже у медицины на этом полномочия всё.
    > //www.youtube.com/watch?v=JHEO7cplfk8
    > Ну вот, чем, по вашему, тут занята ЫЫ?

    Главное, что понаделал кожаный мешок

     
     
  • 5.84, Аноним (58), 17:58, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    ну так чем там занята ЫЫ?
     
     
  • 6.105, aname (ok), 20:40, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > ну так чем там занята ЫЫ?

    Писала коммент, на который я сейчас отвечаю

     
     
  • 7.110, Аноним (58), 22:54, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +/
    ч. и. т. д.
     
  • 2.74, Аноним (73), 16:32, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Вы совершенно правы, я ошиблась в спецификации - ваш рентгеновский аппарат совершенно точно не должен выжигать пациентам суставы в порошок, так что вот вам новая, исправленная, спецификация.
     

  • 1.31, Аноним (34), 12:53, 17/03/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    > математического доказательства корректности

    не гарантирует, что код оптимальный. Чтобы получить "единицу", можно сделать 0+1, а можно сумму квадратов косинуса и синуса, разложенных в ряды, вычисляемых через soft-float повышенной разрядности, от случайного аргумента, полученного криптографически через энтропию устройств ввода-вывода системы.

     
     
  • 2.36, Аноним (36), 13:02, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/
    > не гарантирует, что код оптимальный

    А мясной мешок гарантирует оптимальность?))

    Ну и какую именно оптимальность?
    По памяти? По вычислениям? По минимальности операций для fpu?
    Вы вначале сформулируйте требования.

     
     
  • 3.61, Аноним (58), 15:30, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > Вы вначале сформулируйте требования.

    Ну вот с этого надо и начинать, это равносильно понятию эффективно вычислимой функции (нормальному алгорифму) во времена Черча, Тьюринга, Поста, Маркова.


     
  • 3.88, Аноним (92), 19:32, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/
    > А мясной мешок гарантирует оптимальность?))

    Мясной мешок держит в голове контекст длиною в жизнь, и знает в каких случаях оптимально то или иное решение (если это не стажёр или джун).

     
  • 2.50, aname (ok), 13:51, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • –2 +/
    Ну так критерии оптимальности, для начала, завезите.
     

  • 1.43, Bob (??), 13:12, 17/03/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/
    Вайбкод:
    1) модель тренировали на общедоступном мусоре, а не топовых примерах кода и коммерческом софте
    2) задача максимум токенов "сожрать/выплюнуть" - чтобы платили
    3) общение напоминает диалог глухо-немого со слепым
    4) в тесте не учли человекочасы на годный результат
     
     
  • 2.86, Аноним (92), 19:29, 17/03/2026 [^] [^^] [^^^] [ответить]  
  • +2 +/
    Ты ошибаешься, модели тренируют как раз на Ынтерпрайзном коде, отсюда и берутся хеллоуворлды с клиент-серверными архитектурами на boot spring. Вместо простой функции, модель в большинстве случаев пишет 100500 абстракций, даже если это нафиг не нужно.
     

  • 1.85, Аноним (92), 19:28, 17/03/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +5 +/
    Современные AI итак генерируют *синтаксически* верный код в 99% случаев. Проблема в логических и архитектурных решениях.
     
  • 1.123, Джон Титор (ok), 10:39, 18/03/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/
    А если поставить Aider, то больше команда разработчиков не нужна
     

     Добавить комментарий
    Имя:
    E-Mail:
    Текст:



    Партнёры:
    PostgresPro
    Inferno Solutions
    Hosting by Hoster.ru
    Хостинг:

    Закладки на сайте
    Проследить за страницей
    Created 1996-2026 by Maxim Chirkov
    Добавить, Поддержать, Вебмастеру