대규모 이론에서 모방 없이 추론하기 배우기

본 논문에서는 인간의 증명을 학습하지 않고 대규모 잠재 전제 지식 기반에서 자동 정리 증명을 수행하는 방법을 보여줍니다. 우리는 깊은 강화학습 시나리오에서 tf-idf (term frequency-inverse document frequency) 기반 조회를 통해 선택된 추가 전제를 혼합하는 탐색 메커니즘을 제안합니다. 이는 새로운 정리를 증명하기 위해 관련 있는 전제를 탐색하고 학습하는 데 도움이 됩니다. 우리의 실험 결과는 이러한 탐색 메커니즘으로 훈련된 정리 증명기가 인간의 증명만으로 훈련된 증명기보다 우수한 성능을 발휘함을 보여줍니다. 또한 모방과 강화학습의 조합으로 훈련된 증명기에 가까운 성능을 나타냅니다. 우리는 여러 실험을 수행하여 우리의 탐색 접근 방식이 작동하도록 하는 기본 가정들의 중요성을 이해하므로써 설계 선택의 이유를 설명합니다.