초록
자동 정리 증명(Automated Theorem Proving)은 핵심적인 인공지능 작업 중 하나로, 우리는 이를 연구 대상으로 삼는다. 딥러닝은 정리 증명기를 학습시키는 데 유망한 성과를 보여주었으나, 감독 학습을 위해 활용할 수 있는 인간이 작성한 정리와 증명의 수는 제한적이다. 이러한 한계를 극복하기 위해, 우리는 정리 증명기를 훈련시키는 목적을 위해 자동으로 정리와 증명을 생성할 수 있는 신경망 생성기(Neural Generator)를 학습하는 방안을 제안한다. 실제 응용 과제에 대한 실험 결과, 본 연구에서 제안하는 방법을 통해 생성된 합성 데이터가 정리 증명기의 성능을 향상시키고, 메타매스(Metamath) 환경에서 자동 정리 증명 기술의 최신 기준을 한층 끌어올리는 데 기여함을 확인하였다. 관련 코드는 다음 주소에서 확인할 수 있다: https://github.com/princeton-vl/MetaGen.