초록
고차 논리에서 딥러닝을 활용하고 수작업으로 만든 특징을 배제한 자동 정리 증명 시스템을 제안합니다. Holophrasm은 메타매스(Metamath) 언어의 형식성을 활용하여, 신경망 강화 밴딧 알고리즘과 액션 열거를 위한 시퀀스-투-시퀀스 모델을 사용하여 부분 증명 트리를 탐색합니다. 이 시스템은 Metamath의 set.mm 모듈에서 14%의 테스트 정리를 증명하였습니다.
고차 논리에서 딥러닝을 활용하고 수작업으로 만든 특징을 배제한 자동 정리 증명 시스템을 제안합니다. Holophrasm은 메타매스(Metamath) 언어의 형식성을 활용하여, 신경망 강화 밴딧 알고리즘과 액션 열거를 위한 시퀀스-투-시퀀스 모델을 사용하여 부분 증명 트리를 탐색합니다. 이 시스템은 Metamath의 set.mm 모듈에서 14%의 테스트 정리를 증명하였습니다.