ИИ генерирует проверочные утверждения для чипов — но чуть переписали код, и всё ломается

Исследователи проверили, насколько устойчивы проверочные утверждения, сгенерированные нейросетями, к косметическим изменениям в коде железа. Результат неутешителен: переименование переменной — и до 27% правильных ответов превращаются в мусор.

Нейросеть может идеально проверить ваш чип — пока вы не переименуете переменную в коде. Тогда она уверенно выдаст вам неправильный ответ.

Индустрия проектирования чипов переживает увлечение большими языковыми моделями. Лаборатории и стартапы экспериментируют с автоматической генерацией SystemVerilog Assertions — формальных проверочных утверждений, которые отслеживают корректность поведения цифровой схемы на уровне регистровых передач (RTL). Идея соблазнительная: вместо того чтобы инженер-верификатор часами писал SVA-утверждения вручную, доверить это нейросети.

Но есть проблема, которую большинство исследований деликатно обходят стороной.

Что такое SystemVerilog Assertions и зачем они нужны

Для понимания новости нужно разобраться в базовых понятиях. RTL-код — это текстовое описание цифровой схемы: какие регистры чему присваивают значения, какие сигналы с чем сравнивают, какие условия запускают какие переходы. Это язык, на котором описывают процессоры, контроллеры памяти, сетевые чипы — в общем, всё цифровое железо.

SystemVerilog Assertions — это формальные утверждения поверх этого RTL-кода. По сути, это проверки вида «когда сигнал A равен единице, а сигнал B больше десяти, то на следующем такте на выходе Y должно быть значение X». Если на реальном кристалле или в симуляции это правило нарушается — значит, в схеме баг.

Написание SVA — одна из самых нудных и кропотливых задач в процессе верификации. Каждое утверждение должно точно отражать поведение схемы, учитывать все условия, не пропускать граничные случаи. Ошибка в SVA — ложное срабатывание или, того хуже, пропущенный баг. Отсюда интерес к автоматизации: пусть ИИ читает RTL-код и генерирует проверки.

В чём хитрость эксперимента

Исследователи из (судя по статье) группы вокруг автора Fnu Aditi поставили эксперимент, который выглядит тривиальным на первый взгляд, но обнажает серьёзную проблему. Они взяли набор RTL-программ из датасета VERT, отфильтровали его до 40 программ с 295 поведенческими блоками, и попросили две модели — Qwen2.5-Coder-7B и DeepSeek-Coder-V2-Lite — сгенерировать SVA-утверждения.

Затем они применили три трансформации к исходному RTL-коду, которые не меняют его суть:

• Перестановка операндов. Если написано a & b, заменить на b & a. Логика та же, синтаксис чуть другой.
• Переименование идентификаторов. Сигнал data_in становится sig_47. Смысл не изменился, но буквы поменялись.
• Добавление лишних скобок. (a + b) превращается в ((a + b)). Абсолютно эквивалентный код.

Идея проста: если нейросеть действительно «понимает» поведение схемы, а не просто паттерн-матчит текст, то результат должен быть одинаковым независимо от того, как записан тот же самый RTL.

Что получилось — и почему это важно

Результаты бьют по оптимизму. В диапазоне от 9,7% до 27% поведений, для которых модель изначально сгенерировала правильное SVA-утверждение, после косметической перезаписи RTL-кода превратились в неправильные. То есть модель умела это проверить — но хватило переименовать переменную, и всё посыпалось.

Причём картина неоднородна и местами парадоксальна. DeepSeek-Coder-V2-Lite при переименовании идентификаторов повысил общую точность с 53,9% до 63,7%. Звучит неплохо? Но при этом 19,5% его ранее правильных ответов стали неправильными. Модель научилась лучше решать какие-то случаи, но забыла другие. Итоговая метрика точности при этом растёт — и создаёт иллюзию прогресса.

Это классическая ловушка «точечной метрики». Если вы оцениваете нейросеть только на одном варианте входных данных, вы не знаете, стабилен ли результат. Вы, по сути, измеряете удачу.

Что именно ломается

Авторы вручную разобрали 30 случаев перехода «правильно → неправильно» и выделили четыре типа ошибок:

• Потеря предикатов путей. Модель «забывает» учесть условия, при которых выполняется определённая ветка логики. Вы проверяете поведение схемы для одного контекста — а SVA проверяет для всех подряд.
• Ошибки полярности ветвления. Модель путает «если истинно» и «если ложно». Условие инвертируется — и проверка ловит не тот баг, который нужно.
• Нарушение булевой структуры. Составные логические выражения разваливаются: вместо (A и B) или C модель выдаёт A и (B или C). Формально похоже, семантически — другое.
• Нарушение контракта выхода. SVA проверяет не то поведение, которое требуется — по сути, модель «забывает», что именно должно произойти на выходе схемы.

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

Почему это проблема для индустрии

Тренд на использование LLM в проектировании чипов набирает обороты. Несколько крупных игроков — Cadence, Synopsys, Nvidia — публично говорят об экспериментах с генерацией тестов и проверочных утверждений с помощью нейросетей. Стартапы вроде.debugLine работают над AI-ассистентами для RTL-дизайна.

Проблема в том, что верификация — это область, где ошибка стоит дорого. Пропущенный баг в процессоре может обернуться отзывом партии, потерей репутации и миллионами долларов. Intel в 2018 году столкнулась с дефектами Spectre и Meltdown, которые стоили компании, по оценкам аналитиков, до 3,5 миллиарда долларов — и это были баги, которые формальная верификация теоретически могла бы найти.

Доверять генерацию SVA нейросети, которая ломается от переименования переменной, — это как доверять калькулятору, который даёт другой ответ при перестановке слагаемых. Технически он считает, но доверять ему нельзя.

Что предлагают авторы

Исследователи вводят несколько метрик, которые до них никто не считал для этой задачи:

• Условная робастность — доля поведений, для которых SVA остаётся корректной при всех трансформациях.
• Частота потери инвариантности — как часто результат меняется хотя бы при одной трансформации.
• Any-flip rate — процент поведений, для которых хотя бы одна трансформация приводит к смене правильного ответа на неправильный.

Авторы используют кластерный бутстрэп с 10 000 выборками на уровне RTL-программ, что придаёт результатам статистическую устойчивость. Для исследования с двумя моделями и тремя трансформациями это аккуратная и честная работа.

Главный вывод статьи прямо сформулирован: точечная точность (point accuracy) — недостаточная метрика для оценки надёжности LLM при генерации утверждений. Нужны робастностные метрики, и нужна стандартизированная процедура оценки с семантически эквивалентными трансформациями входных данных.

Что это значит на практике

Результаты не означают, что LLM бесполезны для верификации. Они означают, что текущий подход к их оценке — проверили один раз, записали процент, опубликовали — слишком оптимистичен. Если индустрия действительно хочет интегрировать нейросети в pipeline верификации, нужны:

• метаморфическое тестирование на этапе оценки моделей;
• ансамбли моделей, которые сверяют результаты друг друга;
• обязательная ручная проверка для критических блоков схемы;
• понимание того, что даже модель с 90% точности на «чистом» тесте может давать существенно ниже на слегка переписанном коде.

Илон Маск может сколько угодно рассказывать про «полное самоуправление через год», но когда речь идёт о чипах в вашем телефоне, сервере или автомобиле, надёжность верификации — не место для импровизации.

До тех пор пока нейросети не научатся одинаково хорошо отвечать на один и тот же вопрос, заданный двумя разными способами, автоматизация написания SVA остаётся экспериментом, а не инструментом для продакшена.