arXiv subjects

Peter Müller

Publications and source records attributed to Peter Müller.

At least 19 recordsLinked to original sources

arXiv2026

Explicitly combing hedgehogs over fields of Stufe 4

Let $K[x,y,z]=K[X,Y,Z]/(X^2+Y^2+Z^2-1)$ be the coordinate ring of the algebraic unit sphere over a field $K$. Umberto Zannier showed that there exists a matrix in $\operatorname{SL}_3(K[x,y,z])$ with first row $(x,y,z)$ for $K=\mathbb Q_p$, the field of $p$-adic numbers for an odd prime $p$, or more generally, if $-1$ is a sum of two squares in $K$. The case $K=\mathbb Q_2$ remained open and was subsequently posed and discussed by Zannier with numerous researchers, thereby bringing the problem to broader attention. In 2025, Alexey Ananyevskiy and Marc Levine showed that such a matrix exists if and only if $K$ has Stufe at most $4$, equivalently, if there exist $a,b,c,d\in K$ such that $a^2+b^2+c^2+d^2=-1$. Since $\mathbb Q_2$ has Stufe $4$, this settled Zannier's problem. Their proof is purely existential and does not provide an explicit matrix. In this note, we construct an explicit example in terms of $a,b,c,d$ and describe the computational techniques used to find it.

math.NT↗

arXiv2026

Certified Program Synthesis with a Multi-Modal Verifier

Certified program synthesis (aka vericoding) is the process of automatically generating a program, its formal specification, and a machine-checkable proof of their alignment from a natural-language description. Two challenges make vericoding difficult. First, specifications synthesised from natural language are often either too weak to be meaningful or too strong to be implementable, yet existing approaches lack systematic means to detect such defects. Second, the landscape of program verifiers is fragmented: each tool supports a particular reasoning mode -- auto-active (e.g., Dafny, Verus) or interactive (e.g., Coq, Lean) -- with its own trade-off between automation and expressivity. This forces every synthesis methodology to be tailored to a single verification paradigm, limiting the class of tasks it can handle effectively. We overcome both challenges by structuring the certified synthesis workflow around a multi-modal verifier -- a single tool combining dynamic validation, automated proofs, and interactive proof scripting in one foundational framework. We realise this idea in LeetProof, an agentic pipeline built on Velvet, a multi-modal verifier embedded in Lean. Multi-modality enables LeetProof to validate generated specifications via randomised property-based testing before any code is synthesised, decompose the synthesis task into sub-problems guided by verification conditions, and delegate residual proof obligations to frontier AI provers specialised for Lean. We evaluate LeetProof on benchmarks derived from prior work on certified synthesis. Our specification validation uncovers defects in existing reference benchmarks, and LeetProof's staged pipeline achieves a significantly higher rate of fully certified solutions than a single-mode baseline at the same budget -- consistently across two frontier LLM backends.

cs.SE↗

arXiv2026

Hyper Separation Logic (extended version)

Many important functional and security properties--including non-interference, determinism, and generalized non-interference (GNI)--are hyperproperties, i.e., properties relating multiple executions of a program. Existing separation logics allow one to reason about specific classes of hyperproperties, e.g., $\forall\forall$-hyperproperties such as non-interference and $\exists\exists$-properties such as non-determinism. However, they do not support quantifier alternation, which is for instance needed to express GNI. The only existing logic that can reason about such properties is Hyper Hoare Logic, but it does not support heap-manipulating programs and, thus, is not applicable to common imperative programs. This paper introduces Hyper Separation Logic (HSL), the first program logic that supports modular reasoning about hyperproperties with arbitrary quantifier alternation over programs that manipulate the heap. HSL generalizes Hyper Hoare Logic with a novel hyper separating conjunction that lifts the standard separating conjunction to sets of states, enabling a generalized frame rule for hyperproperties. We prove HSL sound in Isabelle/HOL and demonstrate its expressiveness for hyperproperties that lie beyond the reach of existing separation logics.

cs.PL↗

arXiv2026

Bayesian Semiparametric Multivariate Density Regression with Coordinate-Wise Predictor Selection

We propose a flexible Bayesian approach for estimating the joint density of a multivariate outcome of interest in the presence of categorical covariates. Leveraging a Gaussian copula framework, our method effectively captures the dependence structure across different coordinates of the multivariate response. The conditional (on covariates) marginal (across outcomes) distributions are modeled as flexible mixtures with shared atoms across coordinates, while the mixture weights are allowed to vary with covariates through a novel Tucker tensor factorization-based structure, which enables the identification of coordinate-specific subsets of influential covariates. In particular, we replace the traditional mode matrices with coordinate-specific random partition models on the covariate levels, offering a flexible mechanism to aggregate covariate levels that exhibit similar effects on the response. Additionally, to handle settings with many covariates, we introduce a Markov chain Monte Carlo algorithm that scales with the number of aggregated levels rather than the original levels, significantly reducing memory requirements and improving computational efficiency. We demonstrate the method's numerical performance through simulation experiments and its practical applicability through the analysis of NHANES dietary data.

stat.ME↗

arXiv2026

Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)

Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that the IVL program is correct. Soundness of such translational verifiers requires that the back-end verification is sound and that correctness of the IVL program implies correctness of the input program. Existing formalizations for translational verifiers based on separation logic target the former, but support the latter only under the strong assumption that there exists a separation logic for the input program with the same state model as the IVL. This assumption is unrealistic in practice, especially since the state model also defines the supported separation logic resources. We present the first formal framework for proving the soundness of translational separation logic verifiers with non-trivial state encodings. To be applicable to various front-ends and IVLs, our framework only assumes the existence of a homomorphic encoding relation between the front-end and IVL state models. At the core of our framework is a novel condition, backward satisfiability, which is crucial to guarantee the soundness of the front-end translation. We formalize our framework for front-end verifiers based on concurrent separation logic and separation logic IVLs, such as Raven, VeriFast, and Viper. We demonstrate its expressiveness by proving soundness for three common state encodings. Our framework and all proofs are formalized in Isabelle/HOL.

cs.PL↗

arXiv2026

A note about Jordan's bound on the size of finite linear groups

In 1878 Camille Jordan showed that every finite subgroup $G\le\text{GL}_n(\mathbb C)$ has an abelian normal subgroup $A$ such that $\lvert G/A\rvert$ is bounded in terms of $n$, but he did not give an explicit bound. An explicit bound was obtained by Blichfeldt in a series of papers beginning in 1904, using representation-theoretic methods. In 1911 Bieberbach gave a geometric proof, which is quite different from the approaches of Jordan and Blichfeldt, together with an explicit bound. Frobenius simplified this proof in the same year, and the resulting argument is still the simplest known. We present a self-contained and streamlined variant of Frobenius's argument, yielding the bound $\lvert G/A\rvert\le25^{n^2}$.

math.GR↗

arXiv2026

Return probability on Bienaym\'e-Galton-Watson trees and spectral asymptotics of sparse Erd\H{o}s-R\'enyi random graphs

We derive an upper bound for the annealed return probability of the simple random walk on supercritical Bienaym\'e-Galton-Watson trees. The bound decays subexponentially in time $t$ with $t^{1/3}$ in the exponent. It is valid for all offspring distributions with a finite first moment and is optimal whenever the offspring distribution does not exclude leaves or linear pieces in the tree. This solves completely the cases left open by Piau [Ann. Probab. 26, 1016-1040 (1998)]. A new feature of our proof is a far-reaching flexibility in the location of regions with bad isoperimetric properties in the tree. It allows to efficiently treat general offspring distributions and is gained from the joint consideration of the random tree and the random walk as it is inherent under the annealed measure. In the special case of a Poissonian offspring distribution we apply the upper bound for the annealed return probability to deduce a Lifshits tail for the empirical eigenvalue distribution of the graph Laplacian on supercritical Erd\H{o}s--R\'enyi random graphs with finite mean degree.

math.PR↗

arXiv2026

Engineering in-plane anisotropy in 2D materials via surface-bound ligands

2D materials exhibiting in-plane anisotropy enable novel functionality in electronic, optoelectronic, and photonic devices, yet their availability is generally limited to naturally-occurring low-symmetry van der Waals compounds. Here, we demonstrate an approach to structural engineering in a family of blue-emitting 2D silver phenylchalcogenide semiconductors based on steric interactions among surface-bound organic molecular ligands. By strategically halogenating specific sites of phenyl ligands, we demonstrate dramatic changes to the inorganic AgSe plane in mithrene (silver phenylselenolate, AgSePh). Density functional theory revealed pronounced in-plane electronic anisotropy for direct-gap fluorinated derivatives, while a chlorinated variant exhibited a direct-to-indirect bandgap transition. Furthermore, some fluorinated variants displayed strongly polarized absorption and luminescence, accompanied by a 10x enhancement in photoluminescence quantum yield. This work establishes a versatile approach for tailoring optoelectronic properties in hybrid semiconductors that is difficult or impossible to achieve in all-inorganic materials alone, offering new opportunities in advanced material design.

cond-mat.mtrl-sci↗

arXiv2026

A scalable non-superconducting tunnel junction technology

Tunnel junctions are one of the key elements of chip-scale microsystems serving various technologies from classical microelectronics to quantum information. Aluminium and its oxide (AlOx) have dominated cryogenic tunnel junction technology for decades due to the high quality of AlOx barriers and Al superconducting properties below 1.2 K. However, many applications require non-superconducting junctions, either standalone or in combination with superconducting technology, motivating efforts to suppress Al superconductivity through magnetic fields, doping, or proximity effects -- approaches that so far suffered from integration compatibility and scalability issues. Here, we present a CMOS-compatible normal-metal tunnel junction technology based on TiW alloy and AlOx barriers. We demonstrate wafer-scale fabrication of TiW/Al-AlOx/TiW junctions and validate their performance in Coulomb blockade thermometers operating down to 20 mK, confirming robust normal-state behavior. This TiW-based architecture offers a scalable solution for non-superconducting tunnel junctions across a broad temperature range, enabling integration into advanced cryogenic, quantum and nanoelectronic chip-level systems.

cond-mat.mes-hall↗

arXiv2025

Transitive sets of derangements in primitive actions of PSL_2(q)

Problem 8.75 of the Kourovka Notebook [10], attributed to John G. Thompson, asks the following: Suppose $G$ is a finite primitive permutation group on $\Omega$, and $\alpha$, $\beta$ are distinct points of $\Omega$. Does there exist an element $g\in G$ such that $\alpha^g=\beta$ and $g$ fixes no point of $\Omega$? A recent negative example is given in [12], where $G$ is the Steinberg triality group ${}^{3}D_{4}(2)$ acting primitively on 4,064,256 points. At present this is the only negative example known. In this note we show that almost simple primitive permutation groups with socle isomorphic to PSL_2(q) do not give negative examples.

math.GR↗

arXiv2025

A Dependent Feature Allocation Model Based on Random Fields

We introduce a flexible framework for modeling dependent feature allocations. Our approach addresses limitations in traditional nonparametric methods by directly modeling the logit-probability surface of the feature paintbox, enabling the explicit incorporation of covariates and complex but tractable dependence structures. The core of our model is a Gaussian Markov Random Field (GMRF), which we use to robustly decompose the latent field, separating a structural component based on the baseline covariates from intrinsic, unstructured heterogeneity. This structure is not a rigid grid but a sparse k-nearest neighbors graph derived from the latent geometry in the data, ensuring high-dimensional tractability. We extend this framework to a dynamic spatio-temporal process, allowing item effects to evolve via an Ornstein-Uhlenbeck process. Feature correlations are captured using a low-rank factorization of their joint prior. We demonstrate our model's utility by applying it to a polypharmacy dataset, successfully inferring latent health conditions from patient drug profiles.

stat.ME↗

arXiv2025

Toward Practical Deductive Verification: Insights from a Qualitative Survey in Industry and Academia

Deductive verification is an effective method to ensure that a given system exposes the intended behavior. In spite of its proven usefulness and feasibility in selected projects, deductive verification is still not a mainstream technique. To pave the way to widespread use, we present a study investigating the factors enabling successful applications of deductive verification and the underlying issues preventing broader adoption. We conducted semi-structured interviews with 30 practitioners of verification from both industry and academia and systematically analyzed the collected data employing a thematic analysis approach. Beside empirically confirming familiar challenges, e.g., the high level of expertise needed for conducting formal proofs, our data reveal several underexplored obstacles, such as proof maintenance, insufficient control over automation, and usability concerns. We further use the results from our data analysis to extract enablers and barriers for deductive verification and formulate concrete recommendations for practitioners, tool builders, and researchers, including principles for usability, automation, and integration with existing workflows.

cs.SE↗

arXiv2025

Monitoring Adverse Events Through Bayesian Nonparametric Clustering Across Studies

We introduce a Bayesian nonparametric inference approach for aggregate adverse event (AE) monitoring across studies. The proposed model seamlessly integrates external data from historical trials to define a relevant background rate and accommodates varying levels of covariate granularity (ranging from patient-level details to study-level aggregated summary data). Inference is based on a covariate-dependent product partition model (PPMx). A central element of the model is the ability to group experimental units with similar profiles. We introduce a pairwise similarity measure, with which we set up a random partition of experimental units with comparable covariate profiles, thereby improving the precision of AE rate estimation. Importantly, the proposed framework supports real-time safety monitoring under blinding with a seamless transition to unblinded analyses when indicated. Using one case study and simulation studies, we demonstrate the model's ability to detect safety signals and assess risk under diverse trial scenarios.

stat.ME↗

arXiv2025

The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version)

Existing program verifiers can prove advanced properties about security protocol implementations, but are difficult to scale to large codebases because of the manual effort required. We develop a novel methodology called *Diodon* that addresses this challenge by splitting the codebase into the protocol implementation (the *Core*) and the remainder (the *Application*). This split allows us to apply powerful semi-automated verification techniques to the security-critical Core, while fully-automatic static analyses scale the verification to the entire codebase by ensuring that the Application cannot invalidate the security properties proved for the Core. The static analyses achieve that by proving *I/O independence*, i.e., that the I/O operations within the Application are independent of the Core's security-relevant data (such as keys), and that the Application meets the Core's requirements. We have proved Diodon sound by first showing that we can safely allow the Application to perform I/O independent of the security protocol, and second that manual verification and static analyses soundly compose. We evaluate Diodon on two case studies: an implementation of the signed Diffie-Hellman key exchange and a large (100k+ LoC) production Go codebase implementing a key exchange protocol for which we obtained secrecy and injective agreement guarantees by verifying a Core of about 1% of the code with the auto-active program verifier Gobra in less than three person months.

cs.CR↗

arXiv2025

SIMBA -- A Bayesian Decision Framework for the Identification of Optimal Biomarker Subgroups for Cancer Basket Clinical Trials

We consider basket trials in which a biomarker-targeting drug may be efficacious for patients across different disease indications. Patients are enrolled if their cells exhibit some levels of biomarker expression. The threshold level is allowed to vary by indication. The proposed SIMBA method uses a decision framework to identify optimal biomarker subgroups (OBS) defined by an optimal biomarker threshold for each indication. The optimality is achieved through minimizing a posterior expected loss that balances estimation accuracy and investigator preference for broadly effective therapeutics. A Bayesian hierarchical model is proposed to adaptively borrow information across indications and enhance the accuracy in the estimation of the OBS. The operating characteristics of SIMBA are assessed via simulations and compared against a simplified version and an existing alternative method, both of which do not borrow information. SIMBA is expected to improve the identification of patient sub-populations that may benefit from a biomarker-driven therapeutics.

stat.AP↗

arXiv2025

Borrowing strength between unaligned binary time-series via Bayesian nonparametric rescaling of Unified Skewed Normal priors

We define a Bayesian semi-parametric model to effectively conduct inference with unaligned longitudinal binary data. The proposed strategy is motivated by data from the Human Epilepsy Project (HEP), which collects seizure occurrence data for epilepsy patients, together with relevant covariates. The model is designed to flexibly accommodate the particular challenges that arise with such data. First, epilepsy data require models that can allow for extensive heterogeneity, across both patients and time. With this regard, state space models offer a flexible, yet still analytically amenable class of models. Nevertheless, seizure time-series might share similar behavioral patterns, such as local prolonged periods of elevated seizure presence, which we refer to as "clumping". Such similarities can be used to share strength across patients and define subgroups. However, due to the lack of alignment, straightforward hierarchical modeling of latent state space parameters is not practicable. To overcome this constraint, we construct a strategy that preserves the flexibility of individual trajectories while also exploiting similarities across individuals to borrow information through a nonparametric prior. On the one hand, heterogeneity is ensured by (almost) subject-specific state-space submodels. On the other, borrowing of information is obtained by introducing a Pitman-Yor prior on group-specific probabilities for patterns of clinical interest. We design a posterior sampling strategy that leverages recent developments of binary state space models using the Unified Skewed Normal family (SUN). The model, which allows the sharing of information across individuals with similar disease traits over time, can more generally be adapted to any setting characterized by unaligned binary longitudinal data.

stat.ME↗

arXiv2025

On Euler's magic matrices of sizes $3$ and $8$

A proper Euler's magic matrix is an integer $n\times n$ matrix $M\in\mathbb Z^{n\times n}$ such that $M\cdot M^t=\gamma\cdot I$ for some nonzero constant $\gamma$, the sum of the squares of the entries along each of the two main diagonals equals $\gamma$, and the squares of all entries in $M$ are pairwise distinct. Euler constructed such matrices for $n=4$. In this work, we construct examples for $n=8$ and prove that no such matrix exists for $n=3$.

math.CO↗

arXiv2025

Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees

Rust's novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability. However, fully understanding, extracting and exploiting these guarantees is subtle and challenging: existing models for Rust's type checking either support a smaller idealised language disconnected from real-world Rust code, or come with severe limitations in terms of precise modelling of Rust borrows, composite types storing them, function signatures and loops. In this paper, we present a novel model of Rust's type-checking called Place Capability Graphs, which lifts these limitations, and which can be directly calculated from the Rust compiler's own programmatic representations and analyses. We demonstrate that our model supports over 97% of Rust functions in the most popular public crates, and show its suitability as a general-purpose basis for verification and program analysis tools by developing promising new prototype versions of the existing Flowistry and Prusti tools.

cs.PL↗