挑战AI数学推理极限：FormalMATH基准发布，最强模型成功率仅16%

由香港中文大学、西湖大学、MAP、浙江大学等机构联合推出的FormalMATH形式化数学推理基准测试，包含5560道经过验证的数学题，覆盖代数、微积分、数论等多个领域。结果显示，即便是在最佳条件下，最强模型的成功率也仅为16.46%，多数模型在微积分等领域的表现接近随机猜测。

FormalMATH是目前规模最大的形式化数学推理基准，是经典基准MiniF2F的22.8倍。研究团队采用“三阶段过滤”框架，大幅降低了人工标注的工作量，最终保留了72.09%的高质量命题。

整体来看，主流LLM证明器的表现普遍低迷，代数领域相对较强，但微积分等领域的表现较差，显示出明显的能力断层。分析表明，现有模型常滥用自动化策略，导致冗余假设、不完整证明等问题。

未来，提升LLM形式化推理能力需从多步规划、跨领域泛化以及人机协同验证三个方面突破。FormalMATH的代码、数据和模型已全面公开，供学术界和工业界共同推动相关技术发展。