FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory
This work addresses the challenge of making LLMs practical assistants for mathematicians by providing a new benchmark, though it is incremental as it builds on existing formal theorem proving efforts.
The authors tackled the problem of evaluating large language models (LLMs) as assistants for mathematicians by introducing FormalML, a benchmark for subgoal completion in formal theorem proving, which revealed persistent limitations in accuracy and efficiency of state-of-the-art provers.
Large language models (LLMs) have recently demonstrated remarkable progress in formal theorem proving. Yet their ability to serve as practical assistants for mathematicians, filling in missing steps within complex proofs, remains underexplored. We identify this challenge as the task of subgoal completion, where an LLM must discharge short but nontrivial proof obligations left unresolved in a human-provided sketch. To study this problem, we introduce FormalML, a Lean 4 benchmark built from foundational theories of machine learning. Using a translation tactic that converts procedural proofs into declarative form, we extract 4937 problems spanning optimization and probability inequalities, with varying levels of difficulty. FormalML is the first subgoal completion benchmark to combine premise retrieval and complex research-level contexts. Evaluation of state-of-the-art provers highlights persistent limitations in accuracy and efficiency, underscoring the need for more capable LLM-based theorem provers for effective subgoal completion,