Verification of binary neural network (BNN) robustness is NP-hard, as it can be formulated as a combinatorial search for an adversarial perturbation that induces misclassification. Exact verification methods therefore scale poorly with problem dimension, motivating the use of hardware-accelerated heuristics and unconventional computing platforms, such as Ising solvers, that can efficiently explore complex energy landscapes and discover high-quality solutions. In this work, we reformulate BNN robustness verification as a quadratic unconstrained binary optimization (QUBO) problem and solve it using a digital compute-in-memory (DCIM) SRAM-based Ising machine. Instead of requiring globally optimal solutions, we exploit imperfect solutions produced by the DCIM Ising machine to extract adversarial perturbations and thereby demonstrate the non-robustness of the BNN. The proposed architecture stores quantized QUBO coefficients in approximately 9.1~Mb of SRAM and performs annealing in memory via voltage-controlled pseudo-read dynamics, enabling iterative updates with minimal data movement. Experimental projections indicate that the proposed approach achieves a $178\times$ acceleration in convergence rate and a $1538\times$ improvement in power efficiency relative to conventional CPU-based implementations.

翻译：二进制神经网络（BNN）的鲁棒性验证属于NP难问题，因为它可被表述为寻找导致误分类的对抗扰动的组合搜索问题。因此，精确验证方法随问题维度增加而扩展性差，这促使人们采用硬件加速启发式算法和非常规计算平台（如伊辛求解器），这些平台能够高效探索复杂能量景观并发现高质量解。在本工作中，我们将BNN鲁棒性验证重新表述为二次无约束二进制优化（QUBO）问题，并使用基于数字存内计算（DCIM）SRAM的伊辛机进行求解。我们无需全局最优解，而是利用DCIM伊辛机产生的不完美解来提取对抗扰动，从而证明BNN的非鲁棒性。所提出的架构将量化后的QUBO系数存储在约9.1~Mb的SRAM中，并通过电压控制伪读取动态在内存中执行退火，实现了数据移动最小化的迭代更新。实验预测表明，相对于传统的基于CPU的实现，所提方法在收敛速度上实现了$178\times$的加速，在能效上实现了$1538\times$的提升。