Fahman Saeed

Automated loop invariant inference remains a fundamental challenge in formal verification due to the inherently unbounded search space of candidate invariants. Existing approaches either incur substantial computational overhead during invariant synthesis or rely on manually predefined templates, limiting both scalability and automation. Although recent learning-based methods have shown promise, they often fail to fully exploit the rich structural and semantic information embedded within program representations. This paper presents a learning-guided framework for fully automated loop invariant inference based on a systematic analysis of program structure and semantics. The framework performs a joint analysis of syntactic constructs, control-flow structure, and data-dependence relationships to determine invariant structure before instantiation. These complementary representations are embedded and integrated within a learning-based model that identifies structurally and semantically features and infers expressive invariant templates directly from program structure. The inferred templates are instantiated using execution-derived values, yielding constraint systems that are solved and formally validated using a Satisfiability Modulo Theories solver. Experimental evaluation demonstrates that the proposed approach achieves competitive invariant inference performance on challenging benchmarks. By integrating multi-representation program analysis, the framework effectively supports a wide range of loop structures and advances the state of the art in scalable, expressive, and fully automated loop invariant inference.

Deepfake videos currently facilitate extensive financial deception, political misinformation, and unauthorized imagery, with anticipated U.S. losses from deepfake-related fraud surpassing $40 billion by 2027; human evaluators accurately recognize high-quality forgeries merely 25% of the time, highlighting the pressing necessity for automated, widely applicable detection mechanisms. Adaptive-depth architectures offer an intriguing alternative to fixed-depth deepfake detectors when the optimal model capacity is indeterminate in advance. This study presents the Adaptive Entropy-Guided ICA State-Space Model Forgery Detector (AEGIS-FD), a deepfake detection framework at the video level that progressively increases its depth from one to eight layers via an entropy-driven growth mechanism, attaining peak validation performance at a depth of six. The design incorporates a three-dimensional spatiotemporal stem, Sinkhorn-normalized manifold-constrained hyper-coupling (mHC) layers for balanced temporal integration, a selected state-space temporal block for sequence depiction, and FastICA-based initialization for newly introduced layers. Evaluated using Celeb-DF v2, AEGIS-FD achieves a test AUC of 0.9600 and a validation AUC of 0.9607, above the performance of a single-layer Mamba SSM baseline (AUC = 0.8355). In comparison to a fixed-depth-6 baseline, the model demonstrates consistent improvements over five random seeds (96.12 ± 0.28 vs. 94.84 ± 0.44 AUC; p = 0.0022), suggesting that adaptive development provides advantages that exceed mere depth. In a zero-shot cross-dataset evaluation—trained on Celeb-DF v2 and assessed without fine-tuning on a FaceForensics++ (FF++) C23 subset comprising 1000 original and 1000 FaceSwap videos—AEGIS-FD achieves an AUC of 89.2 compared to 88.4 for the corresponding baseline (+0.8 AUC), providing initial proof of cross-dataset transferability. These findings suggest that adaptive-depth growth presents a viable approach for detecting deepfakes at the video level, while further validation across various datasets and modification techniques is essential.

The quick and accurate diagnosis of Alzheimer's disease (AD) and Frontotemporal Dementia (FTD) is a significant and unresolved challenge in clinical neurology, with early identification being crucial for prompt intervention and disease management. This study presents AutoSSM-ICA-EEG, an automated and interpretable framework that incorporates Fast Independent Component Analysis (FastICA) for artifact removal and relevant feature extraction, few-shot AutoML for efficient hyperparameter optimization and dynamic architecture adaptation, and State-Space Modeling (SSM) for temporal EEG dynamics, facilitating concurrent classification of dementia subtypes and regression of clinical severity. Three distinct datasets were utilized: (1) OpenNeuro ds006036 (open-eyes/photic stimulation EEG; AD, FTD, and Healthy Controls; n = 88), functioning as the primary tri-class benchmark; (2) OpenNeuro ds004504 (closed-eyes resting-state EEG; AD and HC; n = 65), employed for cross-condition generalization; and (3) ADFSU (resting-state EEG; AD and HC; external institution, UNESP Brazil), utilized for cross-institution transfer assessment. Rigorous subject-level leave-one-subject-out (LOSO) cross-validation was uniformly implemented throughout all four evaluation protocols, ensuring that all preprocessing, ICA decomposition, and model tuning were performed solely within each training fold to avert data leakage. In the primary tri-class benchmark, the model attained an accuracy of 87.5%, macro sensitivity of 87.5%, macro specificity of 95.4%, macro F1-score of 88.7%, and macro AUC of 0.99. The regression analysis of MMSE severity produced a R² of 0.81 ± 0.04, with a mean absolute error (MAE) of 1.64 ± 0.31 and a root mean square error (RMSE) of 1.71 ± 0.21. Cross-condition generalization (Closed→Open and Open→Closed) and cross-institution transfer (ADFSU↔OpenNeuro; AD sensitivity = 83.9%) further validate the framework's resilience beyond a singular dataset or recording situation. ICA-refined SHAP channel-level explainability identifies Ch11 and Ch13 as the principal neurophysiological biomarkers for subtype classification and MMSE severity regression, respectively, with Ch17 serving as the most sensitive predictor of disease duration - corroborating established frontotemporal EEG signatures of neurodegeneration. These findings establish AutoSSM-ICA-EEG as a potential, neurophysiologically interpretable paradigm for EEG-based dementia screening, subject to prospective multi-site clinical validation.

Accurate prediction of Chronic Kidney Disease (CKD) development is essential for prompt therapeutic intervention; nevertheless, it is difficult due to the highly individualized disease trajectories and intricate multivariate risk profiles. Contemporary deep learning models provide substantial predictive capability; yet, they frequently exhibit computational inefficiency and a lack of interpretability, akin to a “black box.” To overcome these limitations, we present the Eigen-Guided Transformer, an innovative architecture that systematically enhances model topology by data-driven eigenvalue analysis of clinical feature correlations. Our methodology independently establishes: (1) the optimal quantity of attention heads by ascertaining the intrinsic dimensionality necessary to account for 95% of data variance (h = 11), (2) an eigenvector-informed weight initialization to encapsulate a priori feature interactions, and (3) validation-driven depth optimization. Upon assessing daily-aggregated longitudinal sequences from the MIMIC-IV dataset for creatinine prediction, the model attained a Mean Squared Error (MSE) of 0.089 ± 0.004 and a Mean Absolute Error (MAE) of 0.132 + 0.0001, indicating an 11.1% enhancement over the most robust baseline (TFT). The Eigen-Guided Transformer exhibited exceptional parameter efficiency, achieving a FLOPs/accuracy ratio of 142.4M, markedly lower than that of TFT (300M) and Autoformer (1.0B). External validation of the eICU dataset demonstrated strong cross-institutional generalizability (MSE 0.0117 ± 0.0001; MAE 0.0254 + 0.0008). To guarantee clinical dependability, we incorporated Monte Carlo Dropout for uncertainty quantification, resulting in precisely calibrated prediction intervals with 95.8% observed coverage. Additionally, a demographic fairness audit encompassing age, gender, and ethnicity demonstrated equitable performance, with a maximum discrepancy ratio of merely 1.32. The Eigen-Guided Transformer offers a transparent, efficient, and reliable paradigm for the individualized therapy of chronic renal disease by matching attention mechanisms with the intrinsic biological structure of clinical data.

Modern energy systems necessitate accurate peak demand predictions to minimize costs. This study presents an adaptive FastICA-Transformer that improves feature extraction and forecasting precision using entropy-guided component selection and a redesigned transformer architecture. The model modifies transformer depth according to the forecast horizon and initializes attention heads using statistically independent FastICA components, resulting in interpretable and efficient networks. In comparison to PCA-Transformer and sophisticated neural architectures (LSTM, TCN, N-BEATS, TFT), the FastICA-Transformer demonstrates enhanced MAE, RMSE, and MAPE in forecasting for Next-Hour, Next-Day, Next-Week, and Next-Quarter intervals. The results indicate that architectural adaptation, informed by temporal and statistical characteristics, efficiently tackles peak demand forecasts in practical power systems.

This study examines the complex interactions between CO₂ emissions, economic growth, and energy consumption across various classifications of countries. In this study, we propose SSM-FastICANet, a novel hybrid model that integrates state space models with independent component analysis and a diagonal structure for efficient and accurate economic growth forecasting a predictive model that can forecast economic growth by analyzing energy consumption patterns and emission levels, while also pinpointing the distinct impacts of CO₂ emissions and energy usage. Employing a time-series dataset and an innovative hybrid methodology that combines state space models (SSMs) with fast independent component analysis (FastICA), the study reveals unique interaction patterns among these variables. The FastICA method aids in uncovering essential underlying patterns and reducing dimensionality, whereas the SSM architecture proficiently captures temporal dependencies and emphasizes the most pertinent input features for precise prediction and impact detection. The model utilizes entropy, kurtosis, and variance to filter independent components, guaranteeing that the chosen features are statistically significant, locally structured, and resilient to noise. The findings demonstrate that SSM-FastICANet significantly enhances feature selection, model adaptability, and interpretability, yielding reliable predictions over various time intervals. It enhances the comprehension of the energy-economy-environment relationship and offers a solid framework for policymakers to develop strategies that foster sustainable economic growth while reducing environmental impact.

There is a pressing need to build a sign-to-text translation system to simplify communication between deaf and non-deaf people. This study investigates the building of a high-performance, lightweight sign language translation system suitable for real-time applications. Two Saudi Sign Language datasets are used for evaluation. We also investigate the effects of the number of signers and number of repetitions in sign language datasets. To this end, eight experiments are conducted in both signer-dependent and signer-independent modes. A comprehensive ablation study is presented to study the impacts of model components, network depth, and the size of the hidden dimension. The best accuracies achieved are 97.7% and 90.7% for the signer-dependent and signer-independent modes, respectively, using the KSU-SSL dataset. Similarly, the model achieves 98.38% and 96.22% for signer-dependent and signer-independent modes using the ArSL dataset.

Autism spectrum disorder (ASD) is a diverse neurodevelopmental condition with a significant genetic basis. Machine learning (ML) and deep learning (DL) models are emerging as powerful tools for identifying potential ASD risk genes and biomarkers to improve diagnostic accuracy. This narrative systematic review synthesizes evidence on the use of ML and DL models for ASD prediction and diagnosis, focusing on studies that utilized genetic variants and biomarkers. We conducted a systematic search across six databases [Web of Science, PubMed, Science Direct, Semantic Scholar, Institute of Electrical and Electronics Engineers (IEEE Xplore), and Association for Computing Machinery Digital Library (ACM-DL)] for articles published between 2009 and 2024, yielding 483 initial records. Multiple inclusion criteria were applied, and only peer-reviewed articles that used artificial intelligence, ML, or DL to predict ASD based on genetic biomarkers were included. After deduplication and applying inclusion and exclusion criteria, 14 studies were included in this review. These studies focused on genetic variants based on whole-genome sequencing, whole-exome sequencing, RNA sequencing, single-nucleus RNA sequencing, mRNA expression, long non-coding RNA, or single nucleotide polymorphism data. Our findings indicate that various ML models achieved robust performance, while DL architectures such as DeepASDPred outperformed ML models, with an accuracy of 93.8%. Most of the studies used datasets such as the Simons Foundation Autism Research Initiative (SFARI), the Simons Simplex Collection (SSC), the Autism Genetic Resource Exchange (AGRE), Atlas of the Developing Human Brain (BrainSpan), and the Simons Foundation Powering Autism Research for Knowledge (SPARK). The reviewed studies demonstrate that ML can help identify genetic risk factors and biomarkers that contribute to ASD. However, challenges remain, including data heterogeneity, small sample sizes, and the need for greater model interpretability. Addressing these challenges is crucial for translating ML models into clinically useful tools. In conclusion, DL substantially enhances ASD prediction, leveraging genetic data to identify novel candidate genes and support biological discovery of cell type-specific gene expression and roles of non-coding mutations in ASD.

The incorporation of renewable energy sources into the power grid has necessitated the development of sophisticated forecasting models that can effectively handle the inherent fluctuation and uncertainty associated with renewable energy generation. In this study, an adaptive principal component analysis (PCA)-enhanced transformer architecture, hereinafter referred to as PCA–Transformer, is developed to enhance the performance of transformer models in predicting renewable energy output. The proposed model uses PCA to dynamically determine and adapt the transformer architecture and prioritize the most informative features from time series data, thereby improving the model’s attention on relevant information and reducing computational burden. This is essential for accurately capturing the intricate temporal patterns and nonlinear relationships that are typical present in renewable energy time series data. The PCA–Transformer enhances the performance of transformer models in sequence-to-sequence predictions by incorporating an adaptive mechanism that customizes their structure based on the best PCA eigenvectors. The architecture adaptively aligns with the underlying patterns in data by adjusting the number of attention heads and critical dimensions within each transformer block. The adaptability of the proposed architecture is crucial for effectively simulating the complex nature of renewable energy generation patterns. The efficiency of the proposed model was evaluated using the Alice Springs Australia DKASC-ASA and EIA Energy datasets. The proposed model has superior forecasting performance than traditional transformer models and cutting-edge renewable energy forecasting methodologies.

Nowadays, technology is increasingly being adopted in different kinds of businesses to process, store, and share sensitive information in digital environments that include enormous numbers of users. However, this has also increased the likelihood of cyberattacks and misuse of information, potentially causing severe damage. One promising technology, which can provide the required security services with an improved level of efficiency, is blockchain. This research explores the use of Ethereum blockchain and smart contracts to create a secure and efficient quality assurance system (QAS) for academic programs. By utilizing blockchain and smart contracts, the proposed approach improves the integrity and reliability of sensitive information processed by the QAS, promotes transparency and governance, and reduces the time and effort required for quality operations. The current approach uses an additional access control layer to further enhance user privacy. Smart contracts automate various quality transactions and saves time and resources, and hence increases the efficiency of the QAS. The interplanetary file system (IPFS) is used to address the challenge of size limitations in blockchain. Additionally, this research investigates the use of various cryptographic schemes to provide robust security services at the application layer. The experimental results showed that the use of a hybrid cryptosystem relying on an Elliptic curve digital signature and AES encryption (AES_ECCDSA) outperforms other counterparts’ cryptosystems using an RSA digital signature and AES encryption (AES_RSADSA) and Elliptic Curve Integrated Encryption Scheme (ECIES) in terms of speed. The performance results showed that AES_ECCDSA consumes 188 ms to perform the required cryptographic operations for a standard-quality document with a size of 8088 KB, compared to the 231 ms and 739 ms consumed by the AES_RSADSA and ECIES schemes, respectively. This study presents a prototype implementation of the blockchain-based QAS, which outlines the processing model and system requirements for key QAS processes. It has been found that the cost and time required for blockchain operations vary depending on the size of the input data—a larger data size requires more time and costs more to process. The results of the current study showed that the time delay for blockchain transactions ranges from 15 to 120 s, while the cost ranges from USD 50 to USD 400. This research provides evidence that blockchain and smart contract technologies have the potential to create a secure, efficient, and trustworthy QAS environment for academic programs.