只需一步,快速开始
短信验证,便捷登录
军衔等级:
一级军士长
大模型们,至少需要再战个几年吧。
之所以引入这个基准,是因为大模型越来越多地碾压现有的数学基准
通常需要专业数学家花费数小时甚至数天的努力
如果模型在达到标记限制之前没有提交最终答案,它将收到一个最终提示,要求立即提交最终答案; 如果在收到该提示后模型仍然无法提供正确格式化的最终答案,则该尝试被标记为不正确。
之所以引入这个基准,是因为大模型越来越多地碾压现有的数学基准。有趣的问题是,尽管从许多方面(/evals)来看,大模型正逐步跻身顶级专家行列(如数学和编码等),但你不会雇用他们而不是让他们从事最琐碎的工作。 如果你把问题描述整齐地放在盘子里,他们就能解决复杂的封闭式问题,但他们很难连贯地把长长的、自主的、解决问题的序列串联起来,而人却会觉得非常容易。 这是莫拉维克悖论的变相,他在30多年前就观察到,对人类来说容易/困难的事情,与对计算机来说容易/困难的事情,在非直觉上可能大相径庭。 例如,人类对计算机下国际象棋印象深刻,但国际象棋对计算机来说却很容易,因为它是一个封闭的、确定性的系统,具有离散的行动空间、完全的可观测性等等。 反之亦然,人类可以系好鞋带或叠好衬衫,而且根本不需要考虑太多,但这是一项极其复杂的传感运动任务,对硬件和软件的技术水平都是挑战。 这就像不久前OpenAI发布的魔方一样,大多数人都把注意力集中在解魔方本身(这是微不足道的),而不是用机器人的手转动魔方的一个面这一实际难度极高的任务。 因此,我非常喜欢这个FrontierMath基准,我们应该制作更多的基准。但我也认为,如何为所有 “容易 “但其实很难的东西创建评估是一个有趣的挑战。 很长的语境窗口、连贯性、自主性、常识、有效的多模态输入/输出…… 我们如何建立良好的 “初级工作 “评估?就像你对团队中任何初级实习生的期望。
陶哲轩梦想的就是这样的东西,可以连接到LEAN(微软研究院推出的一款定理证明器),让数学家成为编辑、顾问,偶尔处理一些真正困难的部分,而其余部分则自动化且可证明正确。 很难说一个在这次基准测试中能够达到80%的LLM对数学家来说没有用处。
0 举报本楼
发表回复 回帖后跳转到最后一页
手机版|C114 ( 沪ICP备12002291号-1 )|联系我们 |网站地图
GMT+8, 2024-11-24 06:26 , Processed in 0.208430 second(s), 16 queries , Gzip On.
Copyright © 1999-2023 C114 All Rights Reserved
Discuz Licensed