귀납적 연역적 합성 (Inductive Deductive Synthesis): AI가 형식적으로 검증된 시스템을 생성할 수 있도록 지원하기

AI 에이전트(AI agents)는 코드를 생성, 테스트 및 개선하는 작업에서 점점 더 뛰어난 능력을 보여주고 있습니다. 하지만 테스트만으로는 제공할 수 없는, 전체 커버리지에 대한 형식적 보장 (formal guarantees)이 필요한 작업에서는 한계를 보입니다. 분산 시스템 (Distributed systems)이 대표적인 예입니다. 읽기(reads)와 쓰기(writes) 사이의 일관성(consistency)과 같은 속성은 모든 가능한 이벤트의 교차 실행 (interleaving) 상황에서도 유지되어야 합니다. 기계화된 형식 검증 (Mechanized formal verification)은 이러한 정확성을 보장할 수 있지만, 일반적으로 전문가의 노력이 수개월에서 수년이 소요됩니다. 증거로서, 심지어 최첨단 (SOTA) 코딩 에이전트들(GPT-5.4를 탑재한 Codex 및 Opus 4.6을 탑재한 Claude Code)조차 7개의 분산 키-값 저장소 (distributed key-value-store) 사양 중 2개만을 성공시켰습니다. 본 논문에서는 이 격차를 해결하기 위한 최초의 효과적인 접근 방식인 귀납적 연역적 합성 (Inductive Deductive Synthesis, IDS)을 제시합니다. IDS는 구현 (implementation)과 증명 (proof)을 공동으로 그리고 점진적으로 합성하며, 실패한 시도로부터 학습하여 유망한 전략을 체계적으로 시도합니다. 에이전트 기반 LLM 시스템으로 구축된 IDS는 사양당 평균 약 6.8시간과 106달러의 비용으로 7개 중 7개를 모두 성공시켰으며, 이는 전문가의 노력보다 약 200배 빠르고 SOTA 에이전트보다 17% 저렴합니다. 또한 IDS는 성능 피드백 (performance feedback)을 동일한 루프에 통합하여, 이미 발표된 검증된 시스템보다 최대 3배 더 빠른 구현을 만들어냅니다.