Adnan Rashid

Adnan Rashid

Large Language Models (LLMs) have transformed artificial intelligence from primarily generative systems into increasingly capable reasoning agents. Recent advances in theorem proving, autoformalization, symbolic reasoning, and tool-augmented language models demonstrate substantial progress toward machine-assisted formal reasoning. However, current reasoning systems still suffer from hidden logical inconsistencies, hallucinated symbolic transitions, unsupported theorem applications, and limited reliability guarantees. Existing approaches remain fragmented across formal verification, runtime assurance, neuro-symbolic reasoning and trustworthy Artificial Intelligence (AI) research communities. This paper introduces ReasonOps, a unified operational paradigm for trustworthy verified reasoning systems. Inspired by operational ecosystems such as DevOps and MLOps, ReasonOps treats reasoning as a continuously monitored, verifiable, reliability-aware operational process rather than an isolated inference task. The proposed paradigm integrates semantic interpretation, autoformalization, symbolic reasoning, theorem proving, runtime assurance, probabilistic reliability estimation, and adaptive correction into a unified reasoning lifecycle. The paper further presents the ReasonOps architecture, demonstrates its workflow using an autonomous braking system analysis example, and discusses its potential role in future safety-critical autonomous AI systems. We argue that operational reasoning paradigms such as ReasonOps may become foundational infrastructure for next-generation trustworthy AI ecosystems.

Kubra Aksoy, Adnan Rashid, Osman Hasan et al.

Network topology matrices are algebraic representations of graphs that are widely used in modeling and analysis of various applications including electrical circuits, communication networks and transportation systems. In this paper, we propose to use Higher-Order-Logic (HOL) based interactive theorem proving to formalize network topology matrices. In particular, we formalize adjacency, degree, Laplacian and incidence matrices in the Isabelle/HOL proof assistant. Our formalization is based on modelling systems as networks using the notion of directed graphs (unweighted and weighted), where nodes act as components of the system and weighted edges capture the interconnection between them. Then, we formally verify various classical properties of these matrices, such as indexing and degree. We also prove the relationships between these matrices in order to provide a comprehensive formal reasoning support for analyzing systems modeled using network topology matrices. To illustrate the effectiveness of the proposed approach, we formally analyze the Kron reduction of the Laplacian matrix and verify the total power dissipation in a generic resistive electrical network, both commonly used in power flow analysis.

Nour Dekhil, Adnan Rashid, Sofiene Tahar

We introduce a proof recommender system for the HOL4 theorem prover. Our tool is built upon a transformer-based model [2] designed specifically to provide proof assistance in HOL4. The model is trained to discern theorem proving patterns from extensive libraries of HOL4 containing proofs of theorems. Consequently, it can accurately predict the next tactic(s) (proof step(s)) based on the history of previously employed tactics. The tool operates by reading a given sequence of tactics already used in a proof process (in our case, it contains at least three tactics), referred to as the current proof state, and provides recommendations for the next optimal proof step(s).

Amira Jemaa, Adnan Rashid, Sofiene Tahar

Explainable Artificial Intelligence (XAI) plays an important role in improving the transparency and reliability of complex machine learning models, especially in critical domains such as cybersecurity. Despite the prevalence of heuristic interpretation methods such as SHAP and LIME, these techniques often lack formal guarantees and may produce inconsistent local explanations. To fulfill this need, few tools have emerged that use formal methods to provide formal explanations. Among these, XReason uses a SAT solver to generate formal instance-level explanation for XGBoost models. In this paper, we extend the XReason tool to support LightGBM models as well as class-level explanations. Additionally, we implement a mechanism to generate and detect adversarial examples in XReason. We evaluate the efficiency and accuracy of our approach on the CICIDS-2017 dataset, a widely used benchmark for detecting network attacks.

Adnan Rashid, Osman Hasan

Robotic cell injection is used for automatically delivering substances into a cell and is an integral component of drug development, genetic engineering and many other areas of cell biology. Traditionally, the correctness of functionality of these systems is ascertained using paper-and-pencil proof and computer simulation methods. However, the paper based proofs can be human-error prone and the simulation provides an incomplete analysis due to its sampling based nature and the inability to capture continuous behaviors in computer based models. Model checking has been recently advocated for the analysis of cell injection systems as well. However, it involves the discretization of the differential equations that are used for modeling the dynamics of the system and thus compromises on the completeness of the analysis as well. In this paper, we propose to use higher-order-logic theorem proving for the modeling and analysis of the dynamical behaviour of the robotic cell injection systems. The high expressiveness of the underlying logic allows us to capture the continuous details of the model in their true form. Then, the model can be analyzed using deductive reasoning within the sound core of a proof assistant.

Adnan Rashid, Osman Hasan

Control systems are an integral part of almost every engineering and physical system and thus their accurate analysis is of utmost importance. Traditionally, control systems are analyzed using paper-and-pencil proof and computer simulation methods, however, both of these methods cannot provide accurate analysis due to their inherent limitations. Model checking has been widely used to analyze control systems but the continuous nature of their environment and physical components cannot be truly captured by a state-transition system in this technique. To overcome these limitations, we propose to use higher-order-logic theorem proving for analyzing linear control systems based on a formalized theory of the Laplace transform method. For this purpose, we have formalized the foundations of linear control system analysis in higher-order logic so that a linear control system can be readily modeled and analyzed. The paper presents a new formalization of the Laplace transform and the formal verification of its properties that are frequently used in the transfer function based analysis to judge the frequency response, gain margin and phase margin, and stability of a linear control system. We also formalize the active realizations of various controllers, like Proportional-Integral-Derivative (PID), Proportional-Integral (PI), Proportional-Derivative (PD), and various active and passive compensators, like lead, lag and lag-lead. For illustration, we present a formal analysis of an unmanned free-swimming submersible vehicle using the HOL Light theorem prover.