arXiv subjects

Omar Muhammad

Publications and source records attributed to Omar Muhammad.

3 recordsLinked to original sources

arXiv2026

Mask2Cause: Causal Discovery via Adjacency Constrained Causal Attention

Leveraging deep learning for causal discovery in time series remains challenging because existing neural methods predominantly rely on component-wise architectures that fail to capture shared system dynamics or employ decoupled post-hoc graph extraction that risks overfitting to spurious correlations. We propose $\textbf{Mask2Cause}$, an end-to-end framework that recovers the underlying causal graph directly during the forecasting forward pass. Our approach introduces an Inverted Variable Embedding and an Adjacency-Constrained Masked Attention mechanism, trained with homoscedastic or heteroscedastic objectives to capture causal influences in both mean and variance. Empirical results on diverse benchmarks, from synthetic chaotic dynamics to realistic biological simulations, demonstrate state-of-the-art causal discovery with significantly reduced parameter complexity compared to standard baselines. We further show that inferred causal structures can be used to reduce parameter count of forecasting models by more than 70% on average while maintaining predictive accuracy.

cs.LG↗

arXiv2026

Verification Modulo Tested Library Contracts

We consider the problem of verification modulo tested library contracts as a step towards automating the verification of client programs that use complex libraries. We formulate this problem as the synthesis of modular contracts for the library methods used by the client that are adequate to prove the client correct, and that also pass the scrutiny of a testing engine that tests the library against these contracts. We also consider a new form of method contracts called contextual contracts that arise in this setting that hold in the context of the client program, and can often be simpler and easier to infer than classical modular contracts. We provide a counterexample-guided learning framework to solve this problem, in which the synthesizer interacts with a constraint solver as well as the testing engine in order to infer adequate modular/contextual method contracts and inductive invariants for the client. The main synthesis engines we use are generalizing CHC solvers that are realized using ICE learning algorithms. We realize this framework in a tool called DUALIS and show its efficacy on benchmarks where clients call large libraries.

cs.PL↗

arXiv2025

Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic

Neither the classical nor intuitionistic logic traditions are perfectly aligned with the purpose of reasoning about computation, as neither can permit unconstrained recursive definitions without inconsistency: recursive definitions must normally be proven terminating before admission and use. Grounded arithmetic or GA is a formal-reasoning foundation allowing direct expression of arbitrary recursive definitions. GA adjusts traditional inference rules so that terms that express nonterminating computations harmlessly denote no semantic value ($\bot$) instead of yielding inconsistency. Recursive functions are proven terminating in GA essentially by "dynamically typing" terms, or equivalently, symbolically reverse-executing the computations they denote via inference rules. Once recursive functions have been proven terminating, logical reasoning about them reduces to familiar classical rules. We summarize the development and lessons learned from two mechanically-checked formulations of GA, finding both syntactically consistent and semantically sound with respect to an underlying computable model. Propositional grounded arithmetic or PGA is a quantifier-free system for inductive grounded reasoning about open formulas. PGA has logical expressiveness comparable to Skolem's PRA, but has general-recursive (Turing-complete) functional expressiveness. PGA builds upon a simpler system of basic grounded arithmetic or BGA, which omits logical operators entirely. BGA and PGA are not only sound but semantically complete, a combination impossible for powerful classical systems with arithmetic, due to G\"odel's incompleteness theorems. These results suggest that powerful and consistent formal reasoning with unconstrained recursive definitions is possible, potentially enabling new computation-centric formal languages, proof assistants, and type systems in the future.

cs.PL↗