🛡 Провёл ряд экспериментов с DeepSeek, Qwen, Grok и Claude, которые показывают, что модели имеют целевое обучение на Evidence-Based Testing (EBT). Это стандарты тестирования уровня life-critical систем. Заняться этой темой меня подвинул опыт моей супруги, которая программировала авионику для наших самолётов в Транзас и для Boeing, пока работала в Motorola. В стандартах тестирования авионики как DO-178C по факту Test-Driven Development (TDD) предан анафеме и как аксиома считается, что «зелёные тесты ничего вообще не значат о надёжности». Применяется «доказательное тестирование», где код должен доказывать, что утверждение из спецификации выполнено.

Примерно такой же принцип во всех медицинских устройствах — стандарт IEC 62304 (FDA). Фактически TDD запрещён как ненадёжный, требуется «доказательное тестирование». Аудитору вообще запрещено смотреть на «зелёные тесты» на манер TDD, которые могут быть фиктивными, а смотрит на сквозную трассировку требований через все артефакты разработки и тестирования: «requirement → design → code → test result».

Похожий подход в системах безопасности высокого уровня как Common Criteria: Evaluation Assurance Levels (EAL). EAL7 требует формальной верификации, EAL4 — методического тестирования с независимой проверкой.

Методы «доказательного тестирования» идут к формальной логике, открытой математиками в 1960–1980-е годы: Hoare Logic, Z-notation, TLA+. Идея «спецификация → доказательство» родилась здесь.

Основная проблема таких формальных методов: они были слишком тяжелы для индустрии, а главное очень дорогие не только в части трудоёмкости реализации людьми, но требовался не просто программист, а фактически разработчик с пониманием формальной логики почти как математик. Такое могли себе позволить тогда разработчики критических систем в авиации, медицине и безопасности. Однако, сделав тесты DeepSeek, Qwen, Grok и Claude, я обнаружил, что они не только знают оные стандарты, но что важнее — их явно прямо тренировали на применение их, что весьма понятно. Одно дело заменять ботом разработчика какого-то «онлайн-магазина», а другое дело разработчика life-critical команды, который в 10 раз дороже.

Фактически применение методики заключается в сквозной трассировке требований через все артефакты разработки от первых записок RFC до спеков, кода, логов и тестов. Потом на базе них ИИ может собрать систему «утверждений и доказательств» в математической логике. Причём это работает даже на примитивном коде, как тот же «онлайн-магазин», и не требует очень большого дополнительного расхода токенов. Скорее тут проблема в том, что ИИ как раз понятна реализация EBT через формальную логику, а человеку, который впервые такое видит, не так просто понять даже принципы, как это вообще работает, но работает. Не работало бы — вы бы давно умерли: самолёты бы упали, и вам бы сжёг мозг МРТ, если плотность багов там была бы как в обычном ПО на традиционных тестах.

Думаю, я включу поддержку EBT в новый вариант GRACE, т.к. в реальности это сложные для кожаных, но не для ИИ методы. Коллегам я бы хотел отметить, что есть такое интересное направление контроля качества ПО: с агентами и ИИ стало доступным технологии разработки софта на уровне качества Boeing даже фрилансеру. По ссылке одна из методичек по DO-178C, но в целом ваш ИИ в этом разбирается сам.

https://www.rapitasystems.com/downloads/efficient-verification-through-do-178c-life-cycle