Import AI· Jack Clark·· 17 天前AI 评分44
Import AI 478：数学如何助力对齐；ProgramBench；OpenAI 展示锁定 AI 系统有多难
Import AI 478: Math for alignment; ProgramBench; and Mirendil shows what RSI means
AI 导读
AI 安全初创公司 Resolution 用多智能体自动形式化了统计学习理论中的奇点消解，耗时约一周、消耗约 100B 输入 token 和约 3 亿输出 token（约 $135,000），产出约 60 万行 Lean 代码。
来源：Import AI · importai.substack.com