AlphaGeometry 接近 IMO 金牌选手水平，以 neuro-symbolic 系统实现机器可验证几何证明

Google DeepMind 于 1 月 17 日发布 AlphaGeometry，一个将 neural language model 与 symbolic deduction engine 结合的 neuro-symbolic geometry system。系统在 IMO-AG-30 中解决 30 道 olympiad geometry problems 中的 25 道，接近人类金牌选手平均 25.9 道；训练不依赖人工示范，而是从约 1 亿个合成几何样本中学习构造选择，最终证明结构可由计算机检查。