miniF2F-Lean再考：限界の検証と前進への道筋

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

November 5, 2025

著者: Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh

cs.AI

要旨

我々は、miniF2Fに含まれる問題から構成される数学オリンピックに参加する任務を負ったAIシステムの観点から、miniF2Fベンチマークにおける形式的記述と非形式的記述の徹底的な分析を行う。この設定では、モデルは自然言語で書かれた問題を読み理解し、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.