如题所述
OpenAI 在持续的创新中又迈出了一大步,发布了名为 GPT-f 的新模型,专门用于自动定理证明(ATP)。这款基于 Transformer 语言模型的工具,针对 Metamath 形式化语言,展现出了强大的自动证明能力和证明助手功能。
据论文作者 Stanislas Polu 在 Twitter 的介绍,GPT-f 在实验中超越了现有自动定理证明器 MetaGen-IL,成功证明了测试集中高达 56.22% 的定理,相比之下,MetaGen-IL 只能证明 21.16%。更值得注意的是,GPT-f 还发现了 23 个新的简短证明,其中一部分已被接纳进 Metamath 函式库,这是深度学习模型首次得到数学家的正式认可。
然而,对于 GPT-f 的评价并不完全一致。人工智能领域的大佬如 Gary Marcus 和 Ben Goertzel 表示,尽管 GPT-f 在 ATP 领域取得进展,但他们认为它并不是达到人类水平数学证明的正确研究方向。他们认为,人们可能在错误地将 GPT 用于不适合的领域,这与 GPT-f 的初衷不符。
目前,网友们对 GPT-f 的反应多是中立的,普遍以观察态度对待。他们关注的是模型的实验结果,而非过度吹捧。部分网友提出疑问,如有效证明步骤的定义以及 GPT-f 在处理未被证明的定理时的行为,这表明他们对模型的工作原理保持着深入探讨的兴趣。
总的来说,尽管 GPT-f 在数学推理证明方面展现出了新成果,但其是否能真正推动领域的进步,以及如何避免误用,仍需要业界的持续讨论和验证。感兴趣的朋友可以在论坛和博客中参与讨论,共同探索这个领域的前沿进展。