arXiv subjects

Karen Sargsyan

Publications and source records attributed to Karen Sargsyan.

7 recordsLinked to original sources

arXiv2026

Structural Enforcement of Statistical Rigor in AI-Driven Discovery: A Functional Architecture

AI-Scientist systems risk manufacturing spurious discoveries through uncontrolled multiple testing. We present a functional architecture that enforces statistical rigor at two levels: a Haskell embedded domain-specific language (the Research monad) that makes it impossible to test a hypothesis without updating the error budget, and a declarative scaffold that fixes the data flow and the statistical test, together with an OS-level sandbox that makes validation data physically absent from the environment in which LLM-generated code runs. We treat FDR control as a formal requirement and trace it to the implementation. We ground the design in a machine-checked Lean~4 formalization of LORD online false-discovery-rate (FDR) control: we derive its error budget and prove marginal FDR control, and full FDR control when thresholds do not adapt to earlier rejections. We then verify in SPARK/Ada that the LORD thresholds, computed in IEEE~754 arithmetic, never exceed the available wealth, given a margin condition that our configurations meet by a factor of at least eight; without a margin the property fails. To our knowledge this is the first machine-checked proof of an online FDR control theorem. In simulation, the architecture holds the false discovery rate near 1\% against a 5\% target, where a naive approach reaches 41\%. In end-to-end case studies, a valid test avoids the false discoveries a flawed one produces, yet still finds real effects when the data allow. An adversarial evaluation confirms that, inside the sandbox, generated code cannot read the held-out data even when given its exact path.

cs.SE↗

arXiv2026

Position: The Inevitable Transition to Machine Learning in Quantum Chemistry

Finding exact solutions to the quantum many-body problem is computationally intractable (QMA-hard). Traditional approximations for electrons in an atom or molecule -- density functional theory and wavefunction methods -- have been indispensable, but their development shows signs of saturation: DFT functionals have proliferated without converging toward the exact functional, and strong correlation remains largely unsolved after decades of effort. This position paper argues that machine learning represents the most promising path forward -- not as a proof of logical necessity, but as a decision-theoretic argument: ML succeeds whether the underlying problems are truly hard or merely lack simple analytical solutions. We reframe recent traditional method development as ``hand-crafted machine learning'' that has exhausted the hypothesis space accessible to human intuition. Significant challenges remain, but these have clear research paths forward, unlike the fundamental barriers facing traditional approaches. ML-based approaches merit strategic priority in quantum chemistry's next phase.

physics.chem-ph↗

arXiv2026

A cubical formalisation of topos causal models: intervention, forcing, and a contextuality obstruction

Topos causal models recast causal inference inside a topos: a causal world is a presheaf, an intervention is a sub-model named by a characteristic map into the subobject classifier $\Om$, and reasoning is Kripke-Joyal forcing in an intuitionistic internal language. We give the first axiom-free machine-checked account of this 1-topos core, in Cubical Agda over a previously verified probability monad and do-calculus; the framework is otherwise developed on paper, with central claims stated rather than proved. Three of our results go beyond faithful transcription. We exhibit a contextuality obstruction the programme does not treat: pairwise-consistent local causal data with no global model, detected by a degree-one holonomy class. We delimit the claim that interventions are modelled by the subobject classifier: an intervention and an observation name the same subobject, so $\Om$ fixes the target of a do-operation but not the operation itself, which is surgery on the kernels --- where, on a confounder, the interventional and observational laws differ. And we settle the modal unit --- inflationarity is derivable from $j\top = \top$ and naturality, not a fourth axiom. We also machine-check the classifier of sieves with its classification theorem, the pullback collating local mechanisms, and the Kripke-Joyal forcing clauses. The development assumes no axioms and typechecks under Agda's \texttt{--safe} flag, with the ordered field discharged at $\mathbb{Q}$; type-level sheafification and a directed do-calculus are future work.

cs.LO↗

arXiv2026

Localizing Preference Aggregation Conflicts: A Graph-Theoretic Approach Using Sheaves

We introduce a graph-theoretic framework based on discrete sheaves to diagnose and localize inconsistencies in preference aggregation and, more broadly, in the fusion of partial rankings supplied by many overlapping sources. Unlike linearization methods such as HodgeRank, which embed comparisons into a numerical flow, this approach stays purely ordinal and locates conflict in the interaction structure via the Obstruction Locus, identifying which voter pairs fail to cohere. We formalize the Incompatibility Index to quantify these local conflicts and examine their behavior under stochastic variations using the Mallows model. We further develop a sheaf-theoretic pushforward operation to model voter merging, implemented via a polynomial-time constraint digraph algorithm. We demonstrate that graph quotients transform distributed edge conflicts into local impossibilities (empty stalks), showing topologically how aggregation paradoxes can persist across scales.

econ.TH↗

arXiv2026

A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness

The standard convex-algebra interchange axiom, common to probability-monad formalisations since Stone, is provably too weak to support full Bayesian conditioning. We make this precise in Cubical Agda: finite distributions as a higher inductive type, conditional independence as a cubical path between kernels, recursive Bayesian conditioning as a total function on a full-support fragment. Lifting conditioning to the full HIT exposes a structural mismatch -- the two halves of the rearranged 4-leaf mix carry distinct Bayesian weights related by Bayes' formula, not the single shared inner weight the standard axiom provides. We exhibit the minimal generalisation that resolves this and prove the standard form is the degenerate case where the two inner weights coincide. Around this observation we verify the algebraic context constructively, with zero postulates above an abstract ordered-field interface: bind commutativity, the four semi-graphoid axioms, intersection (reduced to contraction via structural $Σ$-witnesses, without positivity), Pearl's do-calculus Rules~1, 2, and~3 in kernel form, finite-type Bayesian conditioning, and the soundness of Pearl's d-separation theorem on arbitrary finite directed acyclic graphs (DAGs) -- in interventional form for multi-element $X$, $Y$, $Z$, and in Bayesian form for the elementary patterns. The probability monad is also verified as a Markov category; the abstract interface discharges at $\mathbb{Q}$.

cs.LO↗

arXiv2026

Functorial Neural Architectures from Higher Inductive Types

Neural networks often learn the parts of a task but fail on novel combinations of those parts. We argue that this failure is architectural: a decoder generalizes compositionally only when it respects the algebraic laws of the task, i.e. when it descends from freely generated sequences to the quotient determined by those laws. We make this principle constructive by compiling Higher Inductive Type (HIT) specifications into neural architectures. Basepoints, path constructors, and 2-cells are mapped to base constraints, generator networks, structural concatenation, and learned homotopies. The resulting transport decoders are strict monoidal functors by construction: decoding a concatenated word is concatenation of independently generated loop segments. In contrast, we prove that softmax self-attention cannot simultaneously satisfy strict monoidal composition and descent to any non-trivial compositional quotient. Experiments on the torus, wedge of circles, and Klein bottle validate the predicted hierarchy: functorial decoders outperform non-functorial alternatives by $2$--$10\times$, and a learned 2-cell closes a $46\%$ error gap precisely on words exercising the Klein-bottle relation. These results suggest that compositional generalization should be enforced as functorial structure in the architecture, rather than learned from examples alone.

cs.LG↗

arXiv2023

Combinatorial Convolutional Neural Networks for Words

The paper discusses the limitations of deep learning models in identifying and utilizing features that remain invariant under a bijective transformation on the data entries, which we refer to as combinatorial patterns. We argue that the identification of such patterns may be important for certain applications and suggest providing neural networks with information that fully describes the combinatorial patterns of input entries and allows the network to determine what is relevant for prediction. To demonstrate the feasibility of this approach, we present a combinatorial convolutional neural network for word classification.

cs.LG↗