AI 에이전트가 코드를 작성하고 SMT(Satisfiability Modulo Theories) 솔버가 이를 검증하는 새로운 프로그래밍 언어 LLMLL(Large Language Model Logical Language)이 공개되어 주목받고 있습니다. LLMLL은 AI 에이전트가 형식 계약(formal contracts)에 따라 코드를 작성하고, 컴파일러가 각 함수 본문이 계약을 충족하는지 Z3와 같은 SMT 솔버를 이용해 증명하는 방식으로 작동합니다. 이는 AI가 생성한 코드의 정확성과 신뢰성을 높이는 데 중점을 둔 실험적인 접근 방식입니다.
LLMLL의 핵심은 AI 에이전트가 '타입이 지정된 빈 공간(typed holes)'을 채우고, 이 채워진 코드가 미리 정의된 계약(precondition 및 postcondition)을 만족하는지 SMT 솔버가 검증하는 파이프라인입니다. 만약 AI가 작성한 코드가 계약을 위반하면, 설령 문법적으로 올바르더라도 컴파일러는 이를 거부합니다. 예를 들어, 자금 이체 함수에서 총액 보존 계약을 위반하는 코드는 SMT 솔버에 의해 즉시 거부됩니다. 이는 AI의 '환각(hallucination)' 문제를 단순한 실패 모드가 아닌, 스펙에 맞는 코드를 탐색하는 전략으로 활용할 수 있게 합니다. 또한, LLMLL은 코드의 구조(JSON-AST)를 편집하여 텍스트 병합 충돌을 방지하고, 약한 계약을 자동으로 감지하는 기능도 제공합니다.
이러한 접근 방식은 AI가 생성하는 코드의 신뢰성 문제에 대한 중요한 해결책을 제시합니다. 기존에도 Dafny, Liquid Haskell, F*와 같은 도구들이 코드의 형식 검증을 수행했지만, LLMLL은 AI 에이전트가 코드를 작성하는 '루프'를 검증 과정에 통합했다는 점에서 차별점을 가집니다. 실험 결과, 최신 AI 모델들이 30번의 시도 중 30번 모두 검증된 코드를 성공적으로 작성했으며, 잘못된 코드를 생성한 경우는 54번 중 0번으로 나타나 AI가 작성한 코드의 높은 신뢰성을 입증했습니다. 이는 AI가 단순한 코드 생성 도구를 넘어, 엄격한 요구사항을 만족하는 고품질 소프트웨어 개발의 주체로 발전할 잠재력을 보여줍니다.