PaperlayerView exact revision on arXiv

Source-linked AI summary

FIMO: A Challenge Formal Dataset for Automated Theorem Proving

Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, Ming Zhang, Qun Liu

arXiv:2309.04295v2cs.AI

TL;DR

IMO-level theorem proving remains difficult for LLMs, while formal datasets are costly to build and often omit natural-language statements or proofs. FIMO provides 149 Lean-formalized IMO shortlisted problems with informal statements and proofs, using feedback-assisted auto-formalization. GPT-4 proved none of the FIMO statements, underscoring the continuing challenge at this level.

  • Problem

    LLM-based provers still solve few IMO-level problems, and formal datasets are costly to create and often omit natural-language statements or proofs.

    Source: Introduction · p. 1

  • Method

    FIMO pairs 149 Lean-formalized IMO shortlisted problems with informal statements and proofs, using auto-formalization refined through human and Lean feedback.

    Source: Introduction · pp. 1–2, Dataset Analysis · p. 5

  • Results

    GPT-4 achieved over 20% Pass@8 on miniF2F but proved no statements in FIMO, and using human informal proofs did not improve its Pass@8.

    Source: Result · p. 6

  • Takeaways & Limitations

    GPT-4’s inability to prove FIMO statements underscores the enduring challenge of automated theorem proving at IMO level.

    Source: Conclusion · p. 7

    FIMO excludes combinatorics and geometry problems, covers publicly available IMO shortlisted problems from 2006–2021, and may contain a very small number of errors despite human checking.

    Source: Limitation · p. 7

Abstract

from arXiv · show

We present FIMO, an innovative dataset comprising formal mathematical problem statements sourced from the International Mathematical Olympiad (IMO) Shortlisted Problems. Designed to facilitate advanced automated theorem proving at the IMO level, FIMO is currently tailored for the Lean formal language. It comprises 149 formal problem statements, accompanied by both informal problem descriptions and their corresponding LaTeX-based informal proofs. Through initial experiments involving GPT-4, our findings underscore the existing limitations in current methodologies, indicating a substantial journey ahead before achieving satisfactory IMO-level automated theorem proving outcomes.

Introduction

IMO-level automated theorem proving remains an open challenge, while formal data is costly to create and existing datasets often lack difficulty or natural-language proofs. FIMO addresses these gaps with 149 Lean statements paired with informal statements and proofs, and baseline experiments show current LLMs still struggle with IMO-level problems.

Introduction

  • Current LLM-based provers solve few IMO-level problems, leaving the majority unexplored.The paper identifies this as a pivotal open question requiring profound mathematical reasoning.Source: Introduction · p. 1
  • Formal mathematical data is scarce because expert formalization requires substantial effort and cost.The paper contrasts mathlib’s 45MB with the 570GB CommonCrawl dataset used in GPT-3 training.Source: Introduction · p. 1
  • FIMO contains 149 challenging IMO-level Lean statements with corresponding informal statements and natural-language proofs.Each formal statement is manually examined for faithful alignment with its informal version.Source: Introduction · pp. 1–2
  • The authors propose auto-formalization with human and environmental feedback and report that current LLMs struggle to prove IMO-level statements.They evaluate GPT-4 and conduct case studies of its problem-solving capacity.Source: Introduction · p. 2

Formal Mathematics

Formal mathematics represents statements and proofs in a formal domain-specific language that an interactive theorem prover can check automatically.

Formal Mathematics

  • Formal mathematics lets users enter statements and proofs in a formal domain-specific language for automatic correctness checking by an interactive theorem prover.The paper also notes that formal mathematics can support new mathematical insights and educational purposes.Source: Formal Mathematics · p. 2

Auto-Formalization

Formalization translates natural-language mathematical descriptions into formally correct, automatically checkable formats, but the logical gap makes manual work costly. LLM prompting offers an auto-formalization approach, though the cited work reported perfect translations for only 25.3% of competition problems.

Auto-Formalization

  • Formalization translates natural-language mathematics into a formally correct, automatically checkable format.Because formal language must make every simple argument explicit, manual large-scale formalization is tedious, expensive, and time-consuming.Source: Auto-Formalization · p. 2
  • LLM-based auto-formalization prompts models with examples of informal and formal statement pairs.Wu et al. (2022) reported that 25.3% of mathematical competition problems were translated perfectly into Isabelle/HOL specifications.Source: Auto-Formalization · p. 2

Datasets

The related datasets span formal libraries and natural-language competition problems, but differ in scope and representation. MiniF2F offers many manually formalized Olympiad-type statements, while only 40 are authentic IMO problems.

Lean Mathlib

  • Mathlib is a community-maintained Lean library, and the IMO Grand Challenge proposal targets an AI capable of winning an IMO gold medal through formal-to-formal proving.At the time described, mathlib held 32 formal IMO problems with solutions.Source: Lean Mathlib · p. 2
  • MATH contains 12,500 challenging competition problems with step-by-step natural-language solutions, but no formal versions.Its problems come from competitions including AMC 10, AMC 12, and AIME, and are classified into five levels.Source: Lean Mathlib · p. 2

MiniF2F

  • MiniF2F contains 488 manually formalized Olympiad-type statements across Lean, Isabelle, and Coq, with only 40 drawn from authentic IMO problems.The original dataset contained only formal statements; a derived version added informal statements and proofs for each problem.Source: MiniF2F · p. 2

Neural Theorem Provers

The section describes provers operating on formal languages and DSP, which uses informal proofs to guide formal proof generation. It also notes methods that expand training data or guide proof search.

Provers with Formal Language

Provers with Informal Language

FIMO Dataset

FIMO converts shortlisted Algebra and Number Theory problems into Lean statements through OCR, feedback-guided auto-formalization, and manual verification. It contains 149 of 245 eligible problems, and analysis reports that reflective feedback raises GPT-4’s formalization success rate from 32.6% to 60.8%.

Dataset Construction

  • The pipeline converts PDF problems to LaTeX with OCR, manually checks the output, and retains the first solution when multiple solutions are available.Multiple sub-questions are treated as independent problems; non-proof questions are reframed as propositions by appending their answers.Source: Dataset Construction · p. 3

Auto-Formalization with Feedback

  • Lean error messages guide iterative LLM refinement, while human experts check semantic correctness; refinement stops at verification or after five iterations.The process uses few-shot prompts rewritten from Isabelle notation into Lean.Source: Auto-Formalization with Feedback · pp. 3–4

Manual Verification

  • Manual checks verify OCR-generated LaTeX and Lean-accepted formal statements against the informal problems to catch semantic misalignment.The authors note that small errors can alter a mathematical statement’s meaning.Source: Manual Verification · p. 4

Statistics

  • FIMO contains 149 human-verified Lean formalizations among 245 shortlisted Algebra and Number Theory problems from 2006–2021, with aligned natural-language problems and solutions.Problems with multiple sub-questions are counted independently; the work reports formalizing over 60% of the eligible problems.Source: Statistics · p. 4

Dataset Analysis

  • Reflective feedback raises GPT-4’s formalization success rate from 32.6% to 60.8%, while human intervention remains comparable.Algebra problems are generally easier to formalize than Number Theory problems, and gain more from feedback.Source: Dataset Analysis · p. 5
  • In sampled failures, “type mismatch” and “unknown identifier” were the most common syntax errors, though GPT-4 often corrected errors using Lean’s high-level messages.The analysis also reports that GPT-4 can infer latent mathematical facts, such as positivity and triangle inequalities, from informal statements.Source: Dataset Analysis · pp. 5–6

Experiments and Discussion

GPT-4 exceeded 20% Pass@8 on miniF2F but proved no FIMO statements, while experiments examined informal-proof guidance and failure modes. The analysis links FIMO’s difficulty to advanced reasoning demands and identifies mathematical and tactic errors in generated proofs.

Experiments and Discussion

  • The experiments compare formal-only theorem-proving methods with methods using both formal and informal data; FIMO supports both classes.The authors also adapt the informal-proof-guided approach because the original DSP framework targets Isabelle rather than Lean.Source: Experiments and Discussion · p. 6

GPT-4 Guided by Informal Proofs

  • The guidance approach acquires human or GPT-4-generated informal proofs, then prompts formal proof generation with formal and informal statements plus the proof.Human proofs come from IMO selection-committee solutions; GPT-4 informal proofs are regenerated for each formal-proof attempt.Source: GPT-4 Guided by Informal Proofs · p. 6

Result

  • GPT-4 achieved over 20% Pass@8 on miniF2F but proved no FIMO statements; model-generated informal proofs yielded better Pass@8 than human proofs.The authors attribute this difference to the diversity and exploration of directions in generated informal proofs, and believe FIMO problems require more advanced reasoning.Source: Result · pp. 6–7, Table 9 · p. 7

Error Analysis

  • Most model-synthesized informal proofs were mathematically incorrect, potentially misleading formal proof generation.With human-proof guidance, GPT-4 followed solution structure but failed to apply tactics properly; generated proofs averaged over 11 lines, versus fewer than 3 for GPT-f on miniF2F, as reported in Zheng, Han, and Polu 2022.Source: Error Analysis · p. 7, Figure 2 · p. 7

Limitation

FIMO’s coverage is limited by Lean expressibility and the availability of shortlisted problems with solutions. The authors also note that automated formalization and human checking may leave a very small number of errors.

Limitation

  • Combinatorics and Geometry are absent because they are less expressible in formal systems like Lean.This problem-type shift may affect evaluation when FIMO is used as a metric.Source: Limitation · p. 7
  • FIMO covers IMO Shortlisted Problems with Solutions from 2006 to 2021; earlier problems available through other channels are not included.Source: Limitation · p. 7
  • Although formal statements are automatically formalized and human-checked, a very small number of errors may remain.Source: Limitation · p. 7

Conclusion

FIMO pairs formal IMO-level problem statements with informal statements and proofs, and the paper evaluates GPT-4 guided by informal proofs. GPT-4 proves none of FIMO’s statements, underscoring the challenge of IMO-level automated theorem proving.

Conclusion

  • GPT-4 guided by informal proofs failed to formally prove any statement in FIMO, highlighting the continuing challenge of IMO-level automated theorem proving.Source: Conclusion · p. 7
  • FIMO provides formal IMO-level problem statements alongside informal statements and informal proofs in LaTeX.Source: Conclusion · p. 7
  • The paper reports that reflective feedback is significant for improving the auto-formalization process.Source: Conclusion · p. 7
Loading 2309.04295v2…