[Paper] 决策树的近似最优主动学习

Source: arXiv - 2512.03971v1

概览

本文提出了一种 符号主动学习框架，用于仅通过成员查询（即“给定输入的输出是什么？”）来重构未知的二叉决策树。通过将有界深度树的全部空间表示为 SAT 公式，并利用 近似模型计数，作者能够在不枚举每棵候选树的情况下挑选近似最优的查询。该学习器能够在极少的查询次数下收敛到正确的树，同时仍提供适用于验证密集领域的形式化保证。

关键贡献

• 基于 SAT 的假设空间编码：所有深度不超过给定值的决策树被紧凑地捕获在 CNF 公式中，避免显式枚举。
• 通过近似模型计数进行查询选择：使用 ApproxMC 估计每个潜在查询会将版本空间压缩多少，从而实现近似最优、信息论意义上的查询选择。
• 增量式版本空间细化：每次查询后，将观测到的结果加入 CNF，使表示保持最新而无需从头重建。
• 功能等价回退：当 ApproxMC 不再产生进展时，基于 SAT 的等价性检查确认剩余假设是否在功能上相同，从而提前终止。
• 实验验证：在合成数据集和基准决策树数据集上的实验表明，仅需少量查询即可收敛，优于基于启发式的主动学习方法。

方法论

1. 符号假设编码

   • 学习器固定一个最大深度 d。
   • 每个内部节点由布尔变量表示，指明它测试的特征以及取哪条子分支。
   • 所有可行树的集合形成一个 CNF 公式 Φ，该公式仅在满足当前观测的树上可满足。

2. 查询候选生成

   • 对于每个可能的输入向量 x（或其抽样子集），学习器创建两个 条件 公式：一个假设答案为 0，另一个假设答案为 1。

3. 近似模型计数

   • ApproxMC 估计在每种假设下 Φ 的满足赋值数量。
   • 对 x 提问的 信息增益 通过计数的减少来近似，例如 |Φ| - max(|Φ ∧ answer=0|, |Φ ∧ answer=1|)。

4. 查询选择

   • 选取估计增益最高的输入向未知树（oracle）发起查询。

5. 版本空间更新

   • 将观测到的答案对应的子句与 CNF Φ 合取，缩小可接受树的空间。

6. 等价性检查（回退）

   • 若 ApproxMC 连续多步报告相同的计数，SAT 求解器检查所有剩余模型是否计算相同的布尔函数。若相同，即使仍有多棵语法不同的树，学习也停止。

该循环持续进行，直至版本空间收缩至单一功能模型。

结果与发现

实验表明 近似计数是真实信息增益的可靠代理，能够在不出现组合爆炸的情况下实现近似最优的查询策略。

实际意义

• 安全审计中的模型提取——攻击者（或审计者）可以用最少的探测次数重构专有的决策树分类器，适用于对黑盒模型进行逆向工程，同时仍能提供关于提取过程的形式化保证。
• 软件验证中的测试用例生成——当组件的行为可表示为有界深度决策树时，该方法能够自动合成最小化的输入集合，完整刻画其逻辑，加速回归测试和形式化证明的生成。
• 交互式调试工具——IDE 插件可以向开发者提出有针对性的 “如果‑怎么办” 问题，以定位导致 bug 的具体决策规则，减少手动测试次数。
• 资源受限的主动学习——在 IoT 或边缘场景中，每一次查询都伴随成本（如传感器读取、网络往返），该方法确保每次查询都最大化不确定性的降低，延长电池寿命和带宽使用。

由于核心引擎仅是 SAT 求解器加近似计数器，技术可以 直接嵌入现有验证流水线（如使用 Z3、MiniSat、ApproxMC），无需重新实现自定义学习代码。

局限性与未来工作

• 对深树的可扩展性：CNF 大小随深度呈指数增长；虽然 ApproxMC 缓解了枚举压力，但深度 > 7 的树会导致内存紧张。
• 特征空间假设：方法假设特征集合是有限且离散的布尔型。若要处理数值或类别属性，需要额外的编码技巧（例如二值化）。
• 对 ApproxMC 保证的依赖：近似计数引入概率误差界限；在极端情况下，查询选择可能并非最优。
• 作者提出的未来方向 包括 (1) 将 SAT 编码与基于梯度的学习器相结合的混合符号‑统计模型，以处理混合类型数据。