사용자의 의도를 컴퓨터가 자동으로 검사할 수 있는 엄밀한 명세로 자동 변환
AI 코딩 시대의 핵심 문제인 “정말 의도대로 동작하는가?”를 자동 검증하는 돌파구 제시
복잡한 명세를 실시간으로 쪼개며 생성하고, 중간중간 오류를 검사해 신뢰할 수 있는 명세 생성 기술 고안

KAIST 전산학부 허기홍 교수팀이 AI가 만든 프로그램의 올바름을 보장하는 핵심 기술을 개발했다. 해당 기술을 담은 논문 “Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles”는 프로그래밍 언어 분야 최우수 학회인 PLDI 2026에 채택되어 올 6월 발표될 예정이다.

최근 자연어 지시만으로 AI가 코드를 작성해 주는 이른바 “바이브 코딩”이 빠르게 확산되고 있다. 개발자는 “이런 기능을 만들어줘”라고 설명하기만 하면 AI로부터 곧바로 코드를 얻을 수 있지만, 문제는 그 코드가 실제로 사용자의 의도를 정확히 반영했는지 확인하기 어렵다는 데 있다. AI가 생성한 코드를 사람이 일일이 검토하는 데에는 한계가 있으며, 최근에는 그 검토 과정마저 AI에 의존하는 경우가 늘어나면서 코드의 신뢰성을 어떻게 보장할 것인지가 중요한 과제로 떠오르고 있다.

연구팀이 개발한 Expecto는 인간의 요구사항을 컴퓨터가 이해할 수 있는 엄밀한 명세 (formal specification)으로 자동 변환함으로써, AI가 생성한 코드가 사용자의 의도를 실제로 만족하는지 검증할 수 있게 하는 기술이다. 엄밀한 명세는 논리식으로 작성되어 모호함이 없고 컴퓨터가 이해할 수 있지만, 사람이 직접 작성하기는 매우 어렵다. Expecto는 이러한 엄밀 명세 작성을 자동화하고, 작성된 엄밀 명세는 프로그램 검증 기술을 이용하여 자동 생성된 코드의 올바름을 확인하는 데 활용된다.

연구팀은 언어모델과 논리 검증을 결합한, 논리-직관 AI (neurosymbolic AI) 기술을 이용하여 Expecto 를 설계했다. 복잡한 요구사항을 한 번에 처리하지 않고, 여러 논리 계층으로 나누어 각각 엄밀한 명세로 변환하는 방식이다. 기존 기술이 언어모델에게 모든 것을 맡기고, 긴 요구사항 전체를 한 번에 엄밀한 명세로 작성하도록 지시하는 것과 대조적이다. 이는 복잡한 문제의 풀이 과정을 한 번에 모두 쓰게 하는 것과 같아 중간에 작은 실수가 발생하기 쉽기 때문이다.
또한 Expecto는 명세가 올바르게 작성되고 있는지 프로그래밍언어 분야의 기술을 활용하여 지속적으로 점검한다. 아직 완성되지 않은 부분이 있더라도 현재까지 만들어진 규칙이 문법적으로 올바른지, 타입이 맞는지, 논리적 모순은 없는지를 확인한다. 이를 통해 명세가 잘못된 방향으로 생성되고 있을 때 오류를 조기에 발견하고 즉시 수정할 수 있다.

Expecto는 AI 코딩 도구가 코드를 생성하는 단계를 넘어, 생성된 코드의 올바름까지 자동으로 검증하는 “검증형 AI”로 나아가기 위한 기반 기술이다. 연구팀의 이동재씨(전산학부 박사과정)는 “앞으로의 개발 환경에서는 단순히 코드를 빠르게 생성하는 것만으로는 충분하지 않다”며, “AI가 만든 코드가 사용자의 의도를 정확히 만족하는지 자동으로 확인할 수 있어야 한다”고 설명했다. 특히 금융, 보안, 의료, 인프라 소프트웨어처럼 작은 오류도 큰 피해로 이어질 수 있는 분야에서 AI 기반 SW 개발의 신뢰성을 높이는 데 중요한 역할을 할 것으로 기대했다. 허기홍 교수는 “바람직한 AI 기술은 증명의 부담까지 AI가 지는 형태여야 한다”며, “생성한 코드의 올바름까지 스스로 책임지는 AI 에이전트 기술을 실현하겠다”는 포부를 밝혔다.