Refuting equivalence in probabilistic programs with conditioning - Chatterjee, Krishnendu; Kafshdar Goharshadi, Ehsan; Novotný, Petr; Zikelic, Dorde (31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems)
We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature.

Robust image classification with 1-Lipschitz networks - Prach, Bernd
Despite generating remarkable results in various computer vision tasks, deep learning comes with some surprising shortcomings. For example, tiny perturbations, often imperceptible to the human eye, can completely change the predictions of image classifiers. Despite a decade of research, the field has made limited progress in developing image classifiers that are both accurate and robust. This thesis aims to address this gap. As our first contribution, we aim to simplify the process of training certifiably robust image classifiers. We do this by designing a convolutional layer that does not require executing an iterative procedure in every forward pass, but relies on an explicit bound instead. We also propose a loss function that allows optimizing for a particular margin more precisely. Next, we provide an overview and comparison of various methods that create robust image classifiers by constraining the Lipschitz constant. This is important since generally longer training times and more parameters improve the performance of robust classifiers, making it challenging to determine the most practical and effective methods from existing literature. In 1-Lipschitz classification, the performance of current methods is still much worse than what we expect on the simple tasks we consider. Therefore, we next investigate potential causes of this shortcoming. We first consider the role of the activation function. We prove a theoretical shortcoming of the commonly used activation function, and provide an alternative without it. However this theoretical improvement does barely translate to the empirical performance of robust classifiers, suggesting a different bottleneck. Therefore, in the final chapter, we study how the performance depends on the amount of training data. We prove that in the worst case, we might require far more data to train a robust classifier compared to a normal one. We furthermore find that the amount of training data is a key determinant of the performance current methods achieve on popular datasets. Additionally, we show that linear subspaces exist with tiny data variance, and yet we can still train very accurate classifiers after projecting into those subspaces. This shows that on the datasets considered, enforcing robustness in classification makes the task strictly more challenging. -----------------“In reference to IEEE copyrighted material which is used with permission in this thesis, the IEEE does not endorse any of [name of university or educational entity]’s products or services. Internal or personal use of this material is permitted. If interested in reprinting/republishing IEEE copyrighted material for advertising or promotional purposes or for creating new collective works for resale or redistribution, please go to http://www.ieee.org/publications_standards/publications/rights/rights_link.html to learn how to obtain a License from RightsLink. If applicable, University Microfilms and/or ProQuest Library, or the Archives of Canada may supply single copies of the dissertation.”

Early indirect neurogenesis transitions to late direct neurogenesis in mouse cerebral cortex development - Cárdenas, Adrián; Çelik, Irem; Espinós, Alexandre; Streicher, Carmen; López-González, Lara; del-Valle-Anton, Lucia; Fernández, Virginia; Amin, Salma; Negri, Enrico; Ortuño, Eduardo Fernández; Hippenmeyer, Simon; Borrell, Víctor (bioRxiv)
The cerebral cortex must contain the appropriate numbers of neurons in each layer to acquire its proper functional organization. Accordingly, neurogenesis requires precise regulation along development. Cortical neurons are made either directly by Radial Glia Cells (RGCs) that self- consume, or indirectly from RGCs via Intermediate Progenitor Cells (IPCs) and largely preserving the RGC pool. According to the standing model of cortical development, Direct Neurogenesis predominates at early stages of development, and progressively shifts to Indirect Neurogenesis, which predominates at late stages. However, neurogenesis at early stages should be compatible with RGC amplification, and neurogenesis at late stages needs to involve RGC consumption, which seems in conflict with the standing model. Here we studied the modes of neurogenesis along cortical development using multiple approaches, including birthdating, live imaging and MADM clone labeling. Contrary to the established dogma, our data show that Indirect Neurogenesis clearly predominates at early developmental stages, gradually shifting to Direct Neurogenesis at late stages. These findings challenge the current model of cortical neurogenesis, and prompt a re-evaluation of previous and ongoing work about the genetic and molecular mechanisms regulating this process.

Sound statistical model checking for probabilities and expected rewards (experimental reproduction package) - Budde, Carlos; Hartmanns, Arnd; Meggendorfer, Tobias; Weininger, Maximilian; Wienhöft, Patrick
Artifact to reproduce the experimental results presented in the article "Sound Statistical Model Checking for Probabilities and Expected Rewards" by Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft (TACAS 2025). The contents include all data and software (formal models, software tools, Python & bash scripts) used in the experimental evaluation presented in sections 3, 4, and 6 of the article. Detailed instructions on how to reproduce the results are bundled in the artifact.

Artifact: Fixed point certificates for reachability and expected rewards in MDPs - Chatterjee, Krishnendu; Quatmann, Tim; Schäffeler, Maximilian; Weininger, Maximilian; Winkler, Tobias; Zilken, Daniel
This artifact allows to review and reproduce the Isabelle proofs and practical experiments from the paper *Fixed Point Certificates for Reachability and Expected Rewards in MDPs*. The contents are two-fold: First, the artifact contains a formally verified certificate checker for the certificates presented in the paper. The formal Isabelle/HOL proofs of the background theory can be inspected, checked by Isabelle and the code extraction can be retraced. Second, the artifact contains a modified version of the model checking tool `Storm` with support for certificate generation. Together with the provided scripts and benchmark files, this allows to reproduce the experiments from the paper. An appropriate subset of the experiments is given to allow a review in a timely manner. In addition, original logfiles from our experiments are provided, allowing a detailed inspection. The package includes convenient installation scripts for [the TACAS 2023 VM](https://doi.org/10.5281/zenodo.7113223) (based on Ubuntu 22.04). A native installation on Linux or macOS systems (including the newer ARM-based machines) is also possible.

Optimal sums of three cubes in Fq[t] - Browning, Timothy D; Glas, Jakob; Wang, Victor (Mathematische Zeitschrift)
We use the circle method to prove that a density 1 of elements in Fq[t] are representable as a sum of three cubes of essentially minimal degree from Fq[t], assuming the Ratios Conjecture and that char(Fq)>3. Roughly speaking, to do so, we upgrade an order of magnitude result to a full asymptotic formula that was conjectured by Hooley in the number field setting.

Adeno-associated viral tools to trace neural development and connectivity across amphibians - Jaeger, Eliza C.B.; Vijatovic, David; Deryckere, Astrid; Zorin, Nikol; Nguyen, Akemi L.; Ivanian, Georgiy; Woych, Jamie; Arnold, Rebecca C; Ortega Gurrola, Alonso; Shvartsman, Arik; Barbieri, Francesca; Toma, Florina-Alexandra; et al. (Developmental Cell)
Amphibians, by virtue of their phylogenetic position, provide invaluable insights on nervous system evolution, development, and remodeling. The genetic toolkit for amphibians, however, remains limited. Recombinant adeno-associated viral vectors (AAVs) are a powerful alternative to transgenesis for labeling and manipulating neurons. Although successful in mammals, AAVs have never been shown to transduce amphibian cells efficiently. We screened AAVs in three amphibian species—the frogs Xenopus laevis and Pelophylax bedriagae and the salamander Pleurodeles waltl—and identified at least two AAV serotypes per species that transduce neurons. In developing amphibians, AAVs labeled groups of neurons generated at the same time during development. In the mature brain, AAVrg retrogradely traced long-range projections. Our study introduces AAVs as a tool for amphibian research, establishes a generalizable workflow for AAV screening in new species, and expands opportunities for cross-species comparisons of nervous system development, function, and evolution.

Multiplicative auction algorithm for approximate maximum weight bipartite matching - Zheng, Da Wei; Henzinger, Monika H (Mathematical Programming)
We present an auction algorithm using multiplicative instead of constant weight updates to compute a (1-E)-approximate maximum weight matching (MWM) in a bipartite graph with n vertices and m edges in time 0(mE-1), beating the running time of the fastest known approximation algorithm of Duan and Pettie [JACM ’14] that runs in 0(mE-1 log E-1). Our algorithm is very simple and it can be extended to give a dynamic data structure that maintains a (1-E)-approximate maximum weight matching under (1) one-sided vertex deletions (with incident edges) and (2) one-sided vertex insertions (with incident edges sorted by weight) to the other side. The total time time used is 0(mE-1), where m is the sum of the number of initially existing and inserted edges.

Mesoscopic eigenvalue statistics for Wigner-type matrices - Riabov, Volodymyr (Annales de l'institut Henri Poincare (B) Probability and Statistics)
We prove a universal mesoscopic central limit theorem for linear eigenvalue statistics of a Wigner-type matrix inside the bulk of the spectrum with compactly supported twice continuously differentiable test functions. The main novel ingredient is an optimal local law for the two-point function $T(z,ζ)$ and a general class of related quantities involving two resolvents at nearby spectral parameters.

A new varifold solution concept for mean curvature flow: Convergence of the Allen-Cahn equation and weak-strong uniqueness - Hensel, Sebastian; Laux, Tim (Journal of Differential Geometry)
We propose a new weak solution concept for (two-phase) mean curvature flow which enjoys both (unconditional) existence and (weak-strong) uniqueness properties. These solutions are evolving varifolds, just as in Brakke's formulation, but are coupled to the phase volumes by a simple transport equation. First, we show that, in the exact same setup as in Ilmanen's proof [J. Differential Geom. 38, 417-461, (1993)], any limit point of solutions to the Allen-Cahn equation is a varifold solution in our sense. Second, we prove that any calibrated flow in the sense of Fischer et al. [arXiv:2003.05478] - and hence any classical solution to mean curvature flow-is unique in the class of our new varifold solutions. This is in sharp contrast to the case of Brakke flows, which a priori may disappear at any given time and are therefore fatally non-unique. Finally, we propose an extension of the solution concept to the multi-phase case which is at least guaranteed to satisfy a weak-strong uniqueness principle.
Keywords: Mean curvature flow; gradient flows; varifolds; weak solutions; weak-strong uniqueness; calibrated geometry; gradient-flow calibrations

Generalized minimum 0-extension problem and discrete convexity - Dvorak, Martin; Kolmogorov, Vladimir (Mathematical Programming)
Given a fixed finite metric space (V,μ), the {\em minimum 0-extension problem}, denoted as 0-Ext[μ], is equivalent to the following optimization problem: minimize function of the form minx∈Vn∑ifi(xi)+∑ijcijμ(xi,xj) where cij,cvi are given nonnegative costs and fi:V→R are functions given by fi(xi)=∑v∈Vcviμ(xi,v). The computational complexity of 0-Ext[μ] has been recently established by Karzanov and by Hirai: if metric μ is {\em orientable modular} then 0-Ext[μ] can be solved in polynomial time, otherwise 0-Ext[μ] is NP-hard. To prove the tractability part, Hirai developed a theory of discrete convex functions on orientable modular graphs generalizing several known classes of functions in discrete convex analysis, such as L♮-convex functions. We consider a more general version of the problem in which unary functions fi(xi) can additionally have terms of the form cuv;iμ(xi,{u,v}) for {u,v}∈F, where set F⊆(V2) is fixed. We extend the complexity classification above by providing an explicit condition on (μ,F) for the problem to be tractable. In order to prove the tractability part, we generalize Hirai's theory and define a larger class of discrete convex functions. It covers, in particular, another well-known class of functions, namely submodular functions on an integer lattice. Finally, we improve the complexity of Hirai's algorithm for solving 0-Ext on orientable modular graphs.
Keywords: minimum 0-extension problem; metric labeling problem; discrete metric spaces; metric extensions; computational complexity; valued constraint satisfaction problems; discrete convex analysis; L-convex functions

EvoPress: Accurate dynamic model compression via evolutionary search - Sieberling, Oliver; Kuznedelev, Denis; Kurtic, Eldar; Alistarh, Dan-Adrian (42nd International Conference on Machine Learning)
The high computational costs of large language models (LLMs) have led to a flurry of research on LLM compression, via methods such as quantization, sparsification, or structured pruning. A new frontier in this area is given by dynamic, non-uniform compression methods, which adjust the compression levels (e.g., sparsity) per-block or even per-layer in order to minimize accuracy loss, while guaranteeing a global compression threshold. Yet, current methods rely on estimating the "importance" of a given layer, implicitly assuming that layers contribute independently to the overall compression error. We begin from the motivating observation that this independence assumption does not generally hold for LLM compression: pruning a model further may even significantly recover performance. To address this, we propose EvoPress, a novel evolutionary framework for dynamic LLM compression. By formulating dynamic compression as a general optimization problem, EvoPress identifies optimal compression profiles in a highly efficient manner, and generalizes across diverse models and compression techniques. Via EvoPress, we achieve state-of-the-art performance for dynamic compression of Llama, Mistral, and Phi models, setting new benchmarks for structural pruning (block/layer dropping), unstructured sparsity, and quantization with dynamic bitwidths.

Layer-wise quantization for quantized optimistic dual averaging - Nguyen, Anh Duc; Markov, Ilia; Wu, Frank Zhengqing; Ramezani-Kebrya, Ali; Antonakopoulos, Kimon; Alistarh, Dan-Adrian; Cevher, Volkan (42nd International Conference on Machine Learning)
Modern deep neural networks exhibit heterogeneity across numerous layers of various types such as residuals, multi-head attention, etc., due to varying structures (dimensions, activation functions, etc.), distinct representation characteristics, which impact predictions. We develop a general layer-wise quantization framework with tight variance and code-length bounds, adapting to the heterogeneities over the course of training. We then apply a new layer-wise quantization technique within distributed variational inequalities (VIs), proposing a novel Quantized Optimistic Dual Averaging (QODA) algorithm with adaptive learning rates, which achieves competitive convergence rates for monotone VIs. We empirically show that QODA achieves up to a 150% speedup over the baselines in end-to-end training time for training Wasserstein GAN on 12+GPUs.

Sets with arbitrary Hausdorff and packing scales in infinite dimensional Banach spaces - Helfter, Mathieu (Journal of Fractal Geometry)
For every couple of Hausdorff functions ψ and φ verifying some mild assumptions, there exists a compact subset K of the Baire space such that the φ-Hausdorff measure and the ψ-packing measure on K are both finite and positive. Such examples are then embedded in any infinite dimensional Banach space to answer positively a question of Fan on the existence of metric spaces with arbitrary scales.

Space-deniable proofs - Dujmovic, Jesko; Günther, Christoph Ullrich; Pietrzak, Krzysztof Z (23rd International Conference on Theory of Cryptography)
We introduce and construct a new proof system called Non-interactive Arguments of Knowledge or Space (NArKoS), where a space-bounded prover can convince a verifier they know a secret, while having access to sufficient space allows one to forge indistinguishable proofs without the secret. An application of NArKoS are space-deniable proofs, which are proofs of knowledge (say for authentication in access control) that are sound when executed by a lightweight device like a smart-card or an RFID chip that cannot have much storage, but are deniable (in the strong sense of online deniability) as the verifier, like a card reader, can efficiently forge such proofs. We construct NArKoS in the random oracle model using an OR-proof combining a sigma protocol (for the proof of knowledge of the secret) with a new proof system called simulatable Proof of Transient Space (simPoTS). We give two different constructions of simPoTS, one based on labelling graphs with high pebbling complexity, a technique used in the construction of memory-hard functions and proofs of space, and a more practical construction based on the verifiable space-hard functions from TCC’24 where a prover must compute a root of a sparse polynomial. In both cases, the main challenge is making the proofs efficiently simulatable.

Zeroizing attacks against evasive and circular evasive LWE - Agrawal, Shweta; Modi, Anuja; Yadav, Anshu; Yamada, Shota (23rd International Conference on Theory of Cryptography)
We develop new attacks against the Evasive LWE family of assumptions, in both the public and private-coin regime. To the best of our knowledge, ours are the first attacks against Evasive LWE in the public-coin regime, for any instantiation from the family. Our attacks are summarized below. Public-Coin Attacks. 1.The recent work by Hseih, Lin and Luo [17] constructed the first Attribute Based Encryption (ABE) for unbounded depth circuits by relying on the “circular” evasive LWE assumption. This assumption has been popularly considered as a safe, public-coin instance of Evasive LWE in contrast to its “private-coin” cousins (for instance, see [10, 11]). We provide the first attack against this assumption, challenging the widely held belief that this is a public-coin assumption. 2. We demonstrate a counter-example against vanilla public-coin evasive LWE by Wee [26] in an unnatural parameter regime. Our attack crucially relies on the error in the pre-condition being larger than the error in the post-condition, necessitating a refinement of the assumption. Private-Coin Attacks. 1. The recent work by Agrawal, Kumari and Yamada [2] constructed the first functional encryption scheme for pseudorandom functionalities (PRFE) and extended this to obfuscation for pseudorandom functionalities (PRIO) [4] by relying on private-coin evasive LWE. We provide a new attack against the assumption stated in the first posting of their work (subsequently refined to avoid these attacks). 2. The recent work by Branco et al. [8] (concurrently to [4]) provides a construction of obfuscation for pseudorandom functionalities by relying on private-coin evasive LWE. We provide a new attack against their stated assumption. 3. Branco et al. [8] showed that there exist contrived, “self-referential” classes of pseudorandom functionalities for which pseudorandom obfuscation cannot exist. We extend their techniques to develop an analogous result for pseudorandom functional encryption. While Evasive LWE was developed to specifically avoid “zeroizing attacks”, our work shows that in certain settings, such attacks can still apply.

Constrained verifiable random functions without obfuscation and friends - Brandt, Nicholas; Cueto Noval, Miguel; Günther, Christoph Ullrich; Ünal, Akin; Wohnig, Stella (23rd International Conference on Theory of Cryptography)
CVRFs are PRFs that unify the properties of verifiable and constrained PRFs. Since they were introduced concurrently by Fuchsbauer and Chandran-Raghuraman-Vinayagamurthy in 2014, it has been an open problem to construct CVRFs without using heavy machinery such as multilinear maps, obfuscation or functional encryption. We solve this problem by constructing a prefix-constrained verifiable PRF that does not rely on the aforementioned assumptions. Essentially, our construction is a verifiable version of the Goldreich-Goldwasser-Micali PRF. To achieve verifiability we leverage degree-2 algebraic PRGs and bilinear groups. In short, proofs consist of intermediate values of the Goldreich-Goldwasser-Micali PRF raised to the exponents of group elements. These outputs can be verified using pairings since the underlying PRG is of degree 2. We prove the selective security of our construction under the Decisional Square Diffie-Hellman (DSDH) assumption and a new assumption, which we dub recursive Decisional Diffie-Hellman (recursive DDH). We prove the soundness of recursive DDH in the generic group model assuming the hardness of the Multivariate Quadratic (MQ) problem and a new variant thereof, which we call MQ+. Last, in terms of applications, we observe that our CVRF is also an exponent (C)VRF in the plain model. Exponent VRFs were recently introduced by Boneh et al. (Eurocrypt’25) with various applications to threshold cryptography in mind. In addition to that, we give further applications for prefix-CVRFs in the blockchain setting, namely, stake-pooling and compressible randomness beacons.

Rolling at right angles: Magnetic anisotropy enables dual-anisotropic active matter - Fitzgerald, Eavan; Clavaud, Cécile; Das, Debasish; Lenton, Isaac C; Waitukaitis, Scott R (Physical Review E)
We report on an experimental active matter system with motion restricted to four cardinal directions. Our particles are magnetite-doped colloidal spheres driven by the Quincke electrorotational instability. The absence of a magnetic field (|𝑩|=0) leads to circular trajectories interspersed with short spontaneous runs. Intermediate fields (|𝑩|≲20mT) linearize the motion along the axis perpendicular to 𝑩. At high magnetic fields, we observe the surprising emergence of a second, distinct linearization along the axis parallel to 𝑩. With numerical simulations, we show that this behavior can be explained by anisotropic magnetic susceptibility.

Mutation–selection–drift balance models of complex diseases - Berg, Jeremy J.; Li, Xinyi; Riall, Kellen; Hayward, Laura; Sella, Guy (Genetics)
Genetic variation that influences complex disease susceptibility is introduced into the population by mutation and removed by natural selection and genetic drift. This mutation–selection–drift balance (MSDB) shapes the prevalence of a disease and its genetic architecture. To date, however, MSDB has been modeled only for monogenic (Mendelian) diseases. Here, we develop an MSDB model for complex disease susceptibility: we assume that genotype relates to disease risk according to the canonical liability threshold model and that the selection on variants affecting risk stems from the fitness cost of the disease. We focus on diseases that are highly polygenic, entail a substantial fitness cost, and are neither extremely common in the population nor exceedingly rare. The comparison of model predictions with genome-wide association studies and other observations in humans indicates that common genetic variation affecting complex disease susceptibility is little affected by directional selection and instead shaped by pleiotropic stabilizing selection on other traits. In turn, directional selection may exert a more substantial effect on rare, large-effect variants. Our results also suggest that current estimates of disease heritability are likely biased. The model thus provides a better understanding of the evolutionary processes that shape the architecture and prevalence of complex diseases.

Class numbers and integer points on some Pellian surfaces - Diao, Yijie (Journal de theorie des nombres de Bordeaux)
We provide an estimate for the number of nontrivial integer points on the Pellian surface t^2 - du^2 = 1 in a bounded region. We give a lower bound on the size of fundamental solutions for almost all d in a certain class, based on a recent conjecture of Browning and Wilsch about integer points on log K3 surfaces. We also obtain an upper bound on the average of class number in this class, assuming the same conjecture.