고차 논리 및 정리 증명을 위한 그래프 표현

본 논문은 그래프 신경망(GNNs)을 고차 증명 탐색에 처음으로 적용한 결과를 제시하며, 이 방법이 해당 분야에서 최신 기술을 개선할 수 있음을 입증합니다. 상호작용적인 고차 정리 증명기는 대부분의 수학적 이론을 형식화할 수 있으며, 딥 러닝에 대한 중대한 도전 과제로 알려져 있습니다. 고차 논리는 매우 표현력이 뛰어나며, 명확하게 정의된 문법과 의미론을 가지고 있지만, 공식을 그래프 기반 표현으로 변환하는 잘 확립된 방법은 아직 존재하지 않습니다. 본 논문에서는 고차 논리의 여러 그래픽 표현 방식을 검토하고, 이를 고차 정리 증명 벤치마크인 HOList와 비교 평가합니다.