증명 환경과의 상호작용
Lean에서 자료를 추출하고 프로그램으로 증명 환경과 상호작용할 수 있게 한다. 도구와 자료 및 모델이 비공개라 연구를 재현하기 어려웠던 문제를 줄이려는 공개 연구 기반이다.
필요한 전제의 선택
증명에 쓰인 전제에 세밀한 주석을 제공한다. 큰 수학 라이브러리에서 어떤 정의와 정리를 사용할지 고르는 전제 선택은 증명 탐색의 중요한 병목이다.
검색을 더한 ReProver
ReProver는 전제를 검색하는 기능을 언어 모델 기반 증명기에 결합한다. 프로그램 분석으로 실제 접근 가능한 전제와 어려운 부정 예를 구별해 검색을 개선하도록 했다.
새 전제에 대한 일반화
초기 벤치마크는 학습에서 사용하지 않은 새 전제에 의존하는 정리를 포함하는 어려운 분할을 제공했다. 익숙한 증명을 되풀이하는 것과 다른 전제를 활용하는 능력을 구분해 평가한다.
관련 문서
Lean 증명 도구 / Mathlib / DPR / 논리학 / 언어 모델 / 추론