FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916985783189504 |
|---|---|
| author | Yang, Xiao-Wen Zhang, Zihao Cao, Jianuo Zhou, Zhi Li, Zenan Guo, Lan-Zhe Yao, Yuan Chen, Taolue Li, Yu-Feng Ma, Xiaoxing |
| author_facet | Yang, Xiao-Wen Zhang, Zihao Cao, Jianuo Zhou, Zhi Li, Zenan Guo, Lan-Zhe Yao, Yuan Chen, Taolue Li, Yu-Feng Ma, Xiaoxing |
| contents | 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, |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_02335 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory Yang, Xiao-Wen Zhang, Zihao Cao, Jianuo Zhou, Zhi Li, Zenan Guo, Lan-Zhe Yao, Yuan Chen, Taolue Li, Yu-Feng Ma, Xiaoxing Computation and Language Artificial Intelligence 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, |
| title | FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory |
| topic | Computation and Language Artificial Intelligence |
| url | https://arxiv.org/abs/2510.02335 |