TrustedCode: 자동 프로그램 검증을 통한 신뢰 코드 개발을 위한 대규모 언어 모델 평가

요약

본 논문은 AI가 생성한 파이썬 코드의 신뢰성 확보를 위해 자동화된 형식 검증 프레임워크인 TrustedCode를 제시합니다. 이 도구는 LLMs를 활용하여 타입 체크, WhyML 변환, 그리고 자동 정리 증명기를 통해 코드를 체계적으로 검증하는 워크플로우입니다. LangGraph 기반 CoT 프롬프팅을 통합하여 명세 생성 및 프로그램 증명 과정의 한계를 극복했습니다.

핵심 포인트

• AI 코드 증가에 따른 신뢰성 확보를 위해 형식 검증이 필수적임.
• TrustedCode는 파이썬 코드를 위한 자동화된 형식 검증 프레임워크를 제공함.
• LLM과 Why3, 자동 정리 증명기를 결합하여 체계적인 검증을 수행함.
• 오류 원인 분석 결과, 도메인 지식 격차가 가장 큰 문제로 확인됨.