사람의 단계별 증명 활용
Coq에서는 사용자가 기계로 확인할 수 있는 증명을 한 단계씩 구성한다. GamePad는 이런 상호작용형 증명 과정이 사람의 감독을 받는 학습에 제공하는 가능성을 살핀다.
다음 증명 단계 예측
전술 예측은 현재의 증명 상태에서 어떤 다음 단계를 적용할지 예측하는 과제다. 완성된 정답만 고르는 것과 달리 증명을 이어 가는 선택을 모델링한다.
남은 단계 수의 평가
위치 평가는 증명을 끝내기까지 몇 단계가 남았는지 예측한다. 같은 증명 탐색에서도 다음 행동을 정하는 과제와 현재 위치를 평가하는 과제는 구별된다.
초기 실험의 범위
연구는 간단한 대수적 재작성 문제의 증명을 합성하고 Feit-Thompson 정리의 형식화에서 기준 모델을 학습했다. 작은 합성 문제와 큰 수학 형식화의 학습 과제를 함께 살폈다.