附件给了一个"字符级语言模型" ICTFForCausalLM + 权重目录 ictf_model/，
输入 ≤16 个字符，输出 1 个预测字符。要求"找出隐藏在模型中的秘密，恢复 flag"。

tokenizer 的字符表是 0-9a-zA-Z（62 个），另外两个特殊 id：

目标很明确：构造输入让模型吐出 <success>。

读 model_def.py 的 forward：

没有 embedding、没有 attention、没有位置编码 —— 就是个两层 MLP，
而且输入是 token id 的数值本身。整个"模型"是一个 16 变量的确定性函数：

config.json 里 hidden_size=21 这种数字也不像训练出来的模型（21 不是 2 的幂，
也不是任何常见宽度），提示这 21 个隐藏单元是手工设计的。

本机没装 torch，但 safetensors 格式就是 8 字节长度 + JSON header + 裸 float32，
手工解析即可（见 dump.py）。第一眼就看出异常：

lm_head 稀疏到这个程度，绝不是训练产物。逐行打印：

也就是说，整个 64 维 logits 里只有一维是变量：

其余 63 维是常数。所谓"预测下一个字符"其实是：out62 能不能超过 0.4。
这不是模型，是一个套着 PreTrainedModel 外壳的校验函数。

argmax == 62 ⟺ out62 > 0.4，拆成两条：

（1）h1..h20 必须全部被 ReLU 归零

即 20 条线性不等式 W1[i]·x + b1[i] ≤ 0（i=1..20）。

这里有个能省掉浮点讨论的观察：W1[1..20] 的系数和 b1[1..20] 全是整数
（值域 -100..100，bias 是四位整数），而 x 也是整数，所以每个 pre-activation
要么 ≤0，要么 ≥1。一旦某个 h_i ≥ 1，就会给 out62 带来 -1e10 的惩罚；
而 h0 的理论上界只有 Σ(正系数)·61 ≈ 1.5e6，差了四个数量级，永远补不回来。
所以约束是硬的，不存在"某个 h 稍微为正但被 h0 补偿"的边缘解。

（2）h0 要足够大

W1[0] 那一行系数明显比其它行大一个量级（3012、5574、-3472…），就是专门当"得分行"用的。

至此题目完全变成：16 个整数变量 ∈ [0,61]，21 条线性不等式，求解。
没有非线性、没有黑盒，直接扔给 z3。

冰与火的战歌：Windows内核攻防实战高级班！从零到实战，融合AI与Windows内核攻防全技术栈，打造具备自动化能力的内核开发高手。