LLM2Cert：用大模型合成稳定性与安全证书并由SMT或Lean核验
LLM2Cert用大模型合成稳定性与安全性证书，再交SMT求解器或Lean证明修复代理核验。配套基准DynaCertBench含105个实例，覆盖高维与非线性系统。报告验证81例、成功率77.1%，较无反馈一次性提案提升17.1个百分点，并解决All-SMT未决的22例。价格与国内可用性未知。
要点
- DynaCertBench含105个实例，包括文献中80个非冗余系统，以及高维、控制约束和非线性耦合变体。
- LLM2Cert先合成候选证书，再把证明义务交给SMT求解器或Lean证明修复代理，105例中验证81例。
- 相比无反馈的一次性提案提升17.1个百分点，并验证了22个All-SMT未能解决的已固定证书。
为什么值得看
李雅普诺夫函数和障碍证书能为稳定性与安全性提供状态空间保证，但非线性、高维系统的合成与验证仍困难；现有数值、区间和SMT流程常需松弛、偏保守或难以扩展，基准也多偏向低维多项式系统。
谁会受影响
面向控制系统、形式化验证和大模型研究者，以及需要稳定性、吸引域、前向不变性或安全证书的工程师。
今天就能怎么试
摘要称代码与数据已公开，但未给出可核验的具体地址、安装步骤和运行参数；价格与国内可用性未知，本文未实测。
原始来源
1LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification · arXiv cs.AI · 2026年10月23日✓ 已打开核对本条由 AI 根据上面的原始来源整理，经编辑审核后发布。数字和结论以原文为准，发现错误欢迎反馈。
相关动态
开放世界模型结合游戏引擎，单卡生成实时可玩画面
Matrix-Game 4.0 让轻量引擎负责规则和状态，视频模型将低多边形画面转成细致视觉，编码智能体则修改场景与玩法。论文报告 RTX 5090 上实现 480p、60 帧交互，按键到显示延迟为 112 毫秒，并宣布开放代码与资产。实时帧率需与响应延迟分开看。
业务智能体基准检查执行过程，完成任务也可能判失败
BizAgentBench 将 789 份知识文档、601 项业务工具和 50 个长流程任务放进可执行环境，既核验最终目标，也检查中间步骤约束。论文显示只看任务完成会掩盖无效操作；HF 早期标题为 BizBench，arXiv 修订版已改名。同时还应记录任务过程中的工具调用成本。
中英密集文字生图基准发布，专测海报长文与布局
UltraText Bench 提供 432 条人工检查的提示，覆盖 24 类真实场景，中英文各半，每张图要求四至十二处文字。评估分别看文字准确、清晰度、空间安排和场景质量，揭示快速模型可能更清晰却更容易写错字的取舍。适合中文海报选型。
AI协助发现PHP高危漏洞，网站维护者面临集中修补
爱范儿梳理 PHP2Shell 漏洞披露与紧急修补过程，介绍 OpenAI 安全研究在构造可复现证据中的作用。事件涉及底层软件广泛使用带来的连锁影响；具体风险取决于运行版本与部署条件，不能把使用 PHP 都等同于已经遭入侵。