Профиль: Аноним (вход | регистрация) неRU opennet.me  
OpenNET

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

Аnthropic развивает технику для формальной верификации существующего ПО при помощи AI

23.10.2026 10:06 (MSK)

Компания Аnthropic представила результаты экспериментов по использованию AI-моделей для формальной верификации надёжности и безопасности уже существующих проектов. В ходе эксперимента при помощи AI-моделей для 123 открытых библиотек, протестированных в инфраструктуре OSS Fuzz, были сгенерированы математические доказательства отсутствия ошибок при работе с памятью.

Проверка проводилась на уровне скомпилированного ассемблерного кода для архитектуры RISC-V. Общий объём сгенерированных доказательств составил около 180 миллионов строк кода для системы верификации Rocq Prover (около 600 тысяч строк на бинарный файл с 18 тысячами RISC-V инструкций). Доказательства формировались путём автоматического преобразования существующих fuzzing-тестов в формальные спецификации, после чего AI-модель Claude доказывала, что при любых входных данных объёмом до 64 МБ в программе не возникает сбоев.

В процессе построения доказательств AI-модель смогла выявить и подготовить исправления для сотен ошибок, ранее не замеченных при fuzzing-тестировании. Среди прочего, были выявлены уязвимости, приводящие к переполнению буфера при обработке определённых входных данных (например, CVE-2026-56132 в libexpat), а также логические ошибки. Помимо этого, AI-модель была использована для доказательства соответствия реализации алгоритма zlib в ядре Linux спецификации RFC 1950.

Также на языке Rust был сгенерирован интерпретатор для подмножества языка Python, для которого при помощи инструментария Verus подготовлено формальное доказательство соответствия семантике CPython. Для сравнения поведения с CPython было выполнено более 1.7 миллионов случайно сгенерированных Python-программ. В 99.95% случаев результаты выполнения этих программ в новой реализации и в CPython совпали, а выявленные расхождения оказались известными граничными случаями.

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

  1. Главная ссылка к новости (https://www.anthropic.com/rese...)
  2. OpenNews: Выполнена формальная верификация безопасности микроядра seL4 для архитектуры AArch64
  3. OpenNews: В Python задействованы криптофункции с математическим доказательством надёжности
  4. OpenNews: Mistral опубликовал Leanstral, AI-модель для вайб-кодинга с формальной верификацией
  5. OpenNews: Первый выпуск QSOE, операционной системы в стиле QNX с двумя заменяемыми микроядрами
  6. OpenNews: Компания Canonical представила проект по разработке транслятора с Си на Rust
Лицензия: CC BY 3.0
Короткая ссылка: https://opennet.ru/66528-ai
Ключевые слова: ai, verify
При перепечатке указание ссылки на opennet.ru обязательно


Обсуждение (141) Ajax | 1 уровень | Линейный | +/- | Раскрыть всё | RSS
  • 1.3, pic (??), 10:47, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • –3 +/–
    Очень быстро ИИ опуститься до уровня машинных кодов и библиотеки, тулкиты, фреймворки станут бесполезны.
     
     
  • 2.6, Аноним (6), 10:51, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +29 +/–
    точно быстрее чем еи - естественный интеллект - начнёт различать -тся и -ться
     
     
  • 3.21, miu (?), 11:24, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +1 +/–
     
     
  • 4.22, Bottle (?), 11:29, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +/–
     
  • 3.24, pic (??), 11:38, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –3 +/–
    Приставку бес- тоже отмените, она не несёт смысловой нагрузки, без- хотя бы этим отличается.
    Ох уж эти "академики".
     
     
  • 4.25, q (ok), 11:45, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/–
    отличаеться*
     
     
  • 5.28, pic (??), 11:47, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/–
    Лично для здешних обитателей только с мягким знаком, в качестве наказания.
     
  • 5.144, Аноном (?), 18:26, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    -тся, вообще-то.
     
  • 4.73, Аноним (73), 13:33, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    А ещё ЕИ таки выучит правило правописания приставок, оканчивающихся на "с" и "з" https://ruhomeschool.ru/russkiiyazyk/z-i-s-na-koncze-pristavok
     
     
  • 5.119, pic (??), 16:01, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/–
    Приставка бес- не имеет логического смысла и была придумана при коммунистах.
     
     
  • 6.128, Аноним (128), 16:51, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Ну это враньё
     
     
  • 7.133, Пыщь (?), 17:34, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +/–
     
  • 7.138, pic (??), 18:07, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    И какой же у неё смысл?
     
  • 3.26, pic (??), 11:46, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –3 +/–
    В русском языке традиционно применяются французские «ёлочки», а для кавычек внутри кавычек и при письме от руки — немецкие „лапки“ или "скандинавские".

    В рукописном тексте не применяются кавычки "ёлочки", используются "лапки".
    И обозначают они одно и тоже - цитату, прямую речь, отсылку.

     
     
  • 4.102, Пыщь (?), 14:33, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    отсос у невросети засчитан.
     
     
  • 5.118, pic (??), 15:59, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Ваша профессия умирает, идите в смежную, а агонизировать из-за нет смысла - не поможет.
     
     
  • 6.131, Пыщь (?), 17:31, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • –2 +/–
     
  • 6.137, pic (??), 18:05, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Мне не надо знать кем работаешь, я не комплексую из-за ошибок.
    Лучше бы по существу писал своё мнение по теме.
     
  • 5.139, pic (??), 18:09, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    О, как уважительно, смотрю вас хорошо воспитали.
     
  • 5.140, pic (??), 18:13, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    https://ru.wikipedia.org/wiki/Кавычки

    Читай умник.

     
  • 2.8, Аноним (8), 10:59, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +2 +/–
    Хоть какая-то польза от ИИ. Очистить ПО ландшафт от наслоившегося мусора в виде фреймворков, жабаскрипта, раста и всякой питонщины.
     
     
  • 3.75, Аноним (73), 13:38, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    От фреймворков - не дождётесь.
     
  • 3.113, Аноним (113), 15:32, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +1 +/–
     
  • 3.154, Аноним (154), 19:24, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > Хоть какая-то польза от ИИ. Очистить ПО ландшафт от наслоившегося мусора в виде

    ...в видебиомассы программистов азазазаза!

     
  • 2.10, Аноним (10), 11:02, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/–
    Останутся только чисто функциональные языки, запомните этот твит!
     
     
  • 3.37, pic (??), 12:11, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Тогда придётся и дальше плодить оптимизирующие компиляторы.
    Зачем?

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

    Подсказывать не буду.

     
     
  • 4.49, Аноним (10), 12:45, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/–
    Функциональщина поможет составлять непротиворечивые промпты. ИИ сама будет основана на этом языке. Нейро символические ИИ.
     
  • 3.47, Боевой Петух (?), 12:31, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –2 +/–
    Не останется вообще никаких языков, кроме промптинга. Уже через пару лет ИИ будет генерировать машинный код напрямую и коНпилятор станет не нужОн. Запомните этот твит.
     
     
  • 4.52, Аноним (10), 13:05, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +2 +/–
    Если составлять промпты, как ты пишешь комментарии, то на выходе получится ещё хуже, чем у джуна на C/C++
     
     
  • 5.101, Аноним (101), 14:33, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/–
    Но гораздо дешевле. А качество софта волнует не тех, кто его пишет, а тех, кто его использует. Так что всё правильно он написал.
     
  • 5.141, Аноним (141), 18:14, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/–
    > Если составлять промпты, как ты пишешь комментарии, то на выходе получится ещё хуже, чем у джуна на C/C++

    Найс коупинг от 50 летнего корадубщика, который та и не вошел в IT

     
  • 2.12, Ы (?), 11:07, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/–
    Посмотри на «прибыль» антропик.
    Очень скоро может может пузырь лопнет и все опять вернутся к услугам кожаных мешков
     
     
     
    Часть нити удалена модератором

  • 4.64, Аноним (64), 13:20, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Ну несколько лет назад биткойн постоянно лопался, теперь вот ИИ.
     
     
  • 5.124, Аноним (113), 16:16, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    А что, Биткоин генерировал астрономические убытки? Обожаю аналитику на опенке.
     
     
  • 6.149, Инопланетянин (?), 18:55, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > А что, Биткоин генерировал астрономические убытки? Обожаю аналитику на опенке.

    У кого-то генерировал

     
  • 2.35, pic (??), 12:07, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –3 +/–
    В произношении инфинитив не всегда ощущается по мягкому произношению.
    Скорее по ударению, но и ударение тоже бывает одинаковым при спряжении.

    Поэтому старые правила, что по советской реформе, что до неё, создают двойные стандарты.
    Нужна новая реформа.

     
     
  • 3.103, Пыщь (?), 14:35, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +/–
     
  • 2.82, Аноним (82), 13:44, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    ИИ считать нормально не умеет. Скрипты для этого пишет. Путается в перенумерации текстовых документов даже со скриптами, а ты про бинарники.

    Что бы такое делать надо держать модель процессора внутри модели ИИ. Сейчас нет таких механизмов, что бы создавать такие структуры. И никто даже не начинал работать в этом направлении.

     
     
  • 3.97, Аноним (10), 14:09, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Модель riscv проца с базовым набором инструкций не сильно больше модели языка brainfuck
     
  • 3.125, Аноним (113), 16:18, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    "что бы" пишет раздельно, но все ИИ критикует...
     
  • 3.136, pic (??), 18:02, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Кучер сравнивает Теслу со своей повозкой.
     
  • 3.156, Аноним (154), 19:32, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > ИИ считать нормально не умеет.

    Ты из танка-то вылези. ИИка вон недавно порешала более 300 математических задач, над которыми лучшие математики планеты тщетно бились десятилетиями. Включая уравнения Навье-Стокса.

    А вашу корявую кучу г*кода не осилит, ага...

     
  • 2.147, Инопланетянин (?), 18:29, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > Очень быстро ИИ опуститься до уровня машинных кодов и библиотеки

    Rocq Prover это уже машинный код у тебя?

     

     ....большая нить свёрнута, показать (42)

  • 1.5, Аноним (6), 10:50, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • –1 +/–
    тэк, огромадные специалисты в бям (больших языкастых моделях)
    если бинарный файл собирается из одного исходника, но с разными параметрами оптимизации например, бям верифицирует конкретную сборку, или всё же логику исходного кода?
     
     
  • 2.9, Аноним (10), 10:59, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +5 +/–
    Что такое логика исходного кода? Особенно, когда на таких языках как C/C++ каждая вторая строчка это UB? На процессоре выполняется машинный код, его и надо верифицировать, а не какие то влажные мечты Васяна написанные на дырявом языке.
     
     
  • 3.15, Ы (?), 11:09, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Начать надо с верификации верилога процессора. А то окажется что там напортачили со спекулятивным исполнением инструкций 🤷♂
     
     
  • 4.17, Аноним (10), 11:12, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +2 +/–
    Поэтому и проверяют на riscv, где есть железо без этого барахла
     
     
  • 5.39, Аноним (39), 12:19, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +2 +/–
    А есть и с барахлом. RISC-V — это ISA, а не реализация (и в этом смысле в плане уязвимостей много хуже, т.к. несколько десятков производителей вам такой их феерический набор произведут).
     
     
  • 6.53, Аноним (10), 13:06, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    С барахлом станет никому не нужно. Концепция поменяется
     
  • 5.41, Аноним (41), 12:23, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > железо без этого барахла

    Железо без этого оказалось не очень востребованным на рынке.

     
     
  • 6.51, Аноним (10), 12:50, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/–
    Потому что кожаные не могут придумывать подходящий для железа лайаутинг данных и алгоритмы их обработки
     
  • 5.88, Аноним (73), 13:51, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    По-вашему, реализации архитектуры RISC-V написаны на святам духе? Они также написаны на HDL: Verilog, Chisel.
     
     
  • 6.93, Аноним (10), 13:59, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Нет, но есть железо без существующих дырявых концепций, как предсказание ветвлений и кеш
     
     
  • 7.104, Аноним (39), 14:52, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Ага, микроконтроллеры всякие.
     
     
  • 8.105, Аноним (10), 15:07, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    В riscv есть on chip sram, гораздо лучше чем кеш, если уметь программировать Ко... текст свёрнут, показать
     
  • 8.106, Аноним (106), 15:07, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    рассмешил, открой армовый М профиль и посмотри сколько UB в его ISA ... текст свёрнут, показать
     
     
  • 9.142, Аноним (10), 18:21, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Не сравнивал жопу с пальцем, arm и riscv... текст свёрнут, показать
     
     
  • 10.152, Аноним (106), 19:15, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    подробней ... текст свёрнут, показать
     
  • 7.114, Аноним (73), 15:37, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Да даже без если кеша вообще и без спекулятива, всё равно, проектируюься на HDL. Не думаете же ли вы, что топологию на куче ватманов расчерчивают
     
  • 4.150, Инопланетянин (?), 18:56, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > Начать надо с верификации верилога процессора. А то окажется что там напортачили
    > со спекулятивным исполнением инструкций 🤷♂

    Так ты токены не продашь хомякам

     
  • 3.19, Аноним (19), 11:22, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –3 +/–
    Кожаные гении, посчитайте, сколько UB в этом ванильном и типичном коде самого популярного языка на планете:

    int sum;
    for (int i = 0; i <= INT_MAX; i++)
        sum += 2;

     
     
  • 4.23, Bottle (?), 11:34, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +3 +/–
    1. Неявно задана сумма.
    2. Когда индекс станет инт_макс, будет знаковое переполнение.
    3. Сумма к тому моменту будет знаково переполнена дважды? Нет уверенности из-за первого неопределённого поведения.
     
     
  • 5.54, Аноним (10), 13:08, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –2 +/–
    Вот, а это типичный код, которого миллионы строк на github. Обученный ИИ до такого никогда не додумается
     
     
  • 6.65, Смузихеб забывший пароль (?), 13:21, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/–
    едва ли это типичный код
    вдобавок, а на каком коде, думаешь, этот ИИ обучают ?)
     
     
  • 7.71, Аноним (10), 13:33, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Надеюсь, что не на таком. Или такой используют для контрпримеров
     
     
  • 8.78, Аноним (82), 13:41, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Забавный вы И очень наивный ... текст свёрнут, показать
     
     
  • 9.91, Аноним (10), 13:57, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Расскажи как проходит обучение трансформера языку программирования, а мы послуша... текст свёрнут, показать
     
     
  • 10.96, Аноним (82), 14:01, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Что такое трансформер ... текст свёрнут, показать
     
     
  • 11.98, Аноним (10), 14:14, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +1 +/–
     
  • 11.110, Аноним (82), 15:17, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Ответ на реплику выше трансформер 8212 это удачный маркетинговый бренд Реаль... текст свёрнут, показать
     
  • 7.86, Аноним (86), 13:47, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    А на каком его ещё обучать, если другого нет? В php или linux дыры от хорошей жизни завелись?
     
     
  • 8.95, Аноним (10), 14:01, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/–
    Тем дырам сто лет в обед, когда ещё на слуху были только экспертные системы в ме... текст свёрнут, показать
     
     
  • 9.127, Аноним (86), 16:30, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +/–
     
  • 4.29, Аноним (29), 11:48, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/–
    Слишком просто. Попробуйте ещё раз.
     
  • 4.100, Аноним (100), 14:27, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/–
    Даже впадлу такой бред разбирать, тут и переполнение и использование неинициализированной переменной. А бред потому что покажи пример этого "типичного" кода в опенсорсе. Можно прям ссылкой на номер строки в гитхабе.
     
     
  • 5.112, Аноним (10), 15:26, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –6 +/–
    Да без проблем. Тыкнул в случайный файл DPDK, который кстати в другой новости обсуждается. И что мы видим?

    static void
    graph_insert_ordered(struct graph *graph)
    {
    struct graph *after, *g;

    after = NULL;
    STAILQ_FOREACH(g, &graph_list, next) {
    if (g->id < graph->id)
    after = g;
    else if (g->id > graph->id)
    break;
    }
    if (after == NULL) {
    STAILQ_INSERT_HEAD(&graph_list, graph, next);
    } else {
    STAILQ_INSERT_AFTER(&graph_list, after, graph, next);
    }
    }

    Переменная after инициализируется в первом цикле только в одной ветке. И следующая проверка if (after == NULL) что нам скажет, если сишники принципиально не инициализирует свои переменные при объявлении?

    И это код который используется в датацентрах и финтехе, Карл!

     
     
  • 6.116, черпало (?), 15:41, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +2 +/–
    Ты дебил или троллишь?
    Кекспертиза как всегда.

    after = NULL прямо перед форычем, ты внатуре такой дебил?


    Почему, почему именно такие персоны и орут больше всех? Боже, за что всё это

     
     
  • 7.117, Аноним (10), 15:54, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • –4 +/–
     
     
  • 8.134, черпало (?), 17:56, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +1 +/–
     
  • 8.135, черпало (?), 17:59, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +/–
     
  • 4.151, Инопланетянин (?), 18:56, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > Кожаные гении, посчитайте, сколько UB в этом ванильном и типичном коде самого
    > популярного языка на планете:
    > int sum;
    > for (int i = 0; i <= INT_MAX; i++)
    >     sum += 2;

    Справедливости ради современные компиляторы выдадут предупреждение и ИИ выдаст тебе проблемы этого кода, если попросить.

     
     
  • 5.153, черпало (?), 19:17, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > Справедливости ради

    если кому-то нужно в этом коде искать проблемы аж с помощью ии, то ставлю коньяк, что этот спесалист ложку к уху несет, слюни у него капают, в речи отмечаются слова "раст", "дырени", и проч, вид имеет очень важный и напыщенный.

    кажется, когда эти спесалисты были ростом меньше метра, компиляторы это умели.

    Действительно кто-то думает, что с ии эти персонажи СМОГУТ?

     
     
  • 6.155, Инопланетянин (?), 19:31, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    >> Справедливости ради
    > если кому-то нужно в этом коде искать проблемы аж с помощью ии,
    > то ставлю коньяк, что этот спесалист ложку к уху несет, слюни
    > у него капают, в речи отмечаются слова "раст", "дырени", и проч,
    > вид имеет очень важный и напыщенный.
    > кажется, когда эти спесалисты были ростом меньше метра, компиляторы это умели.
    > Действительно кто-то думает, что с ии эти персонажи СМОГУТ?

    По факту это косяки языка и они есть. В расте их нет, по крайней мере выше перечисленных. Пробелма в том, что они могут вылезти в других ситуациях, примеров переполнений полно в cve.

     
  • 6.157, Инопланетянин (?), 19:37, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    >> Справедливости ради
    > если кому-то нужно в этом коде искать проблемы аж с помощью ии,
    > то ставлю коньяк, что этот спесалист ложку к уху несет, слюни
    > у него капают, в речи отмечаются слова "раст", "дырени", и проч,
    > вид имеет очень важный и напыщенный.

    Другой вопрос: почему простой цикл таит в себе столько проблем? Потом удивляемся почему раст предпочитают с++. Конечно, когда ты с большим опытом, то для тебя кажтеся это очевидным, ведь ты уже прошел 10 раз по граблям и набил шишек. Вот только даже у таких код , собранный с fsanitize падает, а в проде cve. И внезапно компиляторы стали анализировать и давать ворнинги, хотя раньше ub была "фишкой".


     
  • 3.80, Аноним (100), 13:43, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/–
    > когда на таких языках как C/C++ каждая вторая строчка это UB?

    Т.е. LLVM, который написан на C++, получается весь в UB? Это ж получается и раст компилится таким компилятором? Оу вей...

     
     
  • 4.89, Аноним (10), 13:55, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –3 +/–
    Прикинь, да... Нет ничего совершенного в этом мире. Алиасинг в LLVM чинили 10 лет, что бы он заработал как было спроектировано, а не как написано Васянами на C++.
     
  • 2.11, Аноним (29), 11:05, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Воспроизводимость сборки и верификация кода - вещи разные, обе полезные.
     
     
  • 3.13, Аноним (10), 11:07, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –2 +/–
    Воспроизводимость сборки это тестирование компилятора. А зачем нужен компилятор когда ИИ умеет сразу в машинный код?
     
     
  • 4.27, Аноним (29), 11:47, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/–
    > Воспроизводимость сборки это тестирование компилятора.

    Нет.
    > А зачем нужен компилятор когда ИИ умеет сразу в машинный код?

    Тоже нет.

    Ещё вопросы?

     
     
  • 5.58, Аноним (10), 13:13, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/–
    Успешно прошел психологический курс - как научиться говорить нет?
     
  • 5.59, Аноним (10), 13:15, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/–
    Отвечу в стиле отладчика CP/M

    - ?

     
  • 4.108, Аноним (106), 15:11, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > А зачем нужен компилятор когда ИИ умеет сразу в машинный код?

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

     
  • 2.32, Аныным (?), 12:00, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Вопрос изначально некорректный, так исходный код описывает логику в рамках абстрактного исполнителя, оставляя кучу всего на откуп конкретного компилятора/интерпретатора.
    В случае анализа бинарников LLM просто статистическими методами пытается увидеть общую картину, но чаще всего это сложно, так как окно контекста забивается безумным объемом мелкозернистой логики.
     
     
  • 3.57, Аноним (10), 13:11, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Объемы логики это чисто техническая проблема, со временем научится обрабатывать все больше и больше
     
  • 3.109, Аноним (106), 15:13, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > так исходный код описывает логику в рамках абстрактного исполнителя

    рассмешил, ни один современный ЯП не описывает логику в рамках абстрактного исполнителя, а фактически повторяет своего исполнителя, тот же С, С++ и т.д.

     
     
  • 4.120, Аноним (10), 16:03, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    А как же SQL?
     
     
  • 5.126, Аноним (113), 16:26, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Еще скажи HTML... точнее HTML + CSS, они же вместе тьюринг полные.
     
     
  • 6.132, Аноним (106), 17:31, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > Еще скажи HTML... точнее HTML + CSS, они же вместе тьюринг полные.

    да у него ведь бесконечная лента как у Тьюринга :)

     
  • 5.130, Аноним (106), 17:30, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > А как же SQL?

    давай, скомпилируй ка мне программу на несуществующей БД :)))

     
  • 2.33, Аноним (86), 12:01, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    >тэк, огромадные специалисты в бям (больших языкастых моделях)

    БЯМ здесь не имеет абсолютно никакого отношения, речь исключительно о компиляции.

    >если бинарный файл собирается из одного исходника, но с разными параметрами оптимизации например, бям верифицирует конкретную сборку, или всё же логику исходного кода?

    БЯМ верифицирует один единственный файл. Если в процессе сборки что-то поменять, например заменить компилятор (gcc -> clang, gcc11 -> gcc12), любой флаг сборки -O0 -> -O2, то всё нужно начинать с нуля. Даже если бинарный патч наложить, то всё опять же с нуля.

     

     ....большая нить свёрнута, показать (56)

  • 1.16, Метрика (?), 11:10, 23/10/2026 Скрыто ботом-модератором [﹢﹢﹢] [ · · · ]     [к модератору]
  • +1 +/–
     

  • 1.31, Аноним (86), 11:57, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +2 +/–
    >Ключевым преимуществом предложенного подхода является работа непосредственно с бинарными файлами, что позволяет обойтись без необходимости переписывания существующего кода на формально верифицируемых языках.

    Кому-то некуда деть деньги. Любая перекомпиляция и начинай всё с начала, с нуля.

     
     
  • 2.69, Аноним (10), 13:31, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/–
    В этом суть экономики. Или ты продвигает принцип - экономика должна быть экономной?
     

  • 1.36, Аноним (41), 12:09, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/–
    > были сгенерированы математические доказательства отсутствия ошибок при работе с памятью

    Растерманы сейчас потеряют работу.

     
     
  • 2.62, Аноним (10), 13:18, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Не, они будут предпоследними
     

  • 1.38, Аноним (41), 12:15, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +2 +/–
    > на языке Rust был сгенерирован интерпретатор для подмножества языка Python
    > В 99.95% случаев результаты выполнения этих программ в новой реализации и в CPython совпали

    Тут сразу узнаётся разработка на безопасном языке, никогда не совпадающая по результату с оригиналом.

     
     
  • 2.67, Аноним (10), 13:29, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/–
    Потому что в оригинале вместо логики - UB.
     
     
  • 3.74, Аноним (82), 13:37, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > Потому что в оригинале вместо логики - UB.

    Ты новости не читал? Там граничные случаи. На которые формальная верификация положила. От такого я аж прослезился.

    Верификация не проверяющая граничные случаи.... :)))

     
     
  • 4.77, Аноним (10), 13:40, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Ну ты так же ржал над первыми ИИ пару лет назад.
     
     
  • 5.123, Xasd1 (?), 16:15, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    это был не он
     

  • 1.40, нах.. (?), 12:23, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +4 +/–
    я за ai, но что новость про платный проприетарный продукт забыла на opennet?
     
     
  • 2.44, Аноним (41), 12:28, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > про платный проприетарный продукт забыла на opennet?

    Забыли домен сменить на comnet

     
  • 2.55, beany (?), 13:09, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +/–
     

  • 1.43, Боевой Петух (?), 12:26, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/–
    Корадубщики за 50, а так же все джуны и вайтишники за 40, что с лицом?
     
     
  • 2.46, Аноним (46), 12:29, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +/–
     
     
  • 3.48, Боевой Петух (?), 12:34, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +/–
     
  • 2.61, Аноним (8), 13:17, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Покажи на этой обезьяне куда тебя укусил коредуба за 50.
     
  • 2.68, Смузихеб забывший пароль (?), 13:30, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    > но полностью не исключает возникновение проблем с безопасностью
    > вызванные проблемами с многопоточностью,
    > динамическим связыванием и
    > аномальным поведением реального оборудования

    а что с лицом должно быть ?

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

     
  • 2.81, Аноним (73), 13:44, 23/10/2026 Скрыто ботом-модератором     [к модератору]
  • +/–
     

  • 1.63, Аноним (63), 13:18, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/–
    Уже выявили политические установки в весах китайских моделей - они допускают больше дыр для американских клиентов и существенно меньше для своих китайских. Ничто не мешает быть подобному и у антропиков.
    Поэтому флаг в руки и верьте всему что скажет ИИ
     
     
  • 2.66, Аноним (10), 13:28, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Старо как мир, любое изобретение используется как оружие в первую очередь.
     
  • 2.76, Смузихеб забывший пароль (?), 13:38, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Это не просто "не мешает"
    Наверняка будет нечто вроде хмурых дядек из экспортного контроля( как было с амуде и его сотрудничеством по "китайскому процессору" ), которым потребуется именно фактически доказать и гарантировать, что эти наработки не ухудшат конкурентноспособность и положение на рынке американских компаний и не позволят зарубежным конторам получить преимущество перед ними

    Поэтому, в случае с той же амуде, китайцам, к примеру, достался лишь "выхлоп от исходников", где они могли менять параметры лишь одного блока( шифрование. На китайское ) и всё это на уже устаревшей архитектуре( т.е получался устаревший амд-проц с изменённым аппаратным шифрованием )
    И это всё было полностью завязано на техпроцессы амд. В итоге, китайцы там что-то меняли, отправляли в амд, которая уже сама делала им кристаллы и после - отгружала в китай. От отправки в амд до получения кристаллов проходило неск мес - где-то полгода.

     
     
  • 3.85, Аноним (10), 13:47, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Поэтому российским разрабам сам бог велел использовать строгие языки, как rust, при использовании буржуйских ИИ
     

  • 1.70, Аноним (70), 13:32, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/–
    LOL. Оно чё, пихало в каждую переменную при вызове библиотечных функций по 64 мега данных? Это уже уровень школоло или уже техдира?
     
     
  • 2.79, Аноним (10), 13:43, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/–
    Проспись, какие переменные? Информатику надо было посещать в школе
     
     
  • 3.83, Аноним (70), 13:45, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Новость дочитать до конца могут не только лишь все?
     
  • 3.84, Аноним (70), 13:47, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Да какая разница, указателями пихать или через другие варианты типа стека. 64 мега всё равно впихуются в функцию в их тестах.
     
     
  • 4.87, Аноним (10), 13:49, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Какие указатели, какой стек? Есть регистры и память - все. Остальное зашито в инструкциях, какие байты куда перекладывать
     
     
  • 5.115, Аноним (70), 15:37, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Какие именно регистры ты нашёл в статических или динамических сбилженных либах? Оно тестило либы, а не вгруженный в память поток функций же... Либу сначала надо подтянуть, потом впихуть данные... а не в регистры писать указатели.
     

  • 1.72, Аноним (82), 13:33, 23/10/2026 Скрыто ботом-модератором [﹢﹢﹢] [ · · · ]     [к модератору]
  • +2 +/–
     
  • 1.90, Аноним (90), 13:56, 23/10/2026 Скрыто ботом-модератором [﹢﹢﹢] [ · · · ]     [к модератору]
  • +/–
     
  • 1.99, опеншлёпивпродакшн (?), 14:24, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/–
    Получается сначала мы создаём компьютеры и пишем программы, а потом нам нужен ИИ, чтобы во всём этом разобраться. Мне кажется, что игроки железного рынка и игроки ИИ рынка не связаны друг с другом, и сейчас происходит крупное смещение капитала в мире. Возможно даже первые как раз мощно инвестируют во вторых для удержания рычагов власти. В таком случае Сэм Альтман не злодей, а козёл отпущения.
     
     
  • 2.111, Аноним (106), 15:22, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • –1 +/–
    Раньше железо каждый в своем гараже делал, а щас? То же ждет и ПО, готовьтесь, зачем волю давать рабам.
     
     
  • 3.121, Аноним (10), 16:05, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    Ну у нас Нива есть, которую в гараже можно допиливать, а вот другим не повезет
     
  • 3.148, Боевой Петух (?), 18:30, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +1 +/–
    Наоборот, с появлением AI возникло множество проектов, где один человек пилит проект лучше, чем там, где кожмешки годами топтались на месте.
     
  • 2.146, Аноним (146), 18:28, 23/10/2026 [^] [^^] [^^^] [ответить]  
  • +/–
    >а потом нам нужен ИИ, чтобы во всём этом разобраться. Мне кажется, что игроки железного рынка и игроки ИИ рынка не связаны друг с другом

    Вещь в себе,
    Когда что то делается не ради чего то, а ради самого делания.
    Вот только это забавы корпоратов.
    Дорожает Озу на генерацию котиков, и на всякие хотелки.

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

     

  • 1.107, Аноним (107), 15:08, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/–
    Очень хорошее применение для ИИ.
     
  • 1.122, Xasd1 (?), 16:11, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/–
    > так как остаются неформализованными
    > риски, вызванные проблемами с
    > многопоточностью

    ну всё, ребята, расходимся..

    то есть даже срааное банальное time-of-check-to-time-of-use это не подсвечивает 🙈🙈🙈

     
  • 1.143, Аноним (143), 18:22, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +1 +/–
    Сначала они показали, что параметры какие надо параметры https://www.opennet.me/opennews/art.shtml?num=66497. Теперь они покажут, что их верификация самая настоящая верификация. Они уверено продвигаются к цели.
     
  • 1.145, Инопланетянин (?), 18:27, 23/10/2026 [ответить] [﹢﹢﹢] [ · · · ]  
  • +/–
    Ну вот инженеры-верификаторы тоже напряглись, дверь на улицу приоткрылась и оттуда подул холодный ветерок.
     

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



    XSQUARE
    Inferno Solutions
    Hosting by Hoster.ru
    Хоcтинг: