Meta AI 构建了一个神经定理证明器，解决了 10 个国际数学奥林匹克问题 (IMO)，比之前的任何人工智能 AI 系统多 5 倍
证明数学定理长期以来一直被科学家们认为是发展人工智能的重要第一步。 要确定一个猜想是对还是错，您必须使用符号思维来对大量可能的备选方案进行分类。 即使是最先进的人工智能系统也无法执行这些任务。
人工智能是当今最先进的。 “立即解决”或可以一次性提出问题的完整解决方案的机器是最先进的。 这不是大多数人处理困难情况的方式。 形式化和量化数学推理要困难得多。
Meta AI 是数学和人工智能交叉领域的重大发展。 该团队的神经定理证明系统解决的 IMO 问题是之前任何人工智能系统的五倍，总共十个。 在一项重要的数学测试 miniF2F 中，AI 的表现优于 state-of-the-art 20%，Metamath 优于 10%。
来源和详细信息：