IDS(Inductive Deductive Synthesis)는 분산 시스템 구현과 형식 증명을 공동으로 점진적으로 합성하고 실패 시도에서 학습해 유망한 전략을 체계적으로 탐색하는 에이전트 LLM 시스템이다. SOTA 코딩 에이전트(GPT-5.4 기반 Codex 2/7, Opus 4.6 기반 Claude Code 2/7)가 실패한 분산 키-값 저장소 7개 명세를 모두 해결하며, 전문가 노력 대비 약 200배 빠른 평균 6.8시간, 명세당 $106에 달성했다. 또한 SOTA 에이전트보다 17% 저렴하며, 성능 피드백을 동일 루프에 통합해 공개 검증 시스템보다 최대 3배 빠른 구현을 생성했다. 형식적 보장이 필요한 분산 시스템 검증에서 AI의 실용적 가능성을 처음으로 입증한 연구다.
- •분산 KV 저장소 명세 7/7 해결 — GPT-5.4 Codex(2/7), Claude Code Opus 4.6(2/7) 대비 월등
- •전문가 노력 대비 약 200배 빠른 평균 6.8시간, 명세당 $106 / SOTA 에이전트 대비 17% 저렴
- •구현과 증명 공동 점진적 합성 + 실패 학습 기반 유망 전략 체계적 탐색
- •성능 피드백 동일 루프 통합으로 공개 검증 시스템 대비 최대 3배 빠른 구현 생성
0단 자동
AI가 규칙대로 쓰고 그대로 게시했습니다. 사람이 따로 보지 않았습니다.
- 규칙 판
- 규칙 판 도입 이전 기사입니다.
- 남기는 것
- 규칙 판 · 모델 · 시각
- 판 기록
- 아직 없습니다.
Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems
- 1.IDS는 구현과 증명을 공동·점진적으로 합성하고 실패 사례에서 전략을 학습하는 에이전트 LLM 시스템
- 2.GPT-5.4·Opus 4.6 기반 SOTA 에이전트는 분산 KV 명세 2/7 해결, IDS는 7/7 달성(평균 $106/명세)
- 3.전문가 대비 약 200배 빠르고 SOTA 에이전트 대비 17% 저렴, 성능 피드백 반영으로 검증된 구현이 기존 시스템 대비 최대 3배
왜 중요한가?
기존 SOTA 코딩 에이전트가 형식 검증 요구 분산 시스템에서 실패하던 한계를 IDS가 처음으로 해결, 안전성 보장이 필수인 소프트웨어 개발 자동화의 실용 가능성을 직접 입증했다.
언급 프로젝트
본문 미리보기
arXiv:2605.23109v1 Announce Type: new Abstract: 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 ef
전체 내용이 궁금하다면?
원문을 직접 읽어보세요
이 글이 만들어진 과정
- 13:12AI 초안
