탐색과 모델의 결합
Transformer 기반 자동 증명기에 새로운 탐색 알고리즘을 결합했다. 연구는 증명 후보를 생성하는 모델만이 아니라 어떤 탐색 절차를 사용하는지도 중요한 구성 요소로 살폈다.
이전 탐색에서 다시 학습하기
모델은 앞선 증명 탐색을 통해 얻은 결과로 온라인 학습한다. 고정된 주석 증명만 사용하는 경우와 달리 탐색 과정에서 새 학습 신호를 얻는 방식이다.
탐색만의 효과와 학습 효과
초기 연구는 주석 증명으로 학습한 모델에 HTPS를 적용한 결과와 미증명 정리에 대한 온라인 학습을 더한 결과를 구분했다. 두 단계의 개선을 하나의 독립 시험 점수로 섞지 않는 것이 중요하다.
여러 증명 환경의 비교
연구는 복잡도가 다른 세 환경에서 구성 요소를 제거하며 효과를 분석했다. Metamath와 Lean 기반 miniF2F-curriculum의 평가를 통해 탐색과 학습의 기여를 비교했다.