数据用于数学 Copilot：更好地呈现证明以适用于机器学习
机器学习
2025-12-22 v2
摘要
用于训练和评估基于AI的数学 Copilot（主要是大型语言模型）的datasets和 benchmarks 存在诸多不足和误导。这包括从数学复杂性范围受限到捕捉最终书面证明之外的要素（如激发证明，或表示导致证明的思维过程）。这些问题因类似Goodhart定律的动态而加剧：随着benchmark性能成为模型开发的主要目标，benchmarks本身变得不够可靠地指示真正的数学能力。我们系统性地探讨了这些限制，认为提升大型语言模型或任何后续AI-based数学助手（copilot或"思维伙伴"）的能力，必要时进行课程纠正，既在数学datasets的设计中，也在模型数学能力的评估标准中。特别是，benchmarks需要超越将theorem statements直接映射到proofs的现有result-based datasets，转而关注将更丰富的数学研究实践转化为LLM可学习数据的datasets。这包括监督证明过程和proof发现过程本身的benchmarks，我们主张数学datasets开发者考虑"激发证明"的概念，这一概念由G. P\'olya于1949年引入，可作为为datasets提供更好证明学习信号的蓝图，以缓解上述一些限制。
关键词
引用
@article{arxiv.2412.15184,
title = {Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learning},
author = {Simon Frieder and Jonas Bayer and Sam Looi and Jacob Loader and Julius Berner and Katherine M. Collins and András Juhász and Fabian Ruehle and Sean Welleck and Gabriel Poesia and Ryan-Rhys Griffiths and Adrian Weller and Anirudh Goyal and Cameron Freer and Thomas Lukasiewicz and Timothy Gowers},
journal= {arXiv preprint arXiv:2412.15184},
year = {2025}
}
备注
59 pages