Jun Sun

Yedi Zhang, Yufan Cai, Xinyue Zuo et al.

Large Language Models (LLMs) have emerged as a transformative AI paradigm, profoundly influencing daily life through their exceptional language understanding and contextual generation capabilities. Despite their remarkable performance, LLMs face a critical challenge: the propensity to produce unreliable outputs due to the inherent limitations of their learning-based nature. Formal methods (FMs), on the other hand, are a well-established computation paradigm that provides mathematically rigorous techniques for modeling, specifying, and verifying the correctness of systems. FMs have been extensively applied in mission-critical software engineering, embedded systems, and cybersecurity. However, the primary challenge impeding the deployment of FMs in real-world settings lies in their steep learning curves, the absence of user-friendly interfaces, and issues with efficiency and adaptability. This position paper outlines a roadmap for advancing the next generation of trustworthy AI systems by leveraging the mutual enhancement of LLMs and FMs. First, we illustrate how FMs, including reasoning and certification techniques, can help LLMs generate more reliable and formally certified outputs. Subsequently, we highlight how the advanced learning capabilities and adaptability of LLMs can significantly enhance the usability, efficiency, and scalability of existing FM tools. Finally, we show that unifying these two computation paradigms -- integrating the flexibility and intelligence of LLMs with the rigorous reasoning abilities of FMs -- has transformative potential for the development of trustworthy AI software systems. We acknowledge that this integration has the potential to enhance both the trustworthiness and efficiency of software engineering practices while fostering the development of intelligent FM tools capable of addressing complex yet real-world challenges.

Jun Sun, Xiaojun Wu, Vasile Palade et al.

The random drift particle swarm optimization (RDPSO) algorithm, inspired by the free electron model in metal conductors placed in an external electric field, is presented, systematically analyzed and empirically studied in this paper. The free electron model considers that electrons have both a thermal and a drift motion in a conductor that is placed in an external electric field. The motivation of the RDPSO algorithm is described first, and the velocity equation of the particle is designed by simulating the thermal motion as well as the drift motion of the electrons, both of which lead the electrons to a location with minimum potential energy in the external electric field. Then, a comprehensive analysis of the algorithm is made, in order to provide a deep insight into how the RDPSO algorithm works. It involves a theoretical analysis and the simulation of the stochastic dynamical behavior of a single particle in the RDPSO algorithm. The search behavior of the algorithm itself is also investigated in detail, by analyzing the interaction between the particles. Some variants of the RDPSO algorithm are proposed by incorporating different random velocity components with different neighborhood topologies. Finally, empirical studies on the RDPSO algorithm are performed by using a set of benchmark functions from the CEC2005 benchmark suite. Based on the theoretical analysis of the particle's behavior, two methods of controlling the algorithmic parameters are employed, followed by an experimental analysis on how to select the parameter values, in order to obtain a good overall performance of the RDPSO algorithm and its variants in real-world applications. A further performance comparison between the RDPSO algorithms and other variants of PSO is made to prove the efficiency of the RDPSO algorithms.