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

요약

LLM을 활용하여 대화형 정리 증명기(ITP) 기반의 신뢰할 수 있는 소프트웨어 프로젝트를 생성하는 연구를 소개합니다. Rocq를 백엔드로 사용하여 부작용이 있는 코드와 순수 로직을 분리함으로써, 인간의 개입 없이 검증된 CPU 인터프리터를 성공적으로 개발했습니다.

핵심 포인트

• ITP를 활용해 LLM 생성 코드의 신뢰성 문제 해결
• 순수 로직과 부작용(Effectful code)의 분리 및 추출 방식 적용
• Rocq 백엔드를 통해 30분 내에 검증된 CPU 인터프리터 생성
• Dafny 대비 Rocq의 구체적인 증명 상태 피드백이 성공의 핵심
• AFL++ 퍼징 테스트를 통해 높은 안정성 입증