본 논문은 포화 기반 정리 증명에서 가장 중요한 선택 지점인 절 선택을 강화 학습(RL) 문제로 설정하여 기존 최첨단 증명기의 휴리스틱을 뛰어넘는 최적의 절 선택 방법을 자동으로 학습하는 것을 목표로 한다. 효율적이면서도 강력한 신경망 구조를 제시하여 절을 평가하고, 이를 Vampire 정리 증명기에 통합하여 성공적인 증명 시도로부터 학습시킨다. TPTP 벤치마크 실험 결과, 신경망 기반 증명기가 기존 전략보다 20% 향상된 성능을 보였다. (제한된 CPU 시간 내 미지의 문제 해결 수 기준)
