AGENTOS_POSITIONING.md 8.6 KB
LambdaAgentPaaS 与 AgentOS：定位思路与投稿策略
状态：思路草稿（2026-06-09） 作者：Kenny + Claude 用途：把"lambdagentpaas 能否对 AgentOS 概念做贡献"这条线的分析、楔子、会议优劣势与推荐沉淀下来，作为后续起草 positioning paper 的依据。
0. 一句话结论
我们有一个别人很难复制的差异化切口：用形式化的 agent 资源语义（graded cost + effect system）作为 AgentOS 的"内核抽象层"。 推荐打法：vision 短文先插旗（用现有家底），OOPSLA 全文做旗舰（补 cost-soundness 机械化证明）。不要现在投系统会议（系统没建）或 ML 主 track（强项错配）。
1. "AgentOS" 现在到底指什么
这个词当前有三股力量在用，内涵不同：
- LLM-as-kernel 派（学术，代表 AIOS / Rutgers）：把 LLM 推理当成稀缺的 CPU 资源，做 OS 式的调度器 / 上下文管理器 / 内存管理器 / 工具管理器，核心是多 agent 并发复用一个推理内核。
- 虚拟内存派（MemGPT / Letta）：把"上下文窗口 = 物理内存、外部存储 = 磁盘"，做 context paging。
- 基础设施派（各家创业公司营销）：把编排 + 工具注册 + 记忆 + 可观测 + 部署打包叫"AgentOS"。
三派共同短板：全是系统工程，没有一个有"agent 到底是什么、消耗什么、能碰什么"的严格语义模型。这正是 lambdagentpaas 的机会。
2. 我们的资产恰好是 OS 抽象层
把已有的东西按 OS 概念对一遍，对得出奇地整齐：
| 操作系统抽象 | lambdagentpaas 已有对应物 | 实现位置 |
|---|---|---|
| 进程（what runs） | 类型化 agent term（11 构造，Paper I） | lambdagent/core.py（Term、Context） |
| 系统调用 / 受控访问 | effect system（pure/llm/io/state + 串并迭代算子） | lambdagent/effects.py；infer_effect_for_term |
| 进程隔离 | L1 sandbox（资源限额）+ git worktree | lambdagent/sandbox.py、isolation.py |
| 内存 / 状态管理 | instance 机制（template vs data）+ run workspace | agentpaas/engine/instance.py、engine/sandbox.py |
| 调度 / 配额 / 计费 | graded cost 语义 + cost 向量（预测 + 实测交叉验证） | lambdagent/cost_grade.py、cek_machine.py、validate_cost |
| 保护环 / 权限 | effect-as-capability + 风险分级网关 | lambdagent/tool_gateway.py |
| 进程间通信（IPC） | 多 agent / Par / Handoff / Send-Receive | effect 推断已覆盖（DESIGN-07） |
| 编译器优化 | 6 条代数律（可证明的语义保持变换） | Paper II / theory.md |
最强的一张牌是 graded cost 语义。 AgentOS 要做调度和计费，而几乎所有现有方案只能事后测量资源消耗。我们把 cost 写进操作语义（CEK + graded type），能在运行前预测一个 agent term 的资源上界。这在 OS 语境里就是 admission control / 截止期调度 / QoS 的形式化基础——别人没有。
3. 楔子（the wedge）
形式化的、cost-graded、effect-typed 的操作语义，作为 AgentOS 内核的调度与保护基底。
三条支撑论点，每条都有实现背书：
- effect system = agent 系统调用 / capability 安全的形式化
effects.py的 effect 代数（pure ≤ state ≤ io ≤ llm，串·/ 并∥/ 迭代^n），对应 OS 的 syscall 接口与保护环。 - graded cost = OS 资源核算与调度的形式化（预测优于事后测量）
cost_grade.py的CostGrade = (p, p_fatal, t, l, m)与组合规则（serial/parallel/loop/guard），加上validate_cost的预测 vs 实测交叉验证（DESIGN-08）。 - algebraic laws = 运行时可证明安全的程序变换（fuse / 并行化 / 缓存） Paper II 的 6 条代数律 + Prop 30（Pair 合流）。
三件套优势：理论（三篇论文）+ 运行时（CEK 机 10K+ LOC）+ 可部署服务（agentpaas）。这是 AgentOS 领域最稀缺的组合——多数工作只有其中一项。
实证家底：
- 2,225 个 YAML 配置爬取，881 解析，835 通过 lint（26 条规则 L001–L026）。
- 核心内核 175 测试通过；2026-06-05 审计结论：kernel"经得住审视"。
4. 诚实的差距（决定能投哪、不能投哪）
两个硬约束：
- 证明还停在 markdown：定理（type safety、adequacy、bounded termination、cost monotonicity、cost soundness）以 markdown 形式陈述，无机器验证（Coq/Rocq/Agda）。cost soundness（实测 ≤ 预测上界）尤其缺一个对 LLM 不确定性建模的真正语义模型。
- 系统层并发还是坏的：审计发现
Par分支共享 Context、单 SQLite 连接check_same_thread=False、模块全局 shell CWD 被并发改写。没有真正的 LLM-kernel 调度器、无多租户硬化、无 L2 容器隔离。
→ 这意味着：PL 路线要补证明，系统路线要先把系统建出来。
5. 四个会议方向 × 优劣势
| 会议方向 | 它要什么 | 我们的强项 | 我们的硬伤 | 现在可投性 |
|---|---|---|---|---|
| PL/语义 POPL/OOPSLA | 严谨元理论，最好机器验证；要讲清与 graded type / 资源分析（AARA、Granule）的 delta | 类型 + effect + graded cost 正是 PL 热点；LLM-as-oracle、cost 上界可证、6 代数律、CEK——题材新且深 | 定理只在 markdown；cost soundness 缺真语义模型 + LLM 不确定性建模；无机械化 | 6–12 月硬化后可投，护城河最深 |
| 系统 OSDI/SOSP/EuroSys | 真 workload、吞吐/延迟实测、对比 AIOS、规模化并发 | AgentOS 叙事正当口；agentpaas 真能部署；cost 预测 → admission control 是地道系统贡献 | 系统本身还没建：并发有 bug、无调度器、无 LLM-kernel 复用、无多租户；形式化在这里反被当过度设计 | 现在不行，最差的时间点 |
| Agent/ML NeurIPS/ICLR/workshop | 主 track 要 SOTA 或强实证；社区大、快 | cost 预测精度可实测；835 配置语料；安全护栏可演示 | 主 track 把"形式化"当非 ML，易被误读"benchmark 呢"；理论价值被低估 | workshop 现在可投；主 track 错配 |
| Vision/Workshop 短文 HotOS 等 | 挑衅性 idea + 立场，不要求完整 eval | 现有家底足够立 claim；HotOS 正是系统界 vision 场，爱"agent 需要形式化内核"这种命题 | 引用/份量低于全文；只是插旗不是定论 | 立刻可投，性价比最高 |
6. 推荐：两步走
第一步（现在，3–6 周）——HotOS 风格 vision 短文，插旗
- 暂定标题："An AgentOS Needs a Formal Kernel: Cost-Graded, Effect-Typed Semantics as the Scheduling Substrate"
- 为什么：今天就有的东西（三篇理论 + 真实现 + 835 实证）刚好够撑 4–6 页 vision，不需要机械化证明、不需要 perf eval。
- 战略价值：在"formally-grounded AgentOS kernel"楔子被别人占之前抢下 priority；HotOS 是系统社区，正好把形式化卖给最需要被说服的人群。
第二步（主攻，6–12 月）——OOPSLA 全文，旗舰
- 为什么是 OOPSLA 而非 POPL：OOPSLA 接受"形式化 + 真实现 + 实证"三件套，而我们三样都有；POPL 纯理论门槛会逼我们去做现在没有的纯元理论。
- 必补的关键一件：把 cost soundness 定理（actual ≤ predicted upper bound）做成有真语义模型、最好机械化的核心结果——这是从"工程文档里的定理"升级为"PL 会议级贡献"的分水岭，也是审稿人必戳之处。
明确不做（现在）
- 系统会议：系统没建，投了就是送。
- ML 主 track：强项错配。
- 备选第三战场：ML/agent workshop，专打 cost 预测精度实证。
7. 下一步 TODO
- 起草 vision 短文 outline + core claims（用
theory.md/cost_grade.py/cek_machine.py做实证支撑） - 列 OOPSLA 全文 claim 骨架，与 vision 对照
- 调研 AgentOS / AIOS / Letta 当前 landscape，确认楔子未被占（deep-research）
- 评估 cost-soundness 定理机械化的工作量（Coq/Rocq vs 纸面严格证明）
- （并行）修系统层并发 bug——为未来系统会议路线铺路
8. 相关材料索引
- 理论三篇：
docs/theory.md、docs/research/THEORY.md - cost 预测解释：
docs/cost-prediction-explained.md - 研究方向总结：
04-Projects/Lambdagent研究方向总结.md - 安全规范 / 审计：
lambdagent/SECURITYSPEC.md、docs/AUDIT_2026-06-05.md - 核心实现：
lambdagent/src/lambdagent/{core,effects,cost_grade,cek_machine}.py、fromconfig/{compiler,lint}.py