研究
我做的是:怎么判断一个自动化系统交出来的东西可不可信——从 agent 的 harness 一路到它生成的 GPU kernel。
排序原则(写死):ML systems / GPU 验证 → LLM agent → reasoning → 多模态 & world model → 大规模系统 → 安全。
安全永远放最后。它是我的本科专业和入门路径,不是我要读博的方向。
ML systems 与 GPU kernel 验证
PhaseGuard
Hopper/Blackwell 上 TMA / tcgen05 等异步写存在现有 dynamic checker 观测不到、且 racecheck 万倍慢化会系统性关掉竞争窗口的 race;把执行主体 × 地址区域 × phase/计数状态 × 完成谓词代数抽成 phase-automaton,从源码静态提取后有界穷举判定。
边界 — 已冻结面:CUTLASS SM90/SM100 + FlashAttention-3。当前为 model-level SAFE / exact J_K REFUSED / source-level INCONCLUSIVE。没有总体误报率估计,没有七阶段 source-level safety theorem。正式导师评审仍待完善。
ProofWeaver
agent 已经能写出带 TMA、tensor-core async group、barrier phase、staged-buffer reuse 的 warp-specialized kernel,但 static validator / random test / Compute Sanitizer / agent 自评分都不能证明在所有合法 GPU 调度下安全。
边界 — refinement 只做到 functional-index leaf 和 bounded tensor-value(P,dP,D ∈ [-16,16] 全整数域),不是 whole-kernel equivalence;binary32 RZ/FTZ 对应关系仍是人工审计的 trusted lemma。
Chimera
按 MoE routing shape 自适应任务与通信粒度。
边界 — 没有性能数字。harness 可跑且已审计,但所有衡量都没开。
OppEval
机会式求值,PL × serving 的混合线。
边界 — 1,032 个阻塞时刻里 84.5% 有 ≥2 个外部调用在途(若以 4,973 个决策点为分母则是 96.8%);两个可从项计算的关键性谓词分别恒假、恒真 → 排序空间是真的,语言给不出用它的依据。
CASM (内部代号)
(内部项目,对外材料不出现)
LLM agent: memory / skill / harness
GuardPatch
可审计 memory:guarded delta patch + counterfactual reuse audit。
边界 — under review;不能写成「已发表」。
Skill2Mem
Probing skill-to-memory transfer in LLM agent memory。公共 skill 库什么时候反而有害。
边界 — under review / 高分;ACL commitment 时间线未核实,不写成已确定。
Skill Form Matters
trace / script / hierarchy / artifact 四种表示在 agent skill memory 中的影响。
边界 — p 区间 0.108–1.000,没有单一赢家。这条结论本身就是这篇论文的核心,藏起来反而让论文标题显得奇怪。
S2CRA
verifier-guided LLM proposal channels for auditable causal graph discovery。
边界 — 国创结项优秀已出(这是线 2 少数几个「已落地的正式结果」之一)。不投 EMNLP。
SkillMask
capability-conditional skill selection(历史名,已被新名吸收)。
DeltaMem
delta-style memory patching(已并入 GuardPatch)。
reasoning 与 credit assignment
多模态生成与 world model
RetargetHOI
视频物体替换里 intent preservation 与 interaction feasibility 的冲突。
边界 — 没有 preservation / feasibility / locality / intent 分数;没有 baseline tradeoff 结论。当前顶层状态 STOP_NO_C0_C2_COMPARISON / BLOCKED_REQUIRED_CALIBRATION_ROLES。绝不能写成「我们提出了一个方法并取得了效果」。
Active4DGS
强 4D 生成先验下经典 information gain 会不会反号。
ActBelief
主动感知策略。
边界 — 何时买证据比买哪个重要三十倍;6.6% 帧上的免费 ensemble 分歧门可回收 60–79% 的 oracle value;自己 11 条预注册预测被否证,含两个 learned component。
FUSE
多模态 post-training 的 forked utility 监督。
大规模系统与仿真基础设施
SEED Emulator
NSF 资助研究路由器仿真平台($1.3M),被 1,180 家机构使用;core maintainer 角色,主导 routing control-plane 与 AI/agent 两条线。从「人来操作」到「agent 可操作」:MCP server + deterministic agent benchmark。
边界 — 引用数两个口径不一致(ACM DL 12 / ResearchGate 21),不报引用数;网传「2026 年 SDN/DoS/ML-IDS 那篇用了 SEED」搜不到确证,不写进任何材料。
Multi-Kernel Execution
SEED Emulator 路由栈从单内核串行化扩展到多内核并行执行基座。
边界 — 不能说的:任何收敛改善的量化数字;「消除」(只是缓解)内核瓶颈;等价于真多物理机部署(实际是单台物理机上的 KVM + K3s)。
我一半的产出是证否自己的假设(Skill Form Matters p 区间 0.108–1.000、ActBelief 自己 11 条预注册预测被否证等)。这是方法论优势,藏起来反而让那批论文标题显得奇怪。
