思考、笔记与记录
AgentMoss 跨平台 Hook 适配
完成了 AgentMoss v1.2.1 的跨平台 Hook 监控适配，支持 OpenClaw、xiaoO、HERMES、JiuwenClaw 四个平台的 hook 对接。三层行为图建模（CFG/DFG/PDG）的基础结构已经稳定，61 条威胁检测规则覆盖了数据泄露、凭证窃取、命令注入等 11 个类别。 核心挑战在于不...
博客文学板块上线
新开了文学板块，把公众号的 40 篇文章全部迁移到了博客。技术上复用了 posts 的数据类型和渲染逻辑，新增了 literatureDirectory 和 getAllLiterature 函数，路由结构保持 /literature/[slug] 的一致性。 比较有意思的一点是 TypeScript 里 slugRe...
GEPA 论文准备发布
在准备发布 GEPA 论文的解读（arXiv 2507.19457，ICLR 2026 Oral）。这篇关于 Graph-based Execution Plan Agent 的工作提供了一个新的视角：用图结构来组织 Agent 的执行计划，而不是传统的线性链式调用。 正在考虑用什么方式呈现架构图——matplotli...
Agentic Design Patterns 翻译进展
《Agentic Design Patterns》的翻译工作持续推进，目前已完成大部分章节。翻译策略上采用了多子 agent 并行处理，每个 agent 负责 1-3 个章节，避免了上下文截断的问题。 一个经验：pdfplumber 提取 PDF 的质量远优于 pypdf——后者在单词间会产生多余空格，段落也容易断裂。...
概率神经符号系统的可扩展鲁棒性验证：松弛近似的胜利
A Scalable Approach to Probabilistic Neuro-Symbolic Robustness Verification
Manginas 等人给出了概率神经符号系统鲁棒性验证的首个松弛近似框架。核心发现：精确求解 E-WMC 决策问题是 NP^PP-完备，因此只能通过编译整个 NeSy 系统为可微计算图，再借用 autoLiRPA 等 NN 验证器做区间传播。实验显示该方法比 Marabou 快数个数量级，并在 ROAD-R 自动驾驶数据集上验证了 6 层 CNN 组合的安全属性。
鲁棒多智能体系统验证：当系统参数不可信时，联盟策略还能信几分？
Verification of Robust Multi-Agent Systems
AAMAS 2026 论文。RWTH Aachen Katoen 团队研究不确定随机多智能体系统的鲁棒策略验证，提出三种扰动语义（ε-扰动 / 固定参数 / 无界参数）下 PATL 鲁棒模型检测的复杂度刻画：在部分观测、有限自动机记忆、对抗 Agent 三重困难下，鲁棒验证仍然可判定，从 P 到 Σ_3^R 阶梯分布，精准刻画了『不确定性表达力 ↔ 计算代价』的内在张力。
Lean4Agent：用依赖类型形式语言建模与验证 Agent 工作流
Lean4Agent: Formal Modeling and Verification for Agent Workflow and Trajectory
UIUC 团队提出首个使用 Lean4 依赖类型形式语言统一建模和验证 LLM Agent 工作流与执行轨迹的框架。三层验证库 FormalAgentLib（151 类型、611 函数、41 定理）配合 LeanEvolve 工作流演化，在 SWE-Bench 和 ELAIP-Bench 上验证通过的工作流平均优于失败的 11.94%，LeanEvolve 额外提升 7.47%。
