Elamur Research⌕
☰
home / papers / 2023 / FIMO: A Challenge Formal Dataset for Automated Theorem Proving

FIMO: A Challenge Formal Dataset for Automated Theorem Proving

Paper · 2023 · Chengwu Liu, Jianhao Shen, Huajian Xin et al.

Summary

Neural provers built on large language models still rarely solve olympiad-grade problems. Formal data is scarce and costly to produce, existing benchmarks contain few truly hard items, and most formal datasets lack natural-language counterparts. The authors address this with FIMO, a Lean benchmark drawn from the IMO Shortlisted Problems (2006–2021), restricted to Algebra and Number Theory. To build it, they converted the PDFs to LaTeX with the Mathpix tool and checked the output by hand. They rephrased answer-type questions as provable claims. GPT-4 then generated the formalizations, revising its drafts using Lean error messages and human feedback, and every result was manually verified against the source problem. For baselines, GPT-4 wrote informal proofs (either supplied by humans or self-generated) and then turned them into formal Lean proofs. The approach reached over 20% Pass@8 on miniF2F but proved none of the FIMO statements. This shows that IMO-level formal reasoning remains far beyond current methods and gives the field a demanding, bilingual (formal and informal) testbed.

Key points

  • FIMO contains 149 Lean formal statements, each paired with an informal statement and a LaTeX informal proof. It is released on GitHub under the Apache License.
  • The authors report that letting the LLM reflect on Lean checker errors and human comments substantially increased the share of problems that could be auto-formalized.
  • GPT-4 baseline results:
    • On miniF2F-test, Pass@8 was 14.3% with human proofs and 20.9% with self-generated proofs.
    • On FIMO, it scored 0.0% in all settings.
    • Self-generated informal proofs gave better Pass@8, likely because they are more diverse.
  • Error analysis found two main failure modes:
    • Model-written informal proofs were mostly mathematically wrong.
    • With human proofs, GPT-4 followed the reasoning but misapplied tactics such as rw.
    • Even so, its generated proofs averaged more than 11 lines, compared with under 3 for GPT-f.
  • Limitations: the dataset excludes Combinatorics and Geometry, covers only shortlists from 2006–2021, and may contain a few residual formalization errors.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Peking UniversityBeijing · China315 works · 43,268 citations🎓Chinese University of Hong KongHong Kong · China159 works · 16,154 citations🏢Huawei TechnologiesShenzhen · China96 works · 15,432 citations🎓Sun Yat-sen UniversityGuangzhou · China72 works · 9,502 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksComputational Theory and Mathematics · 321 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,685 works

Cite

Cite as Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang and Qun Liu. 2023. FIMO: A Challenge Formal Dataset for Automated Theorem Proving. arXiv:2309.04295.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2309.04295 · arXiv 2309.04295

@misc{liu2023fimo,
  title = {{FIMO: A Challenge Formal Dataset for Automated Theorem Proving}},
  author = {Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang and Qun Liu},
  year = {2023},
  doi = {10.48550/arxiv.2309.04295},
  eprint = {2309.04295},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2309.04295}
}

References

16 references, 12 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Brown, T.; Mann, B.; Ryder, N.; Subbiah, M.; Kaplan, J. D.; Dhariwal, P.; Neelakantan, A.; Shyam, P.; Sastry, G.; Askell, A.; Agarwal, S.; Herbert-Voss, A.; Krueger, G.; Henighan, T.; Child, R.; Ramesh, A.; Ziegler, D.; Wu, J.; Winter, C.; Hesse, C.; Chen, M.; Sigler, E.; Litwin, M.; Gray, S.; Chess… — Language Models are Few-Shot Learners
  2. Han, J. M.; Rute, J.; Wu, Y.; Ayers, E. W.; and Polu, S. 2022. Proof Artifact Co-training for Theorem Proving with Language Models. arXiv:2102.06203.
  3. Hendrycks, D.; Burns, C.; Kadavath, S.; Arora, A.; Basart, S.; Tang, E.; Song, D.; and Steinhardt, J. 2021. Measuring Mathematical Problem Solving With the MATH Dataset. NeurIPS.
  4. Jiang, A.; Czechowski, K.; Jamnik, M.; Milos, P.; Tworkowski, S.; Li, W.; and Wu, Y. T. 2022a. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In NeurIPS.
  5. Jiang, A. Q.; Welleck, S.; Zhou, J. P.; Li, W.; Liu, J.; Jamnik, M.; Lacroix, T.; Wu, Y.; and Lample, G. 2022b. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. In Submitted to The Eleventh International Conference on Learning Representations.
  6. Koutsoukou-Argyraki, A. 2021. Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started. Jahresbericht der Deutschen Mathematiker-Vereinigung, 123(1): 3–26. mathlib Community, T. 2020. The Lean Mathematical Library. In Proceedin…
  7. OpenAI. 2023. GPT-4 Technical Report. arXiv:2303.08774.
  8. Polu, S.; Han, J. M.; Zheng, K.; Baksys, M.; Babuschkin, I.; and Sutskever, I. 2023. Formal Mathematics Statement Curriculum Learning. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net.
  9. Polu, S.; and Sutskever, I. 2020. Generative Language Modeling for Automated Theorem Proving. arXiv:2009.03393.
  10. Selsam, D.; Buzzard, K.; Barton, R.; Liang, P.; Loss, S.; and Wiedijk, F. 2020. IMO Grand Challenge. find
  11. Shen, J.; Yin, Y.; Li, L.; Shang, L.; Jiang, X.; Zhang, M.; and Liu, Q. 2021. Generate & Rank: A Multi-task Framework for Math Word Problems. In Findings of the Association for Computational Linguistics: EMNLP 2021, 2269–2279. Punta Cana, Dominican Republic: Association for Computational Linguistics… find
  12. Shinn, N.; Cassano, F.; Labash, B.; Gopinath, A.; Narasimhan, K.; and Yao, S. 2023. Reflexion: Language Agents with Verbal Reinforcement Learning. arXiv:2303.11366.
  13. Szegedy, C. 2020. A Promising Path Towards Autoformalization and General Artificial Intelligence. In Benzmüller, C.; and Miller, B., eds., Intelligent Computer Mathematics, 3–20. Cham: Springer International Publishing. ISBN 978-3-030-53518-6. find
  14. Wang, H.; Yuan, Y.; Liu, Z.; Shen, J.; Yin, Y.; Xiong, J.; Xie, E.; Shi, H.; Li, Y.; Li, L.; Yin, J.; Li, Z.; and Liang, X. 2023. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function. In Proceedings of the 61st Annual Meeting of the Association for Com… find
  15. Wu, Y.; Jiang, A. Q.; Li, W.; Rabe, M. N.; Staats, C.; Jamnik, M.; and Szegedy, C. 2022. Autoformalization with Large Language Models. arXiv:2205.12615.
  16. Zheng, K.; Han, J. M.; and Polu, S. 2022. MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics. arXiv:2109.00110.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/liu-2023-fimo-challenge-formal-dataset-automated/