一句话：提出对称决策树SDT及Horn-SDT方法，从对称样本学习对称不变式，加速参数化程序验证。
不变式合成是程序验证的基础问题，但现有学习方法很少利用参数化与并发程序固有的对称性。对称性诱导出对称可达状态空间与对称样本，并允许对称不变式，从而引出从对称样本学习对称不变式的问题。为此，论文提出对称决策树（SDT），一种在结构上强制对称性的新假设类，从构造上保证所学不变式对称；并给出构造SDT的学习算法，将其作为学习器集成到Horn-ICE框架，形成Horn-SDT。在参数化程序上的实验表明，与非对称基线相比，Horn-SDT收敛更快、生成的树更紧凑。
Invariant synthesis is a fundamental problem in program verification, yet existing learning-based approaches rarely exploit the inherent symmetry present in many programs, particularly parameterized and concurrent systems. Such symmetry induces a symmetric reachable state space, naturally yielding symmetric samples and admitting symmetric invariants, motivating the task of learning symmetric invariants from symmetric samples. To this end, we introduce symmetric decision trees (SDTs), a novel hypothesis class that enforces symmetry structurally, guaranteeing symmetric invariants by construction. Furthermore, we develop a learning algorithm to construct SDTs and integrate it as the learner within the Horn-ICE framework, yielding our approach, Horn-SDT. Empirical evaluation on parameterized programs demonstrates that Horn-SDT achieves faster convergence and constructs more compact trees compared to non-symmetric baselines.