miniCTX: Neural Theorem Proving with (Long-)Contexts
Created by
- Haebom
Category
Empty
저자
Jiewen Hu, Thomas Zhu, Sean Welleck
개요
miniCTX는 실제 Lean 프로젝트와 교과서에서 가져온 정리를 포함하는 새로운 벤치마크입니다. 각 정리는 수만 토큰에 달하는 맥락과 연결되어 있으며, 모델은 정리 증명에 필요한 맥락을 포함하는 해당 저장소의 코드에 접근하여 정리를 증명해야 합니다. 기존의 상태 정보에만 의존하는 방법보다 맥락을 활용하는 미세 조정 및 프롬프팅 방법이 훨씬 성능이 우수함을 보여줍니다. miniF2F와 같은 기존 벤치마크에서는 이러한 맥락 활용 능력을 포착하지 못한다는 점을 밝히고 있으며, 새로운 프로젝트를 쉽게 추가할 수 있도록 자동으로 정리 증명 데이터를 추출하고 주석 처리하는 ntp-toolkit을 함께 제공합니다. miniCTX는 신경망 정리 증명기의 현실적이고 어려운 평가를 제공합니다.
시사점, 한계점
•
시사점:
◦
실제 세계의 형식적 정리 증명에 필요한 맥락(정의, 보조정리, 주석, 파일 구조 등)을 고려한 새로운 벤치마크 miniCTX 제시.
◦
기존 방법 대비 맥락 정보 활용을 통한 정리 증명 성능 향상 확인.
◦
miniF2F 등 기존 벤치마크의 한계점을 보완.
◦
새로운 데이터셋을 쉽게 추가할 수 있는 ntp-toolkit 제공.
◦
신경망 기반 정리 증명기의 현실적인 평가 기준 제시.
•
한계점:
◦
현재는 Lean 프로젝트와 교과서에 국한된 데이터셋. 다양한 형식 및 언어 지원 확장 필요.
◦
ntp-toolkit의 일반성 및 확장성에 대한 추가적인 검증 필요.
◦
맥락 정보의 크기 및 복잡도에 따른 성능 변화에 대한 추가 분석 필요.
