본 논문은 생성형 인공지능(Generative AI)과 상호작용적 정리 증명(Interactive Theorem Proving)을 결합하여 Rocq 증명 생성을 위한 다양한 접근 방식을 평가하고 개선 방향을 제시합니다. 특히, Rocq 증명 생성을 위한 전제 선택의 중요성을 강조하고, 자기 주의 매립 모델을 활용한 검색 기반의 새로운 접근 방식을 제안합니다. 제안된 접근 방식은 생성기 성능을 최대 28% 향상시키는 것으로 평가되었습니다. 또한, 형식적 검증에 맞춤화된 다단계 에이전트 시스템을 사용하여 Rocq 증명 작성 문제를 해결하고, 그 효과를 실증합니다. 추가적으로, 증명 합성 계획 단계에서 다중 에이전트 논쟁의 사용을 보여주는 제거 연구를 수행합니다.
