FormalMATH：大型语言模型形式化数学推理的基准测试

形式化数学推理仍然是人工智能的一个关键挑战，现有基准在范围和规模上的限制阻碍了其发展。为了解决这一问题，我们提出了 FormalMATH，一个大型 Lean4 基准，包含 5,560 个形式化验证的问题，涵盖从高中奥林匹克竞赛挑战到大学水平的定理，涉及代数、应用数学、微积分、数论和离散数学等多个领域。为了减轻手动形式化的低效率，我们引入了一种新颖的人在环自动形式化流程，该流程集成了：(1) 用于陈述自动形式化的专门大型语言模型 (LLMs)，(2) 多 LLM 语义验证，以及 (3) 使用现成的基于 LLM 的证明器进行基于否定的反驳过滤策略。这种方法在手动验证之前保留了 72.09% 的陈述，同时确保了对原始自然语言问题的忠实度，从而降低了专家标注成本。我们对最先进的基于 LLM 的定理证明器的评估揭示了显著的局限性：即使最强的模型在实际采样预算下也仅取得 16.46% 的成功率，表现出明显的领域偏差（例如，在代数方面表现出色但在微积分方面失败）以及过度依赖简化的自动化策略。值得注意的是，我们在链式思考推理场景中发现自然语言解题指导与证明成功之间存在反直觉的反比关系，这表明人类编写的非形式化推理在形式化推理设置中引入了噪音而非清晰度。我们相信 FormalMATH 为形式化数学推理的基准测试提供了一个鲁棒的基准。