논리 공식의 그래프 신경망 표현을 서브그래프 풀링을 통해 개선하기

딥러닝과 자동 정리 증명의 통합 분야에서 최근의 발전은 논리 공식을 딥러닝 시스템의 입력으로 표현하는 데 초점이 맞춰져 왔다. 특히, 논리적 표현의 기반이 되는 그래프 표현을 활용할 수 있도록 구조 인식형 신경망 방법을 적응시키는 데 대한 관심이 증가하고 있다. 기존의 문자 수준 및 토큰 수준 접근 방식에 비해 더 효과적인 그래프 기반 방법은 종종 입력의 핵심 구조적 특성을 충분히 포착하지 못하게 하는 표현상의 타협을 수반해 왔다. 본 연구에서는 이전 방법들의 표현적 한계를 극복하도록 설계된 새로운 논리 공식 임베딩 기법을 제안한다. 제안하는 아키텍처는 다양한 표현력 수준의 논리 체계—예를 들어 일차 논리와 고차 논리—에 모두 적용 가능하다. 두 가지 표준 데이터셋에서 제안하는 아키텍처를 평가한 결과, 전제 선택(premise selection)과 증명 단계 분류(proof step classification) 모두에서 최신 기준(SOTA, state-of-the-art) 성능을 달성함을 확인하였다.