Команда исследователей взяла все 134 публичных сабмита на лидерборде SWE-bench Verified и оценила каждое сравнение, которое эта таблица подразумевает. Получилось 8911 утверждений вида «система ранга 3 лучше системы ранга 4». Если читать таблицу так, как её читают все, сверху вниз, статистический бюджет разоряется на шестом утверждении. Ни одно из 8911 сравнений в порядке чтения не проходит проверку на валидность.

Это не нападки на SWE-bench, а иллюстрация системной проблемы: эмпирические сравнения стали стандартной формой доказательства в computer science, но почти никто не проверяет их статистическую корректность. Большинство сравнений вообще не оформлены как статистические тесты. Статья «Tacet: A Language and Type System for Automatic Statistical Validity Accounting» (arXiv:2608.27451) предлагает необычное решение: не новый статистический метод, а язык программирования с системой типов, который просто отказывается принимать утверждение, если анализ не может его себе позволить.

Почему бенчмарки врут: два неприятных исследования

Масштаб проблемы измеряли как минимум дважды, и оба раза результаты выглядят плохо. Dror и коллеги разметили 180 экспериментальных статей из ACL и TACL: статистическую значимость проверяли только 63 работы, название использованного теста указали 42, а корректный тест применили лишь 36. То есть пятая часть статей в ведущих NLP-venue делала выводы на статистически осмысленной основе.

Marie и соавторы прошли по 769 статьям о машинном переводе за 2010-2020 годы и назвали соответствующий раздел «The Disappearing Statistical Significance Testing». Доля работ с проверкой значимости ни разу не превысила 65%, а с 2016 года резко упала. Большинство авторов, по формулировке исследователей, делали выводы, не проверяя, не случайны ли их результаты.

Классические процедуры множественных сравнений (Bonferroni, Benjamini-Hochberg) могли бы контролировать накопленную ошибку. Но им нужны входные данные, которые невозможно восстановить из готового списка p-values: что именно анализ рассматривал и как устроены наблюдения. Именно здесь начинается Tacet.

Что такое Tacet

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

Первое свойство: что было прочитано при отборе выборки. Второе: как расположены наблюдения, попарно, кластерами или независимо. Об авторском замысле система не спрашивает вообще, и это принципиальный дизайн-ход.

Бит чистоты: почему cherry-picking ловится без чтения мыслей

Классическая дилемма выглядит так. Два клинических испытания сообщают одинаковый p-value по подгруппе. Первое отобрало пациентов старше 65 лет до того, как увидело исходы. Второе отобрало тех, кто ответил на лечение, то есть выбрало подгруппу уже по результатам. Список p-values их не различает, а статистическая цена этих находок совершенно разная.

В Tacet ядро исчисления T состоит из двух взаимно вложенных подъязыков. Подъязык оценки (estimation) бесплатен и отслеживает след (footprint): на каких данных построено каждое значение. Подъязык утверждений (claim) тарифицирован и несёт трансформер богатства. Единственный мост между ними: механизм, который назначает сравнению цену.

Выборка, отобранная по значению исхода («инстансы, которые система не решила», «пациенты, которые ответили»), устанавливает бит чистоты (purity bit) и навсегда записывается как прочитавшая всё, что она просмотрела. Такой выборке никогда не выдаётся односторонняя или подтверждающая цена. Системе не нужно гадать, собирался ли аналитик жульничать: сама конструкция программы уже всё сказала.

Отбор по ключу («инстансы из одного репозитория») записывает только след наблюдений, которые он оставил. Различие синтаксическое, и его видно до запуска на данных.

Парность вычисляется из схемы, а не угадывается

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

Tacet вычисляет парность и кластерность статически из объявленных функциональных зависимостей между ключевыми полями, до чтения любых данных. Механизм, который предполагает структуру, которой нет в схеме, получает отказ (DesignMismatch), а не цену. В кейс-стади это сработало буквально: двусторонний тест, направленный на парные кластеризованные данные, отклонён тип-системой, а не замечен внимательным ревьюером.

Богатство, ставки и пререгистрация как правило типов

Экономика языка унаследована от alpha-investing Фостера и Стайна в обобщении Ахарони и Россет. У анализа есть пул богатства α (обычно 0.05). Каждое утверждение делает ставку: по умолчанию фиксированную долю пула, в примерах статьи половину. Отвергнутая нулевая гипотеза возвращает ставку с доходом, неотвергнутая сжигает её. Когда пул пуст, новых утверждений нет.

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

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

Кейс 1: лидерборд SWE-bench Verified

Теперь к числам, ради которых статью стоит читать целиком. Авторы взяли 134 публичных сабмита SWE-bench Verified из официального репозитория экспериментов, каждый с множеством решённых инстансов, и оценили все сравнения, которые подразумевает полный порядок таблицы: 8911 утверждений по 468 инстансам, решённым хотя бы одним сабмитом. Логика безжалостно последовательна: читатель, принявший, что ранг 3 лучше ранга 4, а ранг 4 лучше ранга 5, уже принял транзитивно, что ранг 3 лучше ранга 5.

Результат зависит от порядка, в котором утверждения предъявляются бюджету, и это известное свойство alpha-investing. В порядке чтения таблицы бюджет поддерживает 0 из 8911 утверждений и банкротится на шестом. В порядке «сначала самые сильные эффекты» поддержаны 6545 из 8911. Та же таблица, те же p-values, диаметрально разные выводы. Порядок, который Tacet берёт из самой программы, оказывается таким же входом процедуры, как и сами данные.

Есть и структурное ограничение. Артефакт объявлен как патч одного сабмита для одного инстанса, с ключом в виде тройки (сабмит, репозиторий, инстанс). 12 репозиториев допускают лишь ограниченное число знаковых перестановок, поэтому самый острый двусторонний p-value, который эти данные вообще могут произвести, выше порога Bonferroni для 8911 утверждений. На репозиторном разрешении семейство неотвечаемо: никакой размер эффекта не спасёт сравнение, потому что потолок точности задан структурой данных. Если же считать каждый из 468 инстансов отдельной единицей, тот же анализ сдвигает p-values соседних рангов и поддерживает 5518 утверждений. Какой из двух запусков правильно прочитал дизайн, из p-values понять нельзя, а из ключей артефакта можно.

Даже узкое прочтение не спасает таблицу: из 133 утверждений о соседних рангах наивная процедура поддерживает 2, а бюджет ни одного.

Кейс 2: BIG-Bench Hard выживает

Второй кейс важен как контрпример: инструмент, который отклоняет всё подряд, измерял бы собственную суровость, а не качество анализов. Статья BIG-Bench Hard утверждает в абстракте, что промптинг без chain-of-thought существенно недооценивает возможности модели. Авторы опубликовали поэлементные выходы code-davinci-002 в обоих режимах, так что утверждения можно оценить: одно на задачу, 26 задач, 6261 пример.

Дизайн следует из ключей без посторонней помощи: оба условия прогоняются на одних примерах (сравнение парное), примеры вложены в задачи (пуловое утверждение: вопрос о задачах). Точный тест Макнемара на разноречивых примерах. Репликация сошлась с таблицей оригинала по всем 22 проверяемым точкам с точностью до одного десятичного знака.

Итог: 19 из 26 утверждений поддержаны бюджетом. Chain-of-thought выигрывает на 21 задаче, но две задачи (causal_judgement и ruin_names) показали забавный артефакт: двусторонний тест формально значим, а сырые счётчики указывают в пользу прямого промптинга. Тест отвергает при большой разноречивости в любую сторону и не проверяет, что знак эффекта совпадает с ярлыком утверждения. Ни одна из этих задач не входит в 19 поддержанных, так что заголовок статьи не пострадал, но именно здесь видно, где живут тонкие расхождения.

Самый показательный эффект дала кластеризация. Считать 6261 пример независимыми испытаниями и уважать структуру «примеры внутри задач»: разница в итоговом p-value составляет 187 порядков. Оба значения значимы, вывод статьи не под сомнением, но реальный объём свидетельства составляет 26 единиц, по одной на задачу, сколько бы примеров ни лежало внутри каждой. Эксперимент с 26 задачами физически не может произвести p-value, который даёт наивный подсчёт.

Реализация и модель угроз

Ядро Tacet занимает 1994 строки Python без единой внешней зависимости: 1566 строк у рантайм-монитора, 428 у статического фронтенда. Импорты ограничены math, itertools, dataclasses, ast и sys. Код и репликация кейсов открыты на GitHub (abuach/tacet-python). Монитор ценит p-value от любого теста: бюджету безразличен инструмент, а вот дизайн-предпосылке нет.

Модель угроз честно заявлена: защита от честного, но ошибающегося аналитика. Монитор живёт как библиотечный объект внутри того же Python-процесса, а богатство пула хранится в обычном mutable float, и ничто не мешает аналитику присвоить ему значение напрямую. Доверенная вычислительная база включает весь Tacet плюс интерпретатор Python. Соответствие между Lean-разработкой и поставляемым кодом проверено на 599 случайных программах, но не доказано.

Ограничения

Авторы не скрывают слабые места. Условная супер-униформность (H3) не верифицирована для обоих корпусов: семейства утверждений реконструированы ретроспективно, по уже опубликованным результатам, а не объявлены заранее, так что кейс-стади демонстрируют информативность цен, но не являются сертифицированными прогонами гарантии. Порядок утверждений должен быть фиксирован независимо от данных, и это предположение, а не проверяемое свойство. Отдельный сюрприз авторы измерили: отношение наивного счёта исходов к счёту артефактов на 17 анализах оказалось меньше, чем предполагала мотивация, то есть складирование наблюдений покупает меньше, чем кажется.

Часто задаваемые вопросы

Чем Tacet отличается от поправки Bonferroni?

Bonferroni работает офлайн: делит α на число тестов и требует готовый список p-values. Tacet работает до запуска анализа: вычисляет дизайн из схемы данных, отслеживает, что было прочитано при отборе, и отказывает утверждениям, которые нельзя корректно протестировать в принципе, а не только тем, что не прошли порог.

Значит ли результат по SWE-bench Verified, что лидерборд бесполезен?

Нет. Результат означает, что порядок чтения таблицы оказывается статистически неподдерживаемым семейством утверждений: бюджет банкротится на шестом сравнении. При порядке «сильнейшие эффекты первыми» 6545 из 8911 сравнений поддержаны. Вывод о том, какие пары систем действительно различимы, зависит от дисциплины предъявления, а не от самих данных.

Нужно ли переписывать анализ на новом языке?

Референс-реализация написана на чистом Python без зависимостей и живёт внутри обычного аналитического процесса. Аналитик объявляет артефакт, ключи и ожидаемые утверждения; монитор в рантайме следит за бюджетом, статический чекер сертифицирует программу заранее.

Итог

Tacet меняет точку приложения статистической дисциплины: с ревьюера, который должен угадать дизайн по таблице, на систему типов, которая читает дизайн из программы. Бит чистоты делает cherry-picking синтаксически видимым, статический вывод парности не даёт применить непарный тест к парным данным, а антимонотонный трансформер богатства превращает пререгистрацию в правило типизации. Два кейса показывают калибровку инструмента: лидерборд, где в порядке чтения не выживает ни одно из 8911 сравнений, и статья с сильными эффектами, которая сохраняет 19 из 26 утверждений. Если ваша работа опирается на лидерборды и таблицы результатов, стоит хотя бы один раз прогнать собственный анализ через вопрос, который задаёт Tacet: что именно вы прочитали, прежде чем это утверждать?