n-version-programming

6 posts

Differential testing работает без формального доказательства, но common-mode failures — вот подвох

Differential testing позволяет находить баги, не зная правильного ответа. Проблема в том, что коррелированные ошибки выглядят как согласие. Вот как обнаружить слепые зоны.

Можно доверять differential testing без формального доказательства, но только если точно понимать, где оно даёт сбой. Эта слабость называется common-mode…

Тестирование не докажет, что две функции эквивалентны. Вот что докажет.

N-версионное программирование предполагает, что ваши реализации согласованы. Мы разбираем, почему тестов недостаточно, как SMT-солверы могут реально доказать эквивалентность и где провести границу между «достаточно хорошо» и формально верифицировано.

Вы построили n-версионную систему. Три независимые реализации одной и той же критической функции, voter, который выбирает результат большинства, и приятное…

Что делать, если мои варианты LLM не согласны? Какой из них прав?

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

Вы отправляете промпт в GPT-4o. Он возвращает JSON с уверенностью 0.97. Вы отправляете тот же промпт в Claude 3.5 Sonnet. Он возвращает другой JSON, тоже с…

Пять реализаций и нет большинства: как на самом деле выбрать лучшую

N-version programming звучит просто: запустить несколько реализаций и выбрать лучший ответ. На практике «лучший» определить гораздо сложнее, чем «самый распространённый».

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

Тот же LLM может написать пять версий вашей функции. Вот как сделать их по-настоящему разными.

N-version programming с LLM не требует нескольких моделей. Можно извлечь разнообразные, корректные реализации из одной модели, варьируя промпты, персоны и ограничения на рассуждения.

N-version programming предполагает, что разнообразие приходит от разных авторов. С LLM это означает разные модели, разных провайдеров, возможно, разные…

NASA запускала 27 копий одной программы. Баги голосовали единым блоком.

N-version programming обещало, что независимые команды допускают независимые ошибки. Эксперимент Knight и Leveson в 1986 году доказал обратное, и NASA тихо отказалась от этой идеи.

В начале 1980-х NASA столкнулась с вопросом, который до сих пор преследует критически важную инженерию: как смириться с багами, которые вы ещё не нашли? Их…