本文重新审视了奥林匹克级几何中自动化定理证明的挑战，特别关注 IMO-AG-30 基准。作者认为，Wu 的方法是一种代数方法，以前被认为不如 AlphaGeometry 等合成方法有效，但它表现出了令人惊讶的强度，并且与其他技术结合时可以显着提高性能。
Wu 的方法可以将符号人工智能提升到银牌得主的竞争对手，而 AlphaGeometry 则可以超越 IMO Geometry 金牌得主。
主要发现：
- 仅 Wu 的方法就解决了 30 个 IMO-AG-30 问题中的 15 个， 超过了之前报告的性能，甚至解决了 AlphaGeometry 无法解决的问题。
- 吴的方法与演绎数据库和角度/比率/距离追逐（DD+AR）相结合解决了21个问题， 达到了与IMO银牌得主相当的水平，并建立了强大的完全符号基线。
- Wu 的方法与 AlphaGeometry 相结合，实现了最先进的性能，解决了 27 个问题 ，超越了金牌得主的能力。
论文的优点：
- 强调代数方法的潜力： 挑战代数方法在该领域不如综合方法的观念。
- 展示组合不同方法的力量： 展示 Wu 的方法如何补充 DD+AR 和 AlphaGeometry 等现有技术，从而显着提高性能。
- 提出有关当前基准测试局限性的问题： 表明 IMO 几何问题可能不够复杂，无法充分测试现代求解器的功能。
论文的缺点：
- 评估范围有限： 作者仅在 IMO-AG-30 基准上进行评估，这可能无法代表整个几何问题。
- 实施挑战： 本文承认吴方法当前实施的局限性，并呼吁在这一领域进一步发展。
- 缺乏可解释性： 像吴的方法这样的代数方法因产生较少的人类可读证明而闻名，这在某些情况下可能是一个缺点。
总的来说，本文为重新评估吴的方法及其在自动几何定理证明中的潜力提供了令人信服的案例。研究结果鼓励进一步探索这种方法并开发新的基准，以真正突破基于人工智能的几何推理的界限。
网友评论：
1. 十多年前，我就通过了数学奥林匹克竞赛，并获得了物理竞赛的资格。这是一种专门为提高几何解题能力而设计的狭义人工智能。当一个通用人工智能，甚至一个大模型能在数论或组合学（忘了拓扑学之类的东西）的问题上胜出/推理时，我就会觉得这很重要了，我很期待那一天的到来。也许就在今年年底？
2. 大大模型将狭义人工智能纳入其 MOE专家系统 的一部分。
3. 诀窍不是获得具体问题的答案，而是将解决数学问题的推理能力融入一般思维中。 MOE专家系统 无法解决这个问题，至少在所有数学位可以提供数字作为响应的情况下无法解决。
4. 当通用人工智能算法能够破解乘法时，我会很高兴，我指的不是“2*2”乘法，而是不使用计算器的任意长的数字链。我们人类小时候用笔和纸就可以做的事情。
5. 几何是关键问题。几何问题对于人工智能来说比其他类别容易得多。有大量的参赛者可以解决几何问题，但不会解决组合问题。今年我们几乎已经拥有了金牌级别的几何图形和 alphageometry，所以这没什么大不了的。
6. 爆炸新闻！计算机擅长数学，因为计算机在数学方面确实很糟糕。