谷歌刚刚推出了一位精英人工智能数学家，它是一个神经符号系统，能将问题形式化为 Lean（一种形式语言），并使用经过微调的 Gemini，使用 AlphaZero 风格的搜索来解决这些问题。
在 IMO（数学奥林匹克竞赛） 2024 上解出 4/6，获得银牌。 未来的数学将由人工智能辅助。
在这篇《人工智能在解决国际数学奥林匹克问题上达到银牌标准》中，Google DeepMind 报告称，他们的 AI 系统 AlphaProof 和 AlphaGeometry 2 在解决 2024 年国际数学奥林匹克 (IMO) 问题时获得了银牌标准。这些系统共同解决了比赛中提出的六个问题中的四个，获得了 42 分中的 28 分，仅比金牌低一分
”我们的系统在几分钟内就解决了一个问题，而解决其他问题则需要长达三天的时间“
关键点：
AlphaProof：该系统专为一般数学推理而设计。它使用大型语言模型 (LLM) 生成候选步骤，然后使用 Lean 形式证明检查系统进行验证。AlphaProof 成功解决了三个问题：两个代数问题和一个数论问题。AlphaGeometry 2：该系统专门研究几何问题，将神经语言模型与基于规则的推理引擎相结合。它在 19 秒内解决了一个几何问题。AlphaGeometry 2 在上一版本的基础上集成了大规模合成数据生成，其中包括 1 亿个独特的训练示例，无需人工演示。成就与局限：
成果：人工智能系统展现出先进的推理能力，解决复杂数学问题的水平堪比人类顶尖选手。这标志着人工智能处理形式数学推理和解决问题的能力迈出了重要一步。局限性：问题被手动翻译成形式数学语言，以便人工智能系统理解，这表明人工智能尚无法独立解释自然语言问题陈述。此外，虽然 AlphaGeometry 2 快速解决了一个问题，但其他问题需要三天时间才能解决，这比人类参赛者允许的时间长得多AlphaProof 和 AlphaGeometry 2 的成功凸显了人工智能在数学发现和解决问题方面的潜力。通过继续改进这些系统并将其与更复杂的推理能力相结合，DeepMind 旨在推进通用人工智能领域并拓展人类知识的边界
网友：还在玩味自己的高考成绩吗？IMO（数学奥林匹克竞赛）被攻克破解了，但是IOL无法被AI破解：最难逻辑考题：来自IOL国际语言学奥林匹克
详细：
