전술 데이터의 부족
형식화된 수학 라이브러리를 구축하려면 전문가의 오랜 작업이 필요하다. 큰 언어 모델로 다음 증명 전술을 예측할 때는 제한된 자료에 과적합할 가능성이 문제가 된다.
증명 내부에서 자료 얻기
PACT는 커널 수준의 증명 항을 이용해 자기 지도 학습 자료를 추출한다. 사람이 새 전술 예시를 작성하는 것과 다른 경로로 학습 신호를 확보한다.
함께 학습하는 목표
추출한 자료의 학습을 일반적인 전술 예측 목표와 병행한다. 내부 증명 표현을 이해하는 학습과 다음 증명 행동을 고르는 학습을 연결하는 방식이다.
Lean에서의 평가
연구는 트랜스포머 언어 모델로 구동하는 신경 증명기를 Lean에 결합했다. 분리한 시험 정리 집합에서의 성공률을 비교했으며 실험 밖의 모든 정리를 증명할 수 있다는 주장은 아니다.
관련 문서
Lean 증명 도구 / Mathlib / LeanDojo / GPT-f / GamePad 증명 환경 / 언어 모델