FMC: Formalization of Natural Language Mathematical Competition Problems

TL;DR

This paper introduces an autoformalization pipeline using large language models to convert natural language mathematical problems into formal representations, creating a new benchmark dataset for automated theorem proving.

Contribution

It presents a fully automatic, training-free autoformalization method, curates a large Olympiad-level dataset, and evaluates LLMs and theorem provers on this challenging benchmark.

Findings

Few-shot learning improves formalization accuracy.

Error feedback enhances autoformalization performance.

The dataset is challenging for current theorem provers.

Abstract

Efficient and accurate autoformalization methods, which leverage large-scale datasets of extensive natural language mathematical problems to construct formal language datasets, are key to advancing formal mathematical reasoning. In this paper, we propose an autoformalization pipeline based on large language models with error feedback, achieving a fully automatic and training-free formalization approach. Using this pipeline, we curate an Olympiad-level dataset aligning natural language problems with Lean formalizations. The dataset comprises $3,922$ mathematical problems in natural language and $9,787$ in Lean, of which $64.46\%$ were assessed as at least above-average quality, making it suitable as a benchmark for automated theorem provers. Additionally, we investigate the formalization and reasoning capabilities of various LLMs and empirically demonstrate that few-shot learning, error feedback, and increasing sampling numbers enhance the autoformalization process. Experiments of three automated theorem provers on the \dataset\ dataset also highlight its challenging nature and its value as a benchmark for formal reasoning tasks.