在人工智能领域，自动化几何定理证明一直是衡量机器推理能力的重要标准。近期，一项由IIIT海得拉巴、图宾根大学AI中心和剑桥大学的研究团队共同完成的研究，取得了历史性的突破。该团队开发的AI系统，在国际数学奥林匹克（IMO）几何问题的测试中，成功解决了30个问题中的27个，超越了人类金牌得主的解题能力，创下了新的纪录。
这项研究的核心在于将传统的吴方法与现代的符号方法相结合，形成了一种全新的自动化定理证明方法。吴方法，一种基于代数的几何定理证明方法，能够将几何问题转化为多项式方程组进行求解。该方法的优势在于能够自动生成非退化条件，处理平面几何以及立体和高维几何问题，而这些都是传统符号方法难以轻松处理的领域。
研究团队首先对吴方法进行了重新评估，发现其在解决IMO几何问题上表现出惊人的实力。吴方法单独就能解决15个问题，其中包括一些其他方法无法解决的问题。这一发现导致了两个关键的成果：首先，将吴方法与经典的符号方法（如演绎数据库和角度、比例、距离追踪）结合，仅使用CPU笔记本电脑，每道题限时5分钟，就能解决30个问题中的21个，几乎与AlphaGeometry系统的表现相当，足以媲美IMO银牌得主。其次，吴方法甚至解决了AlphaGeometry未能解决的2个问题。通过将AlphaGeometry与吴方法结合，研究团队在IMO-AG-30测试中创下了解决27个问题的新高，成为首个超越IMO金牌得主的AI方法。
这一成就不仅展示了吴方法在自动化几何定理证明中的潜力，也为未来的研究和应用提供了新的方向。传统的符号方法在模拟人类推理过程方面具有优势，而代数方法则在处理更广泛的问题类型上显示出其独特的力量。研究结果表明，这两种方法的结合可以显著提高AI在解决复杂几何问题上的能力。
然而，这项研究也面临着一些挑战和局限性。首先，尽管吴方法在多个问题上表现出色，但其在生成可读性证明方面的不足仍然是一个需要解决的问题。此外，现有的吴方法实现较少，且存在一些不足，如支持的构造有限、性能非最优等，这些都限制了其在实际应用中的发挥。研究团队认为，通过改进现有的软件和方法，传统的符号方法有望超越AlphaGeometry的证明能力，他们鼓励未来的研究不要仅基于生成人类可读证明的能力来评价吴方法。
