CMU 提出 LLM2Cert：LLM 生成证书，SMT/Lean 自动验证
CarnegieMellonU · hf · 2026-10-27
卡内基梅隆大学的 LLM2Cert 框架让 LLM 为非线性动力系统合成稳定性与安全性证书（Lyapunov 函数、Barrier 函数、策略），再经 SMT 求解器与 Lean 证明修复 agent 自动验证。流程包含提案 agent、快速筛查、SMT/Lean 路由与失败重试，最终给出稳定性、ROA、不变性与安全性的认证保证；作者同时发布了非线性动力系统 benchmark，验证成功率显著提升。
「研究」频道最新
- DONIC 双手机器人追踪成功率 86.79%，远超此前 SOTA 的 9.43% — liuziwei7 · 2026-10-27
- 研究者吐槽:论文里 PSNR 低于 15dB 基本是用错了指标 — kwangmoo_yi · 2026-10-27
- Ortet 首批医疗评测:34 个开源模型 50 项任务,通用排名不够用 — thegautamkamath · 2026-10-27
- Scaling 拟合之争:Uncheatable 计入输出头 FLOPs,Paloma 剔除,最小档差距高达 65% — dlwh · 2026-10-27
- Marin 作者详解 scaling law 公式：难点在小模型阶段估渐近线 — dlwh · 2026-10-27
- Marin 开源 scaling law 外推 300 倍，预测大模型 loss 误差仅 0.2% — dlwh · 2026-10-27