1
免责声明:Al优秘圈所有资讯仅代表作者个人观点,不构成任何投资理财建议。请确保访问网址为(kx.umi6.com) 投诉及建议

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

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

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

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

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

原文链接
本文链接:https://kx.umi6.com/article/18278.html
转载请注明文章出处
分享至
打开微信扫一扫
内容投诉
生成图片
相关推荐
换一换
DeepSeek开源新模型,数学推理能力大提升
2025-05-01 09:16:24
Claude 3.7 Sonnet AI 被曝将祭出上下文窗口 50 万 tokens 杀手锏
2025-03-27 14:51:00
o3猜照片位置深度思考6分48秒,范围精确到“这么近那么美”
2025-04-27 14:15:41
24小时热文
更多
扫一扫体验小程序