REVIEW 7 cited by
FIMO: A Challenge Formal Dataset for Automated Theorem Proving
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
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.
Forward citations
Cited by 7 Pith papers
-
FormalRx: Rectify and eXamine Semantic Failures in Autoformalization
FormalRx diagnoses Lean autoformalization failures with a 28-category SCI taxonomy and an 8B model that jointly predicts alignment, error type, location, and correction.
-
CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
A critic model trained with reinforcement learning judges semantic correctness of Lean 4 formalizations, and using it as a filter sharply improves autoformalization accuracy.
-
MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
MATP-BENCH pairs 1,056 multimodal math problems with formal theorem statements in Lean 4, Coq, and Isabelle; the strongest tested model solves only 5.68% of Lean 4 end-to-end proving tasks at pass@10.
-
Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification
Safe uses step-level formal verification in Lean 4, aggregated by a small LSTM and combined with process reward scores, to improve best-of-n accuracy for LLM mathematical reasoning.
-
LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics
A live benchmark auto-extracts self-contained lemmas from recent arXiv papers and finds top LLMs solve only 10–15% at pass@1.
-
Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks
A grammar-based model of LLM-generated SMT-LIB code produces uncertainty signals that predict formalization errors on some reasoning tasks, with fused signals giving large error reductions only in an in-sample evaluation.
-
Formally Solving Answer-Construction Problems in Lean
ECP, an enumerate-conjecture-prove framework with Lean verification, improves answer-construction accuracy on ConstructiveBench and a PutnamBench subset, but its benchmark has a 17% major-error rate and its abstract r...
Discussion (0). Continue with ORCID to comment.