MiniF2F: 공식 올림피아드 수준 수학을 위한 크로스시스템 벤치마크

우리는 신경형 정리 증명(neural theorem proving)을 위한 통합형 교차 시스템 기준(testbed)을 제공할 목적으로, 공식 올림피아드 수준의 수학 문제들을 포함하는 miniF2F 데이터셋을 제안한다. 현재 miniF2F 벤치마크는 Metamath, Lean, Isabelle(부분적으로), HOL Light(부분적으로)를 대상으로 하며, AIME, AMC 및 국제 수학 올림피아드(IMO)에서 추출한 488개의 문제 문항과 고등학교 및 대학 수준의 수학 과정 자료를 포함한다. 본 연구에서는 GPT-3 기반의 신경형 정리 증명기인 GPT-f를 활용한 기준 성능을 보고하고, 그 성능에 대한 분석을 제공한다. miniF2F는 커뮤니티 주도의 노력이 될 것을 목표로 하며, 본 벤치마크가 신경형 정리 증명 분야의 발전을 촉진하기를 기대한다.