Anthropic 用 Claude 自动验证现有代码并生成数学证明
Anthropic 使用 Claude 为现有软件生成数学证明，并由独立验证程序 Rocq 自动检查；Anthropic 称，Claude 在数周内生成约 1.8 亿行证明代码。验证条件限于特定处理器架构、单线程程序和小于 64 MB 的输入，单项证明可能消耗数亿个 tokens。
技术方向
推理能力 最新动态
让大模型先想再答的能力：思维链、推理模型，数学与逻辑评测上的突破和争议。
4 条精选近 30 天 4 条共收录 9 条
更新
推理能力的精选
The Decoder精选AI 评分7676 Latent Space精选AI 评分8383 Latent Space 汇总 Kimi K3.1 Pro 发布、独立评测与权重开放进展
Latent Space 汇总了 Kimi K3.1 Pro 的发布信息与社区反应：Moonshot 称该多模态 MoE 模型有 2.8T 总参数、104B 激活参数和 1-million-token 上下文窗口，并提供 Standard 与 Highspeed 版本。
推荐理由：这篇综述把独立评测、厂商宣称与用户反应分开呈现，并对比模型能力、任务成本和权重发布状态，提供了理解发布争议的多重依据。
AWS Machine Learning Blog精选AI 评分7676 Amazon SageMaker AI 多轮强化学习实战指南：训练 gpt-oss-20b 玩 Wordle
AWS 介绍如何在 Amazon SageMaker AI 上用多轮强化学习（MTRL）训练智能体完成需要连续决策的任务，并以 Wordle 演示从部署 AgentCore 智能体、准备数据到训练和评估的完整流程。
推荐理由：文章把多轮强化学习从任务设计、奖励函数到训练评估串成可复现流程，并展示服务设置会显著影响 Wordle 验证结果。
Microsoft Research精选AI 评分8585 Microsoft Research 研究者与合作者证明 KLS 猜想，解决 31 年数学难题
Microsoft Research 研究者与合作者证明了提出于 1995 年的 Kannan–Lovász–Simonovits（KLS）猜想，证明相关界限不随维度增长。研究团队采用人类引导的 AI 智能体搜索流程，探索了约 100 条研究路径；同等总 token 预算下的无引导尝试未能解决问题。独立团队随后给出并行证明，另有 Lean 4 形式化验证工作。
推荐理由：研究展示了人类引导 AI 智能体探索数学思路的具体流程，并与同等 token 预算下未能解决问题的无引导尝试作了比较。