本文只使用官方附件中的相对文件名，不涉及本机绝对路径、用户名或其他环境信息。

附件给出一个字符级「语言模型」ICTFForCausalLM 及其权重。

配套文件：

config.json：

参数量极小：16 → 21 → 64，总共一千多个参数。真正的前向在 model_def.py 里只有几行：

三个反常点：

分词器字符集：

共 62 个字符，id 为 0..61。输入不足 16 时用 pad_token_id = 0 右填充——而 id 0 恰好是字符 '0'。因此「短字符串」和「后面带 0 的 16 字符」在数值上无法区分。后文求解时按满 16 维整数向量处理即可。

inference.py 取 argmax，打印对应字符。本题要的是让 argmax 落到 id 62。

用 safetensors（或不装任何深度学习库，按文件头解析）读出四个张量：

记输入 (x \in {0,\dots,61}^{16})，前向为：

lm_head 一眼露馅：

普通字符和 <fail> 的 logit 不随输入变化：恒为 -10000 和 0.4。唯一会动的是第 62 行：

<success> 要胜过 <fail>，必须：

h[j] ≥ 0。h[1]…h[20] 前面挂着 -1e10：任何一个约束单元哪怕只激活一个很小的正数，logit[62] 都会掉到 -1e10 量级，不可能超过 0.4。

因此成功条件拆成两条：

条件 A（可行性） —— 第 1 到第 20 个隐藏单元必须被 ReLU 压成 0：

条件 B（阈值） —— 第 0 个单元必须够大。此时 h[0] = W_d[0] · x + b_d[0]（该值本身为正），代入：

W_d[0] 与 (x) 都是整数，点积必为整数，故：

整道题变成：在 (x_i \in {0,\dots,61}) 上解 20 条线性不等式，并让一条整数线性函数达到 64573。

dense.weight 全部是整数。第 0 行数量级是几千（目标函数），其余 20 行落在 (\pm 100)（约束）。dense.bias[1:] 也全部是整数。

这是典型的出题构造：

因此可以先把条件 A 当成等式 来解：

A 是 (20 \times 16)、秩 16 的超定系统。最小二乘残差约为 (0)（数值上 (10^{-12}) 量级），说明方程组相容，存在唯一实数解。把解四舍五入：

全部落在 0..61。按字符集映射：

得到候选口令：

代回检查：

余量只有 0.1。这不是训练出来的边界，是手工把 dense.bias[0] = 311558.71875 和 lm_head.bias[62] = -376131.21875 配出来的。

条件 A 写的是 ≤ 0 而不是 = 0，所以只凭等式求解，逻辑上还不能说「多面体里没有别的整点」。需要把条件 B 一起加上。

在整数格 (x_i \in {0,\dots,61}) 上，对

做约束求解（任意整数线性求解器即可，例如 Z3）。搜索结果表明：满足两条条件的整点只有上面这一组。

直观原因：

改一个字符的对照：

dense.weight 第 0 行与 bias：

约束行 (j=1..20)（整数）：

在 (x^\star) 上，上表每一行的点积都等于 (-b_d[j])。

只需 numpy。safetensors 文件是「8 字节头长度 + JSON + 裸 float32」，也可以只用标准库解析。

运行后打印：

在附件目录下（已按题目依赖安装 torch / transformers）：

提示 Enter your prompt: 时输入 f1ag2026c7fa1666，应输出：

等价的纯 numpy 前向（用于核对，不改官方脚本）：

本题不是语言模型，而是一台硬编码的整数约束检查器：

{
  "architectures": ["ICTFForCausalLM"],
  "hidden_size": 21,
  "max_position_embeddings": 16,
  "model_type": "ictf_causal_lm",
  "vocab_size": 64
}

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