Import AI 478: 数学助力对齐、ProgramBench 进展及 RSI 含义

Resolution 团队利用 AI 智能体自动形式化代数几何中的奇点消解，消耗约 100B 输入 token 和 13.5 万美元成本，产出 60 万行 Lean 代码。Claude Opus 5.5 在 ProgramBench 基准上取得 18.5% 的解决率，而该基准今年 5 月发布时所有模型得分均为 0%。