Searcharxiv⌕ Search

arXiv subjects

Mahfuza Farooque

Publications and source records attributed to Mahfuza Farooque.

13 recordsLinked to original sources
arXiv2026

Cogniscope: A Synthetic Longitudinal Benchmark and Browser-Based Evaluation Framework for Early-Risk Cognitive AI Systems

We present Cogniscope, an open evaluation framework for studying longitudinal early-risk AI systems under controlled behavioral drift, sparse observations, delayed evidence, and heterogeneous progression patterns. Cogniscope combines two complementary components: a synthetic simulation engine that generates privacy-preserving longitudinal behavioral traces aligned with configurable latent risk trajectories, and a browser-based data-collection instrument implemented as a Chrome extension for capturing naturalistic video interaction telemetry and micro-question responses during YouTube playback. The released benchmark includes 200,000 simulated video-interaction records from 200 users over 200 days, a 504-session schema-aligned synthetic deployment dataset across nine behavioral profiles, an 18-table relational schema, baseline evaluation scripts, and time-aware metrics including Early Risk Detection Error (ERDE) and time-to-detection (TTD). We emphasize that Cogniscope is not a diagnostic system and does not claim clinical validity. Instead, it provides a reusable testbed for evaluating how sequential models behave under known longitudinal challenges before deployment with real human-subject data. Experiments show that simple behavioral coherence signals separate simulated risk states under controlled priors, while rule-based deployment-profile classification remains challenging, motivating learned temporal models and robust evaluation protocols.

cs.HC↗
arXiv2026

A Pilot Benchmark for NL-to-FOL Translation in Planetary Exploration

Future planetary exploration envisions autonomous robotic agents operating under severe communication constraints, without global positioning, and with minimal human intervention. In such environments, agents must not only perceive and act, but also reason over mission objectives, operational constraints, and evolving environmental conditions. While prior work has largely focused on perception and control, the translation of high-level mission knowledge into structured, machine-interpretable representations remains underexplored. We introduce a pilot benchmark for translating natural language (NL) into First-Order Logic (FOL) within the domain of planetary exploration. The dataset is constructed from real mission documentation sourced from NASA's Planetary Data System (PDS), spanning missions from 2003 to 2013. These documents describe mission phases such as launch, boost, coast, cruise, and orbital operations in rich natural language. We manually annotate these documents with corresponding FOL representations that capture temporal structure, agent roles, and operational dependencies. In addition, we provide structured predicate vocabularies and typed constants to enable controlled experimentation with varying levels of prior knowledge. This pilot benchmark provides a foundation for research at the intersection of language understanding and formal reasoning, grounded in real-world, safety-critical mission data. The dataset is provided at: https://github.com/HaydenMM/planetary-logic-benchmark/blob/main/pilot_benchmark.json

cs.CL↗
arXiv2026

VeriTrans: Fine-Tuned LLM-Assisted NL-to-PL Translation via a Deterministic Neuro-Symbolic Pipeline

\textbf{VeriTrans} is a reliability-first ML system that compiles natural-language requirements into solver-ready logic with validator-gated reliability. The pipeline integrates an instruction-tuned NL$\!\to\!$PL translator, round-trip reconstruction (PL$\!\to\!$NL) used as a high-precision acceptance gate, and canonical PL$\!\to\!$CNF compilation, all executed via fixed API configuration (temperature$=0$; fine-tuning runs use seed$=42$) and per-item artifact logging (prompts, outputs, hashes) to support auditability and replay-driven debugging. On \textbf{SatBench} (2{,}100 specifications), VeriTrans achieves 94.46\% SAT/UNSAT correctness and 87.73\% median round-trip similarity. Compact fine-tuning on 100--150 curated examples improves fidelity by about 1--1.5\,pp without increasing latency (mean 25.8\,s/spec on our 201-spec runtime subset). A thresholded acceptance policy on the round-trip score exposes a reliability--coverage knob: at $τ{=}75$, roughly 68\% of items are retained with $\sim$94\% correctness on the accepted set. Validator overhead contributes $<15\%$ of end-to-end runtime, and all prompts/responses and timing metadata are logged to enable replay-driven debugging and regression testing. By separating learned translation from symbolic verification and enforcing deterministic, validator-gated acceptance, VeriTrans turns NL$\!\to\!$logic front-ends into auditable, reproducible components for reliability-critical workflows.

cs.AI↗
arXiv2025

Cogniscope: Modeling Social Media Interactions as Digital Biomarkers for Early Detection of Cognitive Decline

Alzheimer's disease (AD) and its prodromal stage, Mild Cognitive Impairment (MCI), are associated with subtle declines in memory, attention, and language that often go undetected until late in progression. Traditional diagnostic tools such as MRI and neuropsychological testing are invasive, costly, and poorly suited for population-scale monitoring. Social platforms, by contrast, produce continuous multimodal traces that can serve as ecologically valid indicators of cognition. In this paper, we introduce Cogniscope, a simulation framework that generates social-media-style interaction data for studying digital biomarkers of cognitive health. The framework models synthetic users with heterogeneous trajectories, embedding micro-tasks such as video summarization and lightweight question answering into content consumption streams. These interactions yield linguistic markers (semantic drift, disfluency) and behavioral signals (watch time, pausing, sharing), which can be fused to evaluate early detection models. We demonstrate the framework's use through ablation and sensitivity analyses, showing how detection performance varies across modalities, noise levels, and temporal windows. To support reproducibility, we release the generator code, parameter configurations, and synthetic datasets. By providing a controllable and ethically safe testbed, Cogniscope enables systematic investigation of multimodal cognitive markers and offers the community a benchmark resource that complements real-world validation studies.

cs.HC↗
arXiv2025

LangSAT: A Novel Framework Combining NLP and Reinforcement Learning for SAT Solving

Our work presents a novel reinforcement learning (RL) based framework to optimize heuristic selection within the conflict-driven clause learning (CDCL) process, improving the efficiency of Boolean satisfiability (SAT) solving. The proposed system, LangSAT, bridges the gap between natural language inputs and propositional logic by converting English descriptions into Conjunctive Normal Form (CNF) expressions and solving them using an RL-enhanced CDCL SAT solver. Unlike existing SAT-solving platforms that require CNF as input, LangSAT enables users to input standard English descriptions, making SAT-solving more accessible. The framework comprises two key components: Lang2Logic, which translates English sentences into CNF expressions, and SmartSAT, an RL-based SAT solver. SmartSAT encodes clause-variable relationships as structured graph representations and extracts global features specific to the SAT problem. This implementation provides the RL agent with deeper contextual information, enabling SAT problems to be solved more efficiently. Lang2Logic was evaluated on diverse natural language inputs, processing descriptions up to 450 words. The generated CNFs were solved by SmartSAT, which demonstrated comparable performance to traditional CDCL heuristics with respect to solving time. The combined LangSAT framework offers a more accessible and scalable solution for SAT-solving tasks across reasoning, formal verification, and debugging.

cs.CL↗
arXiv2025

Fine-Tuned Large Language Models for Logical Translation: Reducing Hallucinations with Lang2Logic

Recent advances in natural language processing (NLP), particularly large language models (LLMs), have motivated the automatic translation of natural language statements into formal logic without human intervention. This enables automated reasoning and facilitates debugging, finding loop invariants, and adhering to specifications in software systems. However, hallucinations-incorrect outputs generated by LLMs are challenging, particularly for logical translation tasks requiring precision. This work introduces a novel framework that inputs English sentences, converts them into logical expressions, and then translates them into Conjunctive Normal Form (CNF) for satisfiability solving. It employs classical NLP techniques with self-defined grammar, symbolic computation libraries, and a fine-tuned language model to reduce hallucinations. In the early experiments, we observed that the fine-tuned model, trained on different grammar settings, could intentionally correct the same types of hallucinations made by the original model. Thus, it provides reliable CNF generation.

cs.CL↗
arXiv2025

Memory-Augmented Log Analysis with Phi-4-mini: Enhancing Threat Detection in Structured Security Logs

Structured security logs are critical for detecting advanced persistent threats (APTs). Large language models (LLMs) struggle in this domain due to limited context and domain mismatch. We propose \textbf{DM-RAG}, a dual-memory retrieval-augmented generation framework for structured log analysis. It integrates a short-term memory buffer for recent summaries and a long-term FAISS-indexed memory for historical patterns. An instruction-tuned Phi-4-mini processes the combined context and outputs structured predictions. Bayesian fusion promotes reliable persistence into memory. On the UNSW-NB15 dataset, DM-RAG achieves 53.64% accuracy and 98.70% recall, surpassing fine-tuned and RAG baselines in recall. The architecture is lightweight, interpretable, and scalable, enabling real-time threat monitoring without extra corpora or heavy tuning.

cs.CR↗
arXiv2025

Causally-Informed Reinforcement Learning for Adaptive Emotion-Aware Social Media Recommendation

Social media recommendation systems play a central role in shaping users' emotional experiences. However, most systems are optimized solely for engagement metrics, such as click rate, viewing time, or scrolling, without accounting for users' emotional states. Repeated exposure to emotionally charged content has been shown to negatively affect users' emotional well-being over time. We propose an Emotion-aware Social Media Recommendation (ESMR) framework that personalizes content based on users' evolving emotional trajectories. ESMR integrates a Transformer-based emotion predictor with a hybrid recommendation policy: a LightGBM model for engagement during stable periods and a reinforcement learning agent with causally informed rewards when negative emotional states persist. Through behaviorally grounded evaluation over 30-day interaction traces, ESMR demonstrates improved emotional recovery, reduced volatility, and strong engagement retention. ESMR offers a path toward emotionally aware recommendations without compromising engagement performance.

cs.IR↗
arXiv2025

Next-Gen Education: Enhancing AI for Microlearning

This paper explores integrating microlearning strategies into university curricula, particularly in computer science education, to counteract the decline in class attendance and engagement in US universities after COVID. As students increasingly opt for remote learning and recorded lectures, traditional educational approaches struggle to maintain engagement and effectiveness. Microlearning, which breaks complex subjects into manageable units, is proposed to address shorter attention spans and enhance educational outcomes. It uses interactive formats such as videos, quizzes, flashcards, and scenario-based exercises, which are especially beneficial for topics like algorithms and programming logic requiring deep understanding and ongoing practice. Adoption of microlearning is often limited by the effort needed to create such materials. This paper proposes leveraging AI tools, specifically ChatGPT, to reduce the workload for educators by automating the creation of supplementary materials. While AI can automate certain tasks, educators remain essential in guiding and shaping the learning process. This AI-enhanced approach ensures course content is kept current with the latest research and technology, with educators providing context and insights. By examining AI capabilities in microlearning, this study shows the potential to transform educational practices and outcomes in computer science, offering a practical model for combining advanced technology with established teaching methods.

cs.CY↗
arXiv2015

Axiomatic constraint systems for proof search modulo theories

Goal-directed proof search in first-order logic uses meta-variables to delay the choice of witnesses; substitutions for such variables are produced when closing proof-tree branches, using first-order unification or a theory-specific background reasoner. This paper investigates a generalisation of such mechanisms whereby theory-specific constraints are produced instead of substitutions. In order to design modular proof-search procedures over such mechanisms, we provide a sequent calculus with meta-variables, which manipulates such constraints abstractly. Proving soundness and completeness of the calculus leads to an axiomatisation that identifies the conditions under which abstract constraints can be generated and propagated in the same way unifiers usually are. We then extract from our abstract framework a component interface and a specification for concrete implementations of background reasoners.

cs.LO↗
arXiv2013

Sequent Calculi with procedure calls

In this paper, we introduce two focussed sequent calculi, LKp(T) and LK+(T), that are based on Miller-Liang's LKF system for polarised classical logic. The novelty is that those sequent calculi integrate the possibility to call a decision procedure for some background theory T, and the possibility to polarise literals "on the fly" during proof-search. These features are used in our other works to simulate the DPLL(T) procedure as proof-search in the extension of LKp(T) with a cut-rule. In this report we therefore prove cut-elimination in LKp(T). Contrary to what happens in the empty theory, the polarity of literals affects the provability of formulae in presence of a theory T. On the other hand, changing the polarities of connectives does not change the provability of formulae, only the shape of proofs. In order to prove this, we introduce a second sequent calculus, LK+(T) that extends LKp(T) with a relaxed focussing discipline, but we then show an encoding of LK+(T) back into the more restrictive system LK(T). We then prove completeness of LKp(T) (and therefore of LK+(T)) with respect to first-order reasoning modulo the ground propositional lemmas of the background theory T .

cs.LO↗
arXiv2012

Two simulations about DPLL(T)

In this paper we relate different formulations of the DPLL(T) procedure. The first formulation is based on a system of rewrite rules, which we denote DPLL(T). The second formulation is an inference system of, which we denote LKDPLL(T). The third formulation is the application of a standard proof-search mechanism in a sequent calculus LKp(T) introduced here. We formalise an encoding from DPLL(T) to LKDPLL(T) that was, to our knowledge, never explicitly given and, in the case where DPLL(T) is extended with backjumping and Lemma learning, never even implicitly given. We also formalise an encoding from LKDPLL(T) to LKp(T), building on Ivan Gazeau's previous work: we extend his work in that we handle the "-modulo-Theory" aspect of SAT-modulo-theory, by extending the sequent calculus to allow calls to a theory solver (seen as a blackbox). We also extend his work in that we handle advanced features of DPLL such as backjumping and Lemma learning, etc. Finally, we re fine the approach by starting to formalise quantitative aspects of the simulations: the complexity is preserved (number of steps to build complete proofs). Other aspects remain to be formalised (non-determinism of the search / width of search space).

cs.LO↗