miniF2F-Lean 재검토: 한계점 분석과 향후 발전 방향 모색

초록

우리는 miniF2F 벤치마크의 형식적·비형식적 명제들을 miniF2F 문제들로 구성된 수학 올림피아드에 참가하는 임무를 부여받은 AI 시스템의 관점에서 철저히 분석합니다. 이러한 설정에서 모델은 자연어로 된 문제를 읽고 이해한 후, Lean 언어로 형식화하고, 문제를 증명해야 하며, 형식적 증명이 모델에 제시된 원본 비형식적 명제와 일치할 경우 각 문제에 대해 점수를 인정받습니다. 우리의 평가 결과에 따르면, 이러한 파이프라인의 최고 정확도는 문헌에 보고된 최첨단(SoTA) 모델을 사용할 경우 약 36%로, 자동 형식화 및 정리 증명 분야 문헌에서 보고된 개별 SoTA 정확도인 97%와 69%보다 상당히 낮습니다. 실패 유형을 분석한 결과, 이러한 정확도 하락의 상당 부분이 miniF2F 문제의 절반 이상에서 발생하는 형식적 명제와 비형식적 명제 간의 불일치에 기인함을 확인했습니다. 우리는 형식적 및 비형식적 명제의 모든 오류, 불일치 및 단순화를 수정하고, 완전히 검증된 형식적·비형식적 명제와 증명을 갖춘 miniF2F-v2를 제시합니다. miniF2F-v2에 대한 전체 정리 증명 파이프라인을 평가한 결과, 최고 정확도는 70%로, 원본 miniF2F의 40%에서 크게 향상되었으나, 이는 자동 형식화 모델과 정리 증명기 간의 상당한 불일치가 여전히 존재함을 나타냅니다. 우리의 심층 분석은 더 높은 품질의 벤치마크가 형식적 추론 분야의 진전을 더 잘 평가하고, 자동 형식화 및 정리 증명 모델의 실패와 성공 유형을 더 잘 진단하는 데 커뮤니티에 도움을 줄 수 있음을 시사합니다. 우리의 데이터셋은 https://github.com/roozbeh-yz/miniF2F_v2에서 이용할 수 있습니다.

English

We perform a thorough analysis of the formal and informal statements in the miniF2F benchmark from the perspective of an AI system that is tasked to participate in a math Olympiad consisting of the problems in miniF2F. In such setting, the model has to read and comprehend the problems in natural language, formalize them in Lean language, then proceed with proving the problems, and it will get credit for each problem if the formal proof corresponds to the original informal statement presented to the model. Our evaluation results reveal that the best accuracy of such pipeline can be about 36% using the SoTA models in the literature, considerably lower than the individual SoTA accuracies, 97% and 69% reported in the autoformalization and theorem proving literature. Analyzing the failure modes, we trace back a considerable portion of this drop to discrepancies between the formal and informal statements for more than half of the problems in miniF2F. We proceed with correcting all the errors, discrepancies and simplifications in formal and informal statements, and present the miniF2F-v2 with fully verified formal and informal statements and proofs. Evaluating the full theorem proving pipeline on miniF2F-v2 leads to the best accuracy of 70%, a significant improvement from the 40% on the original miniF2F, yet indicating considerable misalignment between the autoformalization models and theorem provers. Our deep analysis suggests that a higher quality benchmark can help the community better evaluate progress in the field of formal reasoning and also better diagnose the failure and success modes of autoformalization and theorem proving models. Our dataset is available at https://github.com/roozbeh-yz/miniF2F_v2.

miniF2F-Lean 재검토: 한계점 분석과 향후 발전 방향 모색

miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward

초록

Support