TLDR: A new research paper introduces miniF2F-v2, a revised benchmark for AI in formal mathematics. It addresses significant errors, inconsistencies, and simplifications found in the original miniF2F dataset, which led to inflated performance metrics for AI models. The new version provides a more accurate and challenging evaluation for autoformalization and theorem proving systems, revealing a substantial gap between reported and actual AI capabilities in solving complex mathematical problems.
A new research paper titled “miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward” by Azim Ospanov, Farzan Farnia, and Roozbeh Yousefzadeh delves into the challenges of evaluating AI systems in formal mathematical reasoning. The study highlights significant issues with the widely used miniF2F benchmark and introduces a corrected and more robust version, miniF2F-v2, to foster more accurate progress in the field.
Automated reasoning with computers has seen remarkable advancements, especially with the rise of Large Language Models (LLMs). These AI systems are increasingly capable of understanding and proving mathematical theorems in formal languages like Lean. The miniF2F benchmark, comprising 488 theorems from mathematical competitions, has been instrumental in driving progress in Automated Theorem Proving (ATP) and autoformalization – the process of translating natural language math problems into formal statements.
However, the researchers found that the original miniF2F benchmark contained numerous limitations. These included discrepancies between informal (natural language) and formal (Lean) statements, unprovable theorems, and excessive simplifications that made problems easier for AI models than their original competition counterparts. Such issues led to an inflated perception of AI capabilities, with reported accuracies for autoformalization reaching as high as 97% and theorem proving around 70%, while the end-to-end pipeline accuracy was considerably lower, around 36%.
The paper introduces miniF2F-v2, which comes in two variations: miniF2F-v2s (simplified) and miniF2F-v2c (competition). In miniF2F-v2s, errors in informal statements are corrected, and formal statements are modified to precisely match them. This version ensures all theorems are correct and provable, with no discrepancies. miniF2F-v2c takes this a step further by changing informal statements to reflect the exact wording of original competitions, including multiple-choice options and removing solutions when the original problem required participants to find them first. This significantly increases the difficulty and realism of the benchmark.
The authors conducted a thorough evaluation of autoformalization models, such as Herald translator and Kimina autoformalizer, on both miniF2F-v1 and miniF2F-v2. A key finding was the substantial gap between LLM-based evaluations and human expert evaluations of autoformalization accuracy. While LLMs often reported high accuracies (e.g., 97% for Herald), human review revealed much lower figures (e.g., 66%). This indicates that LLMs tend to overlook subtle but critical discrepancies between informal and formal statements, leading to false positives.
Similarly, theorem provers were evaluated on the formal statements of miniF2F-v1, v2s, and v2c. While the overall accuracy of provers decreased on miniF2F-v2 due to the increased difficulty and removal of simplifications, the models showed improved performance on a subset of problems that were previously unprovable in miniF2F-v1. This demonstrates the value of a high-quality, error-free benchmark in accurately diagnosing model strengths and weaknesses.
The research also highlights how the new benchmark impacts AI performance on specific competition types like IMO and AMC problems. Stronger provers experienced a substantial decline in solving IMO problems and a 15-50% accuracy drop on AMC problems in the v2c version, reflecting the more challenging and faithful problem formulations. For a deeper dive into the methodology and results, you can access the full research paper here.
Also Read:
- New Benchmarks Advance AI Mathematical Reasoning to Olympiad Levels
- Scrutinizing AI Explanations: A Deep Dive into PyXAI’s Accuracy
In conclusion, miniF2F-v2 serves as a clearer and more demanding benchmark for evaluating AI systems in formal reasoning. By correcting errors, eliminating simplifications, and ensuring semantic alignment between informal and formal statements, this revised dataset provides a more reliable foundation for measuring true progress in autoformalization and automated theorem proving, guiding future research towards more robust and capable AI mathematicians.
