Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems

AI agents increasingly excel at generating, testing, and refining code. However, they fall short on tasks requiring formal guarantees of full coverage that testing alone cannot provide. Distributed systems are a prime example: properties such as consistency between reads and writes must hold under every possible interleaving of events. Mechanized formal verification can guarantee such correctness, but typically demands months to years of expert effort. As evidence, even SOTA coding agents (Codex with GPT-5.4 and Claude Code with Opus 4.6) succeed on only 2/7 distributed key-value-store specifications. In this paper, we present the first effective approach to addressing this gap, Inductive Deductive Synthesis (IDS), which jointly and incrementally synthesizes implementation and proof, and learns from failed attempts to systematically try promising strategies. Built as an agentic LLM system, IDS achieves 7/7 in about 6.8 hours and $106 per spec on average, roughly 200x faster than expert effort and 17% cheaper than SOTA agents. IDS further incorporates performance feedback into the same loop, yielding implementations up to 3x faster than published verified systems.

📋 한 줄 요약

**[Inductive Deductive Synthesis]** IDS가 implementation과 proof를 점진 공동 합성·실패에서 학습 — 분산 KV-store 7/7 spec을 6.8시간·$106에 검증(전문가 200×·SOTA agent보다 17% 저렴·구현 최대 3× 빠름).

🎯 핵심 기여도

AI 에이전트가 코드 생성·테스트·개선에 능해지고 있지만 full coverage의 formal guarantee가 필요한 태스크(분산 시스템의 read–write consistency 등)는 testing으로 부족함을 지적 — 정형 검증은 보장하지만 보통 전문가 수개월~수년 소요.
SOTA coding agent(Codex+GPT-5.4, Claude Code+Opus 4.6)조차 분산 KV-store spec 7개 중 2개만 해결하는 격차 실증.
이 격차를 메우는 첫 효과적 방법으로 Inductive Deductive Synthesis(IDS) 제안 — implementation과 proof를 공동·점진적으로 합성하고 실패한 시도로부터 학습해 promising strategy를 systematically 시도하는 agentic LLM 시스템.
IDS가 평균 spec당 약 6.8시간·$106으로 7/7 spec 해결 — 전문가 대비 약 200× 빠르고 SOTA agent 대비 17% 저렴. 동일 루프에 performance feedback도 통합해 출판된 verified system 대비 최대 3× 빠른 구현 산출.

💡 핵심 아이디어

Formal verification은 정확성 guarantee가 필요한 분산 시스템에서 LLM agent의 핵심 차별 영역이며, implementation과 proof를 분리해 합성하는 대신 inductive(예제) + deductive(증명) 합성을 jointly·incrementally 수행하고 실패 경험을 학습해야 실용적 비용·시간으로 검증 시스템을 구축할 수 있다.

🔬 기술적 접근법

**방법론**: IDS — joint inductive (implementation) + deductive (proof) synthesis with failure-driven learning.
**핵심 기법**: (1) Implementation과 proof를 공동·incremental 합성, (2) 실패 시도에서 systematic하게 promising strategy 학습, (3) Agentic LLM 시스템으로 multi-stage 오케스트레이션, (4) Performance feedback을 동일 루프에 통합해 구현 속도도 함께 최적화, (5) 분산 KV-store 7개 spec 위주 평가.

📊 주요 결과

분산 KV-store: SOTA agent(Codex+GPT-5.4·Claude Code+Opus 4.6)는 2/7, IDS는 7/7.
평균 spec당 약 6.8시간·$106 — 전문가 대비 약 200× 빠름, SOTA agent 대비 17% 저렴.
Performance feedback 통합으로 출판된 verified system 대비 최대 3× 빠른 구현.

💭 의의 및 한계

**의의**: LLM 에이전트가 정형 검증 영역에서 실용 비용으로 동작함을 처음 입증, formal correctness가 필요한 critical infrastructure에 AI 도입 가능성 확대, 비용·시간 모두 break-through. **한계**: 분산 KV-store 7개 spec 중심 — 다른 정형 도메인 일반화 검증 필요, $106·6.8시간이 여전히 작지 않음, agent 시스템 복잡성 증가.

🚀 실용적 활용

분산 시스템 정확성 보장 자동화.
Verified critical infrastructure 구축.
AI 에이전트 기반 정형 SW 엔지니어링.