Thor: 언어 모델과 자동 정리 증명기 통합을 위한 망치의 사용

정리 증명에서 주어진 추측에 대한 증명을 열기 위해 큰 라이브러리에서 유용한 전제들을 선택하는 작업은 핵심적인 중요성을 지닌다. 이는 특히 텍스트 형식으로 대량의 전제를 추론하는 데 한계가 있는 언어 모델 기반 증명기들에게 큰 도전 과제를 제기한다. 본 논문은 언어 모델과 자동 정리 증명기(Automated Theorem Provers, ATPs)를 통합하여 이러한 어려움을 극복하는 프레임워크인 Thor를 제안한다. Thor에서는 자동 정리 증명기의 강력한 능력을 활용하는 '해머(hammers)'라고 불리는 일련의 방법을 전제 선택에 사용하고, 나머지 모든 작업은 언어 모델에 위임한다. Thor는 PISA 데이터셋에서 언어 모델의 성공률을 39%에서 57%로 높였으며, 언어 모델과 자동 정리 증명기 각각이 단독으로 해결하지 못한 문제 중 8.2%를 해결했다. 또한 훨씬 더 적은 계산 자원을 사용함에도 불구하고, MiniF2F 데이터셋에서 기존 최고 수준의 방법들과 동등한 성공률을 달성할 수 있다. 본 연구에서 제시하는 간단한 프로토콜을 통해 Thor는 다수의 대표적인 인터랙티브 정리 증명기(Interactive Theorem Provers, ITPs)에 쉽게 적용 가능하다.