PROPOSAL_SKILL_HARMONYOS.md 14 KB

投标技术方案:面向开源鸿蒙的 Skill 可迁移性评估与自动适配框架

对应课题:技术课题2 — 开源 Skill 迁移适配开源鸿蒙,支撑 Skill 生态繁荣 投标方技术底座:lambdagentpaas(λA 类型化 Lambda 演算 Agent 引擎,BSL 开源) 状态:草案 v0.1(待团队/评审定稿) 技术附录:SKILL_FORMALIZATION_DESIGN.mdharmonyos-agent-dsl-comparison.mdMCP_SKILL_DESIGN.mdPRODUCT_GATE_DESIGN.md


0. 一句话方案

把开源 Skill 迁移从「逐个人工评测 + 经验改写」升级为一条形式化全链路SkillBench(可判定评估)→ Skill IR(纯函数抽象)→ Migration Harness(自动迁移)→ Formal Guard(静态安全封顶)。 其中可判定的部分(依赖/能力/类型缺口)由形式化方法可证正确地给出适配报告,模糊的部分(脚本归约、行为改写)由 Coding Agent + 验收闭环把准确率抬到 95%+。


1. 课题理解与定位

1.1 课题诉求拆解

课题2 的两条核心技术诉求:

  • 诉求①(评估):构建开源 Skill 能力评估能力,涵盖功能、质量、安全性、开源鸿蒙系统适配性,自动化分析并输出适配报告,分析准确率 95%+
  • 诉求②(抽象+迁移):构建 Skill 抽象能力,解耦核心逻辑、提取"纯函数"、消减对系统/Agent 框架的依赖,让高质量 Skill 跨系统/语言/环境执行;并针对 Skill 迁移构建一套 Harness 框架,开源 Skill → 开源鸿蒙迁移准确率 95%+

1.2 我们的定位(收窄)

不做泛泛的"生态繁荣",聚焦一件硬事:

面向开源鸿蒙的 Skill 可迁移性评估与自动适配框架

差异化主张一句话:

现有工作(SkillsBench[2])回答"这个 Skill 在鸿蒙上跑得通吗"——实证、事后、pass/fail;我们回答"为什么通/不通、缺哪条能力、怎么补"——形式、事前、可证。

这正填补课题2 自身承认的缺口:"关注功能和质量,但缺少对可靠性、可迁移性的评估"。


2. 技术背景与痛点

  • 量大质杂:社区 Skill 已达万级,重复率高、部分功能冲突,缺一套科学的质量评估框架。
  • 迁移率低:对 OpenClaw Top60 Skill 分析,仅 26%(16/60)可无痛迁移(课题2 现状数据)。其余分属 A1–A4(鸿蒙环境/设备依赖)、B1–B4(网络/凭据/系统能力/质量缺陷)。
  • 安全合规:开源 Skill 存在大量安全、隐私、合规风险,需可量化、可定性评估(prompt 注入、越权工具调用、凭据外泄等)。
  • 方法待立:业界当前路线是把 Skill 转 MCP 服务、或封装 SubAgent A2A 调用、或完全重写,缺统一的中间表示与自动判定——每条都靠人工经验,无法规模化到万级。

3. 总体方案:四层形式化全链路

解决课题2 核心机制 已有底座
① SkillBench(评估) 诉求①:适配报告 95%+ 自动派生 Skill 的效果/成本/类型契约;portable(s,device) 可判定判定 + 缺口报告;注入扫描 infer_effect_for_term / estimate_cost / is_subtype / scan_injection
② Skill IR(抽象) 诉求②:提取纯函数、去框架依赖 Skill : Term→Term 注入组合子 + interface: 运行时无关契约;脚本型 normalize 成 Tool/Compose Skill 形式化设计 §3/§4/§7.3
③ Migration Harness(迁移) 挑战:"用 Coding Agent 快速迁移" native coding-agent 车道做改写 + IR→鸿蒙 DSL/MCP/SubAgent 多目标 codegen + 行为一致性测试 native claude-code 执行车道 + worktree 隔离 + §6 鸿蒙映射
④ Formal Guard(安全) 安全/隐私/合规 Guard(输出验收)+ Restrict(效果封顶,伽罗瓦连接)+ 工作目录硬沙箱 extensions.py::Guard + Skill 形式化 §3.5 + _sandbox.py

四层关系:评估层判定可迁移性 → 抽象层把 Skill 提成 IR → 迁移层 codegen 到鸿蒙目标形态 → 安全层在工具调用层静态封顶能力。评估与抽象共用同一套形式契约(effect/cost/type),这是全链路自洽的关键。


4. 核心技术点

4.1 SkillBench:可判定的 Skill 迁移评估器

输入一个开源 Skill,输出适配报告(功能/依赖/权限/安全/鸿蒙适配难度 + 迁移路径建议)。

关键:把课题2 那张"A1–C 人工分类表"变成自动可判定的效果/工具/验收条件——

课题2 分类 本质 形式判定(自动)
A1 macOS/特定 Linux 依赖 环境依赖 tools_s ⊄ tools_device(端侧无此原生工具)
A2/A3 无依赖工具(虚机可/不可解) 工具可替代性 工具面取交后能否经 MCP 回退(降级策略 §6.3)
A4 app/软件依赖 外部进程 effect = io(外部桥接型)
B1 网络服务不可用 网络 io effect_ceiling 砍 io → 判不可迁移
B2 需 API Keys/Credentials STATE/密钥 STATE(state_keys) 效果 + 凭据缺失
B3 系统能力暂不支持 效果超端侧上界 effect_leq(ε_s, ε_device) 为假
B4 Skill 不正确/配置/格式 质量缺陷 validate_skill + Guard 验收失败
C 兼容 全满足 portable(s,device) 为真

可判定性判定(编译期):

portable(s, device) ⟺
    effect_leq(ε_s, ε_device_max)      -- 效果不超端侧允许
  ∧ tools_s ⊆ tools_device              -- 所需工具端侧都有实现
  ∧ grade_leq(g_s, g_device_budget)     -- 成本(token/延迟)不超端侧预算

任一条不满足 → 报告具体缺口 + 降级建议(工具缺失→云端 MCP 回退;成本超→换小模型+收紧重试;效果超→人工裁剪),而非端侧运行时炸。

安全评估:复用 scan_injection(prompt 注入模式扫描,已上线)+ Restrict 效果封顶(越权工具调用静态拦截)+ 高风险工具权限 diff,输出安全/隐私/合规子报告。

4.2 Skill IR:核心逻辑抽象与"纯函数"提取

把 Skill 抽象成运行时无关的 term + 契约,这就是课题2 要的"解耦、提取纯函数、去框架依赖":

  • 注入型 Skill → 组合子 Skill_s(A) ≜ Guard(Memory(A ⊕ prompt ⊕ tools), P_s),携带 interface: 契约(输入/输出类型、效果上界、验收谓词、成本先验)。契约是运行时无关的,可重定向到任意目标运行时。
  • 约束型 Skill → 对偶组合子 Restrict_r(A)(效果取下确界、工具面取交、调用守卫),覆盖 careful/freeze/guard 这类安全 Skill。SkillRestrict 在效果格上构成伽罗瓦连接,使 Skill 最终能力被可证地夹在 [下界, 上界]
  • 脚本型 Skill(OpenClaw/Claude SKILL.md + scripts) → normalize:frontmatter→元数据、正文→prompt、脚本调用→Tool/MCP scope、workflow 步骤→Compose(带验收则每步 Guard)。由此脚本型也获得 interface: 契约,进入统一 IR。

"纯函数"提取的形式含义:把一个 Skill 的副作用(IO/STATE)显式标注为 effect,把其确定性核心逻辑提成 Tool/Compose 的纯结构。effect 标注让"哪些依赖能去掉、哪些必须保留"成为可计算问题。

4.3 Migration Harness:自动迁移与一致性验证

  • 改写引擎:复用 native claude-code 执行车道(直接调 claude -p --output-format stream-json,native 工具开、worktree 隔离并行改写互不冲突),把不可直接迁移的 Skill 自动改写成可迁移形态。
  • 多目标 codegen:IR → 鸿蒙 Agent DSL(CangjieMagic @agent/@prompt[pattern]/@tool)/ MCP 服务 / SubAgent A2A,三选一(对应课题2 业界三路线)。映射规则见 harmonyos-agent-dsl-comparison.md 与形式化设计 §6。
  • 行为一致性测试:迁移前后用同一组测试任务跑,Guard 验收输出契约一致(pass/fail),作为迁移正确性证据。

4.4 Formal Guard:静态安全封顶

把安全从"输出验收"推进到"工具调用层的静态能力封顶":

  • Guardextensions.py:146):输出必须满足谓词,否则重试/失败。
  • Restrict(形式化设计 §3.5):effect_meet 砍效果上界、工具面取交、deny_patterns 调用守卫(ask/deny),对应迁移后 Skill 在端侧的最小权限运行。
  • 工作目录硬沙箱(_sandbox.py,已上线):越界写直接拒绝,防迁移 Skill 在端侧逃逸。

安全代数结论:迁移后 Skill 的能力 ε_final 被可证地夹在 [Restrict 下界, Skill 上界]——这是相对纯 prompt 工程最硬的安全卖点,也直接回应课题2 的安全/隐私/合规诉求。


5. 与现有工作的差异化

课题2 引用了两篇关键文献:Agent skills 数据驱动分析[1] 与 SkillsBench[2]。我们不重造它们的实证基准,而是补上它们没有的形式化层:

维度 Agent skills[1] / SkillsBench[2] 本方案
评估方法 实证、跑 trajectory 统计 pass/fail 形式、编译期可判定
输出 成功率数字 缺口定位 + 迁移路径 + 可证安全边界
可迁移性 实测能不能跑 为什么、缺什么、怎么补
抽象层 无统一 IR Skill/Restrict term + interface: 契约 IR
安全 基本不覆盖 效果封顶 + 伽罗瓦连接 + 硬沙箱
理论根基 经验/数据 λA 类型化 Lambda 演算(三篇论文)

一句话:SkillsBench 是"考试",我们是"诊断 + 处方 + 手术"。


6. 95% 准确率的可信拆解

把课题2 要求的两个 95% 拆开讲,避免一刀切吹:

部分 占比(按 Top60 估) 准确率来源 风险
可判定类(A1–B3、C) 多数 effect/工具/类型判定可证正确,趋近 100% 低(形式化送的红利)
质量缺陷类(B4) 少数 validate_skill + LLM-judge 验收 中(judge 阈值需调)
脚本归约 + 行为改写(迁移核心难点) 关键少数 Coding Agent + Guard 验收闭环 高(是工程主战场,从 ~70% 抬到 95%)

结论:评估侧(诉求①)的 95% 主要靠可判定红利,可达;迁移侧(诉求②)的 95% 是真正要堆工程的地方,靠 Harness 的"改写→验收→重试"闭环逼近,这也是课题"挑战"二字的落点。这样拆,评审能看出我们知道难在哪。


7. 里程碑与交付

阶段 周期 交付物 验收指标
M1 评估器 MVP T+2 月 SkillBench:单 Skill → 适配报告(A1–C 自动分类 + 缺口) 对 Top60 复现人工分类,一致率 ≥90%
M2 Skill IR T+4 月 Skill/Restrict 组合子 + interface: 解析 + 脚本 normalize 内置/OpenClaw 样例 Skill 提成 IR,回归通过
M3 迁移 Harness T+6 月 IR→鸿蒙 DSL/MCP/SubAgent codegen + 一致性测试 可迁移 Skill 自动迁移 + 行为一致 ≥90%
M4 全链路 + 指标冲刺 T+9 月 端到端:开源 Skill 批量评估+迁移+验证 评估准确率 95%+、迁移准确率 95%+(挑战值)

每阶段产出可复现实验 + 报告,对齐课题验收。


8. 可复用资产清单(证明不是从零起步)

资产 现状 对应层
λA 类型化 Lambda 演算引擎(term/effect/cost/type/Guard) 已实现,175+ 测试 ①②④
infer_effect_for_term / estimate_cost / validate_cost 已实现
Skill 注册中心 + mount_into_config + scan_injection + 权限 diff 已上线 ①②
Skill 形式化设计(Skill/Restrict/interface:/鸿蒙映射) 设计完成(本文档技术附录) ②③
native claude-code 执行车道 + worktree 隔离 已上线
鸿蒙 Agent DSL / CangjieMagic 对比文档 已完成
工作目录硬沙箱 _sandbox.py 已上线
产物 Gate 流水线(gate=Guard、LLM-judge) 已实现,39 测试 ①④
MCP / A2A / AgentPack 接入 已上线 ②③

即:四层中每一层都有可演示的存量代码或设计,投标不是 PPT 概念,而是已有工程的形式化收口。


9. 风险与应对

风险 等级 应对
脚本型 Skill 行为改写准确率达不到 95% M3 起以 Guard 验收闭环驱动迭代;对低置信迁移标"需人工复核",不强迁
开源鸿蒙 / CangjieMagic 端侧运行时接口变动 IR 运行时无关,codegen 后端可替换;先对齐稳定子集
effect/工具白名单与真实端侧能力清单不一致 端侧能力清单 Caps_device 作为可配置输入,随版本更新
LLM-judge 评估阈值漂移 复用 PRODUCT_GATE 的 judge 框架,阈值可调 + 本地 ollama 兜底
CJK token 估算低估致成本判定偏松 已知问题,cost_hint + validate_cost 回填校准

10. 参考文献

  • [1] Ling G, Zhong S, Huang R. Agent skills: A data-driven analysis of claude skills for extending large language model functionality. arXiv:2602.08004, 2026.
  • [2] Xiangyi L, Wenbo C, et al. SkillsBench: Benchmarking How Well Agent Skills Work Across Diverse Tasks. arXiv:2602.12670, 2026.
  • 本方技术附录:SKILL_FORMALIZATION_DESIGN.mdSkill : Term→Term 语义、interface: 扩展、鸿蒙契约映射)。
  • λA 三篇论文(类型系统 / 效果与代价 / 算法律),见项目 docs/research。