신뢰할 수 있는 소프트웨어 프로젝트 생성: 대화형 정리 증명기(ITP)를 이용한 사례 연구

자연어 요구사항으로부터 코드를 생성하는 것은 LLM(Large Language Model) 지원 소프트웨어 개발의 주요 경로가 되었습니다. LLM이 작은 프로그래밍 작업들을 성공적으로 완료할 수는 있지만, 미세한 오류가 컴파일과 테스트 과정에서 살아남을 수 있기 때문에 전체 복잡한 프로젝트를 생성하는 것은 여전히 신뢰하기 어렵습니다. 검증된 프로그래밍(Verified programming)은 생성된 구현체가 기계가 확인하는 명세(Specification)를 충족하도록 요구함으로써 이러한 위험을 줄일 수 있습니다. 기존의 탐색들은 주로 Dafny나 Frama-C와 같은 검증 지향적 언어 및 툴체인(Toolchain)을 대상으로 하지만, 이러한 시스템들로 프로젝트 규모의 검증된 코드를 직접 생성하는 것은 여전히 어렵습니다. 본 논문은 대화형 정리 증명기(Interactive Theorem Prover, ITP)가 대규모 소프트웨어 생성을 지원할 수 있는지 연구합니다. ITP는 순수 전역 함수(Pure total functions)는 다루지만 I/O와 같은 부작용(Effects)은 다루지 못하기 때문에, 우리의 에이전트는 부작용이 있는 코드(Effectful code)를 순수 로직(Pure logic)으로부터 분리합니다. 즉, 부작용은 대상 언어(Target language)에서 구현하고, 순수 로직은 ITP에서 증명한 뒤, 이를 최종 프로젝트에 통합하기 위해 추출(Extraction)합니다. 우리는 비특권 RISC-V RV32I 베이스의 47개 명령어 전체에 대한 CPU 인터프리터(Interpreter)를 완전히 자동화된 방식으로 개발함으로써 이 경로를 연구합니다. 요구사항이 제공된 후에는 합성(Synthesis), 증명 수정(Proof repair), 추출(Extraction) 또는 통합(Integration) 과정에 인간이 개입하지 않습니다. Rocq를 백엔드(Backend)로 사용하여, 에이전트는 30분 이내에 프로젝트를 완료하며, 1,859줄의 검증된 Rocq 코드를 생성하고 2,848줄의 C++ 코드를 추출합니다. 결과물인 인터프리터는 47개 명령어를 다루는 265개의 LLM 생성 테스트를 모두 통과하였으며, 12시간 동안의 AFL++ 퍼징(Fuzzing) 동안 크래시(Crash)와 행(Hang)이 전혀 발생하지 않았습니다. 동일한 구성에서 Dafny 기반의 백엔드는 검증을 완료하는 데 실패했습니다. 우리의 관찰 결과는 Rocq가 증명 시도가 실패했을 때 구체적인 증명 상태(Proof state)를 노출하여, 에이전트에게 수정을 위한 실행 가능한 피드백을 제공한다는 점입니다. 이러한 결과는 ITP 기반의 검증된 프로그래밍이 LLM이 생성한 소프트웨어 프로젝트를 위한 실행 가능한 경로라는 실증적 증거를 제공합니다.