# Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning

arXiv: https://arxiv.org/abs/2412.15184 · HTML: https://mlsanity.com/paper/2412.15184/

## Key facts

- Cited by 11 papers in the map (data through 14 Oct 2026).
- Builds on 81 of its 138 references that are in the map.
- First posted on arXiv 19 Dec 2024.

## Builds on (most cited first, 30 of 81)

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Measuring Massive Multitask Language Understanding](https://mlsanity.com/paper/2009.03300/) (2020)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [Qwen Technical Report](https://mlsanity.com/paper/2309.16609/) (2023)
- [Gemini 1.5: Unlocking multimodal understanding across millions of tokens of context](https://mlsanity.com/paper/2403.05530/) (2024)
- [A Survey of Large Language Models](https://mlsanity.com/paper/2303.18223/) (2023)
- [Qwen2 Technical Report](https://mlsanity.com/paper/2407.10671/) (2024)
- [MathVista: Evaluating Mathematical Reasoning of Foundation Models in Visual Contexts](https://mlsanity.com/paper/2310.02255/) (2023)
- [Datasheets for Datasets](https://mlsanity.com/paper/1803.09010/) (2018)
- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems](https://mlsanity.com/paper/2402.14008/) (2024)
- [DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Model](https://mlsanity.com/paper/2405.04434/) (2024)
- [Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvement](https://mlsanity.com/paper/2409.12122/) (2024)
- [Large Language Models are not Fair Evaluators](https://mlsanity.com/paper/2305.17926/) (2023)
- [The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery](https://mlsanity.com/paper/2408.06292/) (2024)
- [Are NLP Models really able to Solve Simple Math Word Problems?](https://mlsanity.com/paper/2103.07191/) (2021)
- [AGIEval: A Human-Centric Benchmark for Evaluating Foundation Models](https://mlsanity.com/paper/2304.06364/) (2023)
- [Program Induction by Rationale Generation : Learning to Solve and Explain Algebraic Word Problems](https://mlsanity.com/paper/1705.04146/) (2017)
- [WizardMath: Empowering Mathematical Reasoning for Large Language Models via Reinforced Evol-Instruct](https://mlsanity.com/paper/2308.09583/) (2023)
- [GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models](https://mlsanity.com/paper/2410.05229/) (2024)
- [TinyStories: How Small Can Language Models Be and Still Speak Coherent English?](https://mlsanity.com/paper/2305.07759/) (2023)
- [CMMLU: Measuring massive multitask language understanding in Chinese](https://mlsanity.com/paper/2306.09212/) (2023)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Llemma: An Open Language Model For Mathematics](https://mlsanity.com/paper/2310.10631/) (2023)
- [Orca: Progressive Learning from Complex Explanation Traces of GPT-4](https://mlsanity.com/paper/2306.02707/) (2023)
- [Solving General Arithmetic Word Problems](https://mlsanity.com/paper/1608.01413/) (2016)

## Built on by (most cited first, 11 of 11)

- [Can We Trust AI Benchmarks? An Interdisciplinary Review of Current Issues in AI Evaluation](https://mlsanity.com/paper/2502.06559/) (2025)
- [Aviary: training language agents on challenging scientific tasks](https://mlsanity.com/paper/2412.21154/) (2024)
- [On Benchmarking Human-Like Intelligence in Machines](https://mlsanity.com/paper/2502.20502/) (2025)
- [MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving](https://mlsanity.com/paper/2503.03205/) (2025)
- [A Matter of Interest: Understanding Interestingness of Math Problems in Humans and Language Models](https://mlsanity.com/paper/2511.08548/) (2025)
- [Documenting Deployment with Fabric: A Repository of Real-World AI Governance](https://mlsanity.com/paper/2508.14119/) (2025)
- [Matrix as Plan: Structured Logical Reasoning with Feedback-Driven Replanning](https://mlsanity.com/paper/2601.10101/) (2026)
- [Tool Use Reduces Depth-Induced Collapse in OOD Reasoning](https://mlsanity.com/paper/2602.21061/) (2026)
- [ImProver 2: Iteratively Self-Improving LMs for Neurosymbolic Proof Optimization](https://mlsanity.com/paper/2605.22885/) (2026)
- [Human agency in initial human-AI proof formalization workflows](https://mlsanity.com/paper/2606.04273/) (2026)
- [The Missing Primitive: Diagnosing and Repairing Mathematical Reasoning in Large Language Models](https://mlsanity.com/paper/2610.02191/) (2026)

## Abstract (arXiv)

The datasets and benchmarks commonly used to train and evaluate the mathematical capabilities of AI-based mathematical copilots (primarily large language models) exhibit several shortcomings and misdirections. These range from a restricted scope of mathematical complexity to limited fidelity in capturing aspects beyond the final, written proof (e.g. motivating the proof, or representing the thought processes leading to a proof). These issues are compounded by a dynamic reminiscent of Goodhart's law: as benchmark performance becomes the primary target for model development, the benchmarks themselves become less reliable indicators of genuine mathematical capability. We systematically explore these limitations and contend that enhancing the capabilities of large language models, or any forthcoming advancements in AI-based mathematical assistants (copilots or ``thought partners''), necessitates a course correction both in the design of mathematical datasets and the evaluation criteria of the models' mathematical ability. In particular, it is necessary for benchmarks to move beyond the existing result-based datasets that map theorem statements directly to proofs, and instead focus on datasets that translate the richer facets of mathematical research practice into data that LLMs can learn from. This includes benchmarks that supervise the proving process and the proof discovery process itself, and we advocate for mathematical dataset developers to consider the concept of "motivated proof", introduced by G. P'olya in 1949, which can serve as a blueprint for datasets that offer a better proof learning signal, alleviating some of the mentioned limitations.