Новый метод IDS: ИИ научился создавать формально верифицированные системы за 7 часов вместо месяцев
Формальная верификация программного обеспечения традиционно требует месяцев или даже лет ручного труда экспертов. Однако новый подход, названный Inductive Deductive Synthesis (IDS), кардинально ускоряет этот процесс. Разработчики представили метод, который позволяет ИИ-агентам совместно и пошагово синтезировать реализацию и математическое доказательство её корректности.
Проблема особенно остра для распределённых систем, где свойства вроде согласованности чтения и записи должны выполняться при любом возможном чередовании событий. Даже современные кодирующие агенты, такие как Codex на базе GPT-5.4 и Claude Code с Opus 4.6, справляются лишь с 2 из 7 спецификаций распределённого хранилища ключ-значение. IDS же достигла показателя 7 из 7.
Как сообщается в препринте на arXiv, IDS построена как агентная LLM-система. Она обучается на неудачных попытках и систематически перебирает перспективные стратегии. В среднем на одну спецификацию уходит около 6,8 часов и $106 — это примерно в 200 раз быстрее работы эксперта-человека и на 17% дешевле, чем использование существующих SOTA-агентов.
Кроме того, IDS интегрирует обратную связь по производительности в тот же цикл, что позволяет получать реализации, работающие до трёх раз быстрее опубликованных верифицированных систем. Такой подход открывает путь к автоматическому созданию надёжного кода для критически важных систем — от финансовых протоколов до облачных инфраструктур.
По мнению авторов, IDS представляет собой первый эффективный метод, устраняющий разрыв между возможностями ИИ по генерации кода и требованиями формальной верификации. Дальнейшие исследования могут быть направлены на масштабирование метода для более сложных систем и снижение затрат.
