FormalMATH

香港中文大学等机构联合推出FormalMATH基准测试，包含5560道经过验证的数学题。尽管大语言模型在自然语言处理和代码生成领域表现优异，但在数学定理证明任务中成功率仅为16.46%。研究提出了一套三阶段过滤框架用于自动形式化和语义一致性检测，并分析了现有LLM证明器的表现，发现代数较强而微积分较弱，存在滥用自动化策略的问题。