Can Zhou

Can Zhou, Razin A. Shaikh, Yiran Li et al.

A domain-theoretic framework is presented for validated robustness analysis of neural networks. First, global robustness of a general class of networks is analyzed. Then, using the fact that Edalat's domain-theoretic L-derivative coincides with Clarke's generalized gradient, the framework is extended for attack-agnostic local robustness analysis. The proposed framework is ideal for designing algorithms which are correct by construction. This claim is exemplified by developing a validated algorithm for estimation of Lipschitz constant of feedforward regressors. The completeness of the algorithm is proved over differentiable networks, and also over general position ReLU networks. Computability results are obtained within the framework of effectively given domains. Using the proposed domain model, differentiable and non-differentiable networks can be analyzed uniformly. The validated algorithm is implemented using arbitrary-precision interval arithmetic, and the results of some experiments are presented. The software implementation is truly validated, as it handles floating-point errors as well.

Can Zhou, Yulong Gao, Pian Yu

Synthesising autonomous agents that can navigate uncertain environments while adhering to complex temporal constraints remains a fundamental challenge. While Linear Temporal Logic (LTL) provides a rigorous language for specifying such tasks, the inherent undecidability of qualitatively verifying LTL satisfaction in partially observable Markov decision processes renders quantitative synthesis difficult, especially when designing reliable reward signals for approximate solvers. In this paper, we bridge this gap with a novel, sound reward-shaping mechanism that dynamically generates belief-dependent rewards grounded in certified LTL satisfaction. By integrating this mechanism into an enhanced Monte Carlo Planning framework, we empower agents to navigate the `fog' of partial observability with a search process focused on maximising verifiable success. Our experiments demonstrate that this approach not only thrives in scenarios where existing solvers fail but also maintains effectiveness and scalability across diverse benchmark domains.

Canzong Zhou, Can Zhou, Hongqiu Zhu et al.

Zinc electrolysis is one of the key processes in zinc smelting, and maintaining stable operation of zinc electrolysis is an important factor in ensuring production efficiency and product quality. However, poor contact between the zinc electrolysis cathode and the anode is a common problem that leads to reduced production efficiency and damage to the electrolysis cell. Therefore, online monitoring of the contact status of the plates is crucial for ensuring production quality and efficiency. To address this issue, we propose an end-to-end network, the Frequency-masked Multimodal Autoencoder (FM-AE). This method takes the cell voltage signal and infrared image information as input, and through automatic encoding, fuses the two features together and predicts the poor contact status of the plates through a cascaded detector. Experimental results show that the proposed method maintains high accuracy (86.2%) while having good robustness and generalization ability, effectively detecting poor contact status of the zinc electrolysis cell, providing strong support for production practice.