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

Understand

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.