Как я ранее и предсказывал, вендоры вроде Anthropic начали двигаться от традиционного тестирования в духе TDD в сторону формального доказательства отсутствия в коде ошибок определенного рода

Anthropic показал, что Claude с помощью методов формальной верификации доказывал свойства безопасности и корректности для скомпилированных программ (на уровне ассемблера RISC-V или x86). Например, Claude доказывал, что программы из 123 open-source библиотек никогда не завершатся аварийно (без memory-safety errors и падений ассертов) для любого входа размером менее 64 МБ при определённых допущениях о среде исполнения. В основном использовался Verus для Rust.

Однако важно понимать, что ИИ потенциально намного мощнее в формальной верификации, т.к. кроме строгой формальной дедуктивной логики ему доступна и семантическая вероятностная. Поэтому важно уже учитывать этот тренд, и он прямо связан с важным аспектом философии контрактного программирования — инвариантами.

Если вы в коде объявите формально инварианты при его генерации, то ИИ сможет сделать рассуждение как доказательство, что этот код никогда не нарушает эти инварианты. Чем более формальные инварианты, тем ближе рассуждение LLM будет к формальному доказательству, т.е. такой код не тестируется традиционным способом, а переходит в плоскость «доказательного программирования».

Я до статьи Anthropic уже сильно экспериментировал с этими подходами, как можно было заметить по моим постам, но я думал, что они сделают LLM, способную к ведению такого анализа, через несколько месяцев. Пора уже нам всем учитывать, что во время ИИ-сингулярности самое время пристегнуться от скорости прогресса.

Всё будет развиваться очень быстро. Ещё вчера очень узкие методики профессионалов могут стать быстро широко используемыми.

https://www.anthropic.com/research/formal-verification

Телеграм: t.me/ainewsline

Источник: t.me

Комментарии: