Индуктивно-дедуктивный синтез: ИИ научился создавать формально верифицированные системы

Исследователи из UC Berkeley представили метод Inductive Deductive Synthesis (IDS), который позволяет AI-агентам генерировать код с формальными доказательствами корректности. Это первый подход, решающий проблему, с которой не справляются даже лучшие современные кодинг-агенты.

Современные AI-системы (Codex с GPT-5.4 и Claude Code с Opus 4.6) успешно справляются лишь с 2 из 7 спецификаций распределённого key-value хранилища. IDS достигает 7/7 в среднем за 6.8 часов и $106 на спецификацию — это примерно в 200 раз быстрее работы эксперта-человека и на 17% дешевле SOTA-агентов.

Метод основан на совместном и инкрементальном синтезе реализации и доказательства. IDS учится на неудачных попытках, систематически перебирая перспективные стратегии. Система также интегрирует обратную связь по производительности, что даёт реализации до 3 раз быстрее опубликованных верифицированных систем.

Особенно важно для разработки распределённых систем, где свойства вроде консистентности чтения/записи должны гарантироваться при любом возможном чередовании событий. Формальная верификация, которая раньше требовала месяцев работы экспертов, теперь становится доступной AI-агентам.

#AI #Verification #Research #IDS