Блог
[измерено на строгом сете t27 из 391 айтемов: 0/150 плоской генерации против 3/150 маскированной на тех же 30 труднейших; 65% первых ошибок компиляции — необъявленные идентификаторы; строгая петля закрыта на 30 раундах / 8083 сэмплах = 4/391 pass, 283/391 compile; три ограничения декодера, ноль параметров; чекпоинт бенчмарка = t27-файнтюн tern_tc, пакет шипит базовый] tern_tc, тернарная модель на 9M под блочную память XC7A200T, не может выучить имена областей видимости — и вместо масштабирования мы ограничили её декодер: маска области видимости на каждом шаге, разнообразие правилами маски, а не температурой (15/30 против 3/30 union compile), и запрет n-граммов повторов после того, как 1517/2177 нескомпилированных кандидатов оказались каскадами повторов. Результат — не решатель: 1.0% строгого сета проходит тесты. Это модель-черновик для верификатора: 72% сета получает компилируемое тело, tri tc-draft возвращает первое проверенное тестами или честный отказ.
tern_tc — тернарная модель на 9M параметров (веса из {-1, 0, +1}), шесть слоёв, ширина 320, словарь 8K, рассчитанная под блочную память XC7A200T. Её задача — заполнять тела функций в спеках t27, где ответ судят собственные тесты спеки. На строгой половине бенчмарка — 391 функция, тесты которой ловят обоих константных мутантов, — плоский сэмплинг дал 0 прохождений из 150 на 30 самых трудных айтемах, а 65% первых ошибок компиляции были «use of undeclared identifier». Модель не знает имён — и на 9M параметров не может. Этот пост о том, что мы сделали вместо масштабирования: ограничили декодер. Провенанс, чтобы ничего не пряталось: все числа ниже — один чекпоинт, эта же архитектура после доменного файнтюна: базовая модель, продолженная ~3 эпохами (22M токенов) по самому корпусу t27-спек. Публичный пакет шипит базовый чекпоинт, и его карточка не делает заявлений о качестве; файнтюннутый чекпоинт бенчмарка с тех пор опубликован отдельно — playra/tern-tc-9m-t27, с той же честной карточкой.
C-движок говорит по протоколу step-io: печатает один токен и принимает одну строку маски («.» свободно, «+» список разрешённых, «-» список запрещённых). Внешний маскер — тот же код, что знает области видимости спеки, — вычисляет, какие идентификаторы грамматичны на этой позиции: сигнатура самой функции, соседние функции, константы модуля до неё и имена, которые тело уже объявило. Внутри строки и комментария, а также после точки маска снята. В середине идентификатора выживают только продолжения, ведущие к разрешённому имени. «Сначала объяви — потом используй» перестаёт быть надеждой и становится свойством декодирования. Запрет — это -1e30 в логитах, до argmax и до top-p, поэтому жадный режим и сэмплинг подчиняются одинаково.
На тех же 30 айтемах, где плоская генерация дала 0/150, маскированная дала 3 прохождения из 150 сэмплов — 2.0%, первый ненулевой результат модели на этом бенчмарке, — а петля «сгенерировать-проверить-повторить» довела это до 3 из 30 решённых айтемов на 149 сэмплах, каждое подтверждено тестами самой спеки.
Петле нужны разные сэмплы в каждом раунде. Обычный рычаг — температура. Мы измерили оба рычага по одним и тем же историческим артефактам: три температуры (0.7/0.8/1.1) при одном правиле маски дают union-покрытие 3 из 30 айтемов по компиляции; три правила маски при одной температуре — 15 из 30. Все прохождения в этом наборе достались температуре 0.7. Температура перетасовывает те же ошибки; смена правила меняет само множество допустимого.
Когда полная строгая петля застряла на 2 прохождениях за 20 раундов, разбор отказов объяснил, почему кандидаты не компилировались: 1517 из 2177 кандидатов в blocked_codegen были каскадами повторов — r.unshift(r.unshift(… снова и снова. Модель на температуре >= 0.7 заходит в цикл и не выходит. Лекарство — та же дисциплина, что у маски, наведённая на вторую моду отказа: запрет любого n-грамма, который продолжение уже содержит (-1e30 до сэмплинга, --no-repeat 4). Оба поздних прохождения финального прогона пришли уже с этим запретом. Маскирование областей видимости, разнообразие правил и запрет повторов — три ограничения на один декодер, и ни одно не стоит ни одного параметра.
Полная петля закрылась на 30 раундах, 8083 сэмплах, около 21 на айтем. Четыре прохождения из 391 (1.0%) — раунды 3, 7, 26 и 27 — и каждое досталось другому arm'у (s0.7, w0.7, w0.8, m0.7): тезис о разнообразии правил, ставший фактом. Второе число важнее: 283 из 391 айтемов (72%) дали хотя бы одно компилируемое тело. Маскированная модель на 9M говорит на языке почти трёх четвертей строгого сета; стена — семантика, не синтаксис. Её роль — модель-черновик для верификатора, упакованная в одну команду: tri tc-draft принимает спеку и сигнатуру функции, платит префилл один раз за N маскированных сэмплов, судит каждый через t27c, печатает первое тело, прошедшее собственные тесты спеки, и выходит с кодом 1 и таблицей статусов, когда такого нет. Ни одно неверифицированное тело не выдаётся за ответ.
Для масштаба: модель на 100M с плавающими весами на том же бенчмарке даёт 7.4% pass@10, её тернарная пара — 2.3% (обе — после такого же t27-файнтюна, то есть сравнение честное), и разрыв вырос с 1.5x до 3.2x при учетверении данных. Тернарность дорога для кода; этот результат тоже опубликован, и этот пост — не спор с ним, а честный отчёт о том, для чего на самом деле нужна тернарная модель-board-размера.
Публикуются веса базового чекпоинта: пакет, карточка модели, графики бенчмарка и контракт CI генерируются из t27-спек, несущих собственные тесты, а публичный verify-workflow перепроверяет хеши пакета, пересобирает C-движок, воспроизводит бордовую квитанцию генерации (1 3 204 276 405 659 85 1516) и держит битовый паритет с PyTorch — зелёный против байтов на хабе сегодня. Числа бенчмарка в этом посте — с файнтюннутого чекпоинта, описанного выше, а не с базового из пакета. Файнтюн опубликован: https://huggingface.co/playra/tern-tc-9m-t27 — тот же C-движок, тот же токенайзер, одна команда sh scripts/verify.sh проверяет хеши и воспроизводит кросс-энжинную квитанцию (C == PyTorch CPU == MPS); карточка несёт те же числа, что этот пост, с протоколом каждого.
Поработаем вместе
Я аудирую RTL и строю независимые побитово точные модели, затем провожу результат через синтез и, когда это полезно, проверяю на плате Artix-7. Первый модуль проверки — бесплатно.