FormalMATH发布了5560道数学题的基准测试，以评估AI模型的数学推理能力。最佳模型的成功率仅为16.46%，显示出在严格逻辑推导方面的困难。研究团队提出了自动化流程以提高效率，并呼吁学术界共同推动形式化数学推理技术的发展。

本文提出了FormalMATH，一个包含5560个经过形式验证的数学问题的大型基准，旨在提升人工智能的形式数学推理能力。研究通过人机协作的自动形式化流程，降低了专业标注成本，并揭示了当前语言模型在形式证明中的局限性，为未来研究指明了方向。