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

Source: arXiv - 2512.03971v1

概述

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

关键贡献

• SAT‑based 编码的假设空间：所有深度不超过给定值的决策树都紧凑地表示为 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 求解器会检查所有剩余模型是否计算相同的布尔函数。若是，则即使仍存在多棵语法不同的树，学习也会停止。

该循环持续进行，直至版本空间收敛到唯一的功能模型。

Results & Findings

实际意义

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

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

限制与未来工作

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