arXiv subjects

Christian Schilling

Publications and source records attributed to Christian Schilling.

At least 37 records · Page 2Linked to original sources

arXiv2025

In Search of Trees: Decision-Tree Policy Synthesis for Black-Box Systems via Search

Decision trees, owing to their interpretability, are attractive as control policies for (dynamical) systems. Unfortunately, constructing, or synthesising, such policies is a challenging task. Previous approaches do so by imitating a neural-network policy, approximating a tabular policy obtained via formal synthesis, employing reinforcement learning, or modelling the problem as a mixed-integer linear program. However, these works may require access to a hard-to-obtain accurate policy or a formal model of the environment (within reach of formal synthesis), and may not provide guarantees on the quality or size of the final tree policy. In contrast, we present an approach to synthesise optimal decision-tree policies given a deterministic black-box environment and specification, a discretisation of the tree predicates, and an initial set of states, where optimality is defined with respect to the number of steps to achieve the goal. Our approach is a specialised search algorithm which systematically explores the (exponentially large) space of decision trees under the given discretisation. The key component is a novel trace-based pruning mechanism that significantly reduces the search space. Our approach represents a conceptually novel way of synthesising small decision-tree policies with optimality guarantees even for black-box environments with black-box specifications.

cs.AI↗

arXiv2024

Ground and Excited States from Ensemble Variational Principles

The extension of the Rayleigh-Ritz variational principle to ensemble states $ρ_{\mathbf{w}}\equiv\sum_k w_k |Ψ_k\rangle \langleΨ_k|$ with fixed weights $w_k$ lies ultimately at the heart of several recent methodological developments for targeting excitation energies by variational means. Prominent examples are density and density matrix functional theory, Monte Carlo sampling, state-average complete active space self-consistent field methods and variational quantum eigensolvers. In order to provide a sound basis for all these methods and to improve their current implementations, we prove the validity of the underlying critical hypothesis: Whenever the ensemble energy is well-converged, the same holds true for the ensemble state $ρ_{\mathbf{w}}$ as well as the individual eigenstates $|Ψ_k\rangle$ and eigenenergies $E_k$. To be more specific, we derive linear bounds $d_-Δ{E}_{\mathbf{w}} \leq ΔQ \leq d_+ Δ{E}_{\mathbf{w}}$ on the errors $ΔQ $ of these sought-after quantities. A subsequent analytical analysis and numerical illustration proves the tightness of our universal inequalities. Our results and particularly the explicit form of $d_{\pm}\equiv d_{\pm}^{(Q)}(\mathbf{w},\mathbf{E})$ provide valuable insights into the optimal choice of the auxiliary weights $w_k$ in practical applications.

quant-ph↗

arXiv2024

The Reachability Problem for Neural-Network Control Systems

A control system consists of a plant component and a controller which periodically computes a control input for the plant. We consider systems where the controller is implemented by a feedforward neural network with ReLU activations. The reachability problem asks, given a set of initial states, whether a set of target states can be reached. We show that this problem is undecidable even for trivial plants and fixed-depth neural networks with three inputs and outputs. We also show that the problem becomes semi-decidable when the plant as well as the input and target sets are given by automata over infinite words.

cs.LG↗

arXiv2024

Efficient Shield Synthesis via State-Space Transformation

We consider the problem of synthesizing safety strategies for control systems, also known as shields. Since the state space is infinite, shields are typically computed over a finite-state abstraction, with the most common abstraction being a rectangular grid. However, for many systems, such a grid does not align well with the safety property or the system dynamics. That is why a coarse grid is rarely sufficient, but a fine grid is typically computationally infeasible to obtain. In this paper, we show that appropriate state-space transformations can still allow to use a coarse grid at almost no computational overhead. We demonstrate in three case studies that our transformation-based synthesis outperforms a standard synthesis by several orders of magnitude. In the first two case studies, we use domain knowledge to select a suitable transformation. In the third case study, we instead report on results in engineering a transformation without domain knowledge.

cs.LO↗

arXiv2024

Quantum Information-Assisted Complete Active Space Optimization (QICAS)

Automated active space selection is arguably one of the most challenging and essential aspects of multiconfigurational methods. In this work we propose an effective quantum information-assisted complete active space optimization (QICAS) scheme. What sets QICAS apart from other correlation-based selection schemes is (i) the use of unique measures from quantum information that assess the correlation in electronic structures in an unambiguous and predictive manner, and (ii) an orbital optimization step that minimizes the correlation discarded by the active space approximation. Equipped with these features QICAS yields for smaller correlated molecules sets of optimized orbitals with respect to which the CASCI energy reaches the corresponding CASSCF energy within chemical accuracy. For more challenging systems such as the Chromium dimer, QICAS offers an excellent starting point for CASSCF by greatly reducing the number of iterations required for numerical convergence. Accordingly, our study validates a profound empirical conjecture: the energetically optimal non-active spaces are predominantly those that contain the least entanglement.

quant-ph↗

arXiv2024

Refining the weighted subspace-search variational quantum eigensolver: compression of ansätze into a single pure state and optimization of weights

The weighted subspace-search variational quantum eigensolver (SSVQE) is a prominent algorithm for calculating excited-state properties of molecular quantum systems. In this work, we elaborate on some of its fundamental features with the aim of improving its practical realization. First, we demonstrate that the initial ansätze for various excited states could be prepared into a single pure state through a minimal number of ancilla qubits, followed by the optimization of a subsequent global unitary rotation in the targeted subspace. Since the ancillas' sole purpose is to purify an underlying ensemble $ρ_{\boldsymbol{w}}$ state with spectral weights $\boldsymbol{w}$, their measurement would just collapse $ρ_{\boldsymbol{w}}$ with probabilities $w_j$ to one of its eigenstates $|Ψ_j \rangle$. We thus observe that our realization of SSVQE is equivalent to the original SSVQE improved by importance sampling. Then, we elaborate by numerical means on the potential influence of the auxiliary weights $\boldsymbol{w}$ on the accuracy of the sought-after eigenstates and eigenenergies. Clear trends are discovered which are contrasted with some recent mathematical results concerning the ensemble variational principle that underlies SSVQE.

quant-ph↗

arXiv2024

Unveiling Intrinsic Many-Body Complexity by Compressing Single-Body Triviality

The simultaneous treatment of static and dynamical correlations in strongly-correlated electron systems is a critical challenge. In particular, finding a universal scheme for identifying a single-particle orbital basis that minimizes the representational complexity of the many-body wavefunction is a formidable and longstanding problem. As a substantial contribution towards its solution, we show that the total orbital correlation actually reveals and quantifies the intrinsic complexity of the wavefunction,once it is minimized via orbital rotations. To demonstrate the power of this concept in practice, an iterative scheme is proposed to optimize the orbitals by minimizing the total orbital correlation calculated by the tailored coupled cluster singles and doubles (TCCSD) ansatz. The optimized orbitals enable the limited TCCSD ansatz to capture more non-trivial information of the many-body wavefunction, indicated by the improved wavefunction and energy. An initial application of this scheme shows great improvement of TCCSD in predicting the singlet ground state potential energy curves of the strongly correlated C$_{\rm 2}$ and Cr$_{\rm 2}$ molecule.

quant-ph↗

arXiv2024

What Can Quantum Information Theory Offer to Quantum Chemistry?

It is the ultimate goal of this work to foster synergy between quantum chemistry and the flourishing field of quantum information theory. For this, we first translate quantum information concepts such as entanglement and correlation into the context of quantum chemical systems. In particular, we establish two conceptually distinct perspectives on `electron correlation' leading to a notion of orbital and particle correlation. We then demonstrate that particle correlation equals total orbital correlation minimized over all orbital bases. Accordingly, particle correlation resembles the minimal, thus intrinsic, complexity of many-electron wave functions while orbital correlation quantifies their complexity relative to a basis. We illustrate these concepts of intrinsic and extrinsic correlation complexity in molecular systems, which also manifests the crucial link between the two correlation pictures. Our results provide theoretical justification for the long-favored natural orbitals for simplifying electronic structures, and open new pathways for developing more efficient approaches towards the electron correlation problem.

quant-ph↗

arXiv2023

Physical Entanglement Between Localized Orbitals

In [arXiv:2207.03377] the first closed formula of a faithful entanglement measure applicable to realistic electron systems has been derived. In the present work, we build on this key achievement with the ultimate goal of guiding the development of quantum technologies. For this, we first elucidate the process of entanglement swapping in electron systems such as atoms, molecules or solid bodies. This clearly demonstrates the necessity of both the reference to localized few-orbital subsystems and the implementation of the number-parity superselection rule. Accordingly, in virtue of Wick's theorem, we then provide a fully analytical study of the true physical entanglement between sites in free electron chains. In that sense, we break the common paradigm of restricting such analytical analyses to unitarily invariant settings, i.e. bipartitions of the chain into rather impractical, macroscopically large subsystems. We then upgrade this model to a hydrogen ring of interacting electrons and construct the sought-after localized orbitals. For both systems, we confirm the presence of long-distance entanglement, provided the filling fractions are sufficiently low/high.

quant-ph↗

arXiv2023

Refining and relating fundamentals of functional theory

To advance the foundation of one-particle reduced density matrix functional theory (1RDMFT) we refine and relate some of its fundamental features and underlying concepts. We define by concise means the scope of a 1RDMFT, identify its possible natural variables and explain how symmetries could be exploited. In particular, for systems with time-reversal symmetry, we explain why there exist six equivalent universal functionals, prove concise relations among them and conclude that the important notion of $v$-representability is relative to the scope and choice of variable. All these fundamental concepts are then comprehensively discussed and illustrated for the Hubbard dimer and its generalization to arbitrary pair interactions $W$. For this, we derive by analytical means the pure and ensemble functionals with respect to both the real- and complex-valued Hilbert space. The comparison of various functionals allows us to solve the underlying $v$-representability problems analytically and the dependence of its solution on the pair interaction is demonstrated. Intriguingly, the gradient of each universal functional is found to always diverge repulsively on the boundary of the domain. In that sense, this key finding emphasizes the universal character of the fermionic exchange force, recently discovered and proven in the context of translationally-invariant one-band lattice models.

quant-ph↗

arXiv2023

Shielded Reinforcement Learning for Hybrid Systems

Safe and optimal controller synthesis for switched-controlled hybrid systems, which combine differential equations and discrete changes of the system's state, is known to be intricately hard. Reinforcement learning has been leveraged to construct near-optimal controllers, but their behavior is not guaranteed to be safe, even when it is encouraged by reward engineering. One way of imposing safety to a learned controller is to use a shield, which is correct by design. However, obtaining a shield for non-linear and hybrid environments is itself intractable. In this paper, we propose the construction of a shield using the so-called barbaric method, where an approximate finite representation of an underlying partition-based two-player safety game is extracted via systematically picked samples of the true transition function. While hard safety guarantees are out of reach, we experimentally demonstrate strong statistical safety guarantees with a prototype implementation and UPPAAL STRATEGO. Furthermore, we study the impact of the synthesized shield when applied as either a pre-shield (applied before learning a controller) or a post-shield (only applied after learning a controller). We experimentally demonstrate superiority of the pre-shielding approach. We apply our technique on a range of case studies, including two industrial examples, and further study post-optimization of the post-shielding approach.

cs.LO↗

arXiv2023

The inverse problem for neural networks

We study the problem of computing the preimage of a set under a neural network with piecewise-affine activation functions. We recall an old result that the preimage of a polyhedral set is again a union of polyhedral sets and can be effectively computed. We show several applications of computing the preimage for analysis and interpretability of neural networks.

cs.LG↗

arXiv2023

Deriving density-matrix functionals for excited states

We initiate the recently proposed $\boldsymbol{w}$-ensemble one-particle reduced density matrix functional theory ($\boldsymbol{w}$-RDMFT) by deriving the first functional approximations and illustrate how excitation energies can be calculated in practice. For this endeavour, we first study the symmetric Hubbard dimer, constituting the building block of the Hubbard model, for which we execute the Levy-Lieb constrained search. Second, due to the particular suitability of $\boldsymbol{w}$-RDMFT for describing Bose-Einstein condensates, we demonstrate three conceptually different approaches for deriving the universal functional in a homogeneous Bose gas for arbitrary pair interaction in the Bogoliubov regime. Remarkably, in both systems the gradient of the functional is found to diverge repulsively at the boundary of the functional's domain, extending the recently discovered Bose-Einstein condensation force to excited states. Our findings highlight the physical relevance of the generalized exclusion principle for fermionic and bosonic mixed states and the curse of universality in functional theories.

cond-mat.quant-gas↗

arXiv2023

Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes

We present a novel approach to efficiently compute tight non-convex enclosures of the image through neural networks with ReLU, sigmoid, or hyperbolic tangent activation functions. In particular, we abstract the input-output relation of each neuron by a polynomial approximation, which is evaluated in a set-based manner using polynomial zonotopes. While our approach can also can be beneficial for open-loop neural network verification, our main application is reachability analysis of neural network controlled systems, where polynomial zonotopes are able to capture the non-convexity caused by the neural network as well as the system dynamics. This results in a superior performance compared to other methods, as we demonstrate on various benchmarks.

cs.CV↗

arXiv2023

1-matrix functional for long-range interaction energy of two hydrogen atoms

The leading terms in the large-$R$ asymptotics of the functional of the one-electron reduced density matrix for the ground-state energy of the H$_2$ molecule with the internuclear separation $R$ is derived thanks to the solution of the phase dilemma at the $R \to \infty$ limit. At this limit, the respective natural orbitals (NOs) are given by symmetric and antisymmetric combinations of "half-space" orbitals with the corresponding natural amplitudes of the same amplitudes but opposite signs. Minimization of the resulting explicit functional yields the large-$R$ asymptotics for the occupation numbers of the weakly occupied NOs and the $C_6$ dispersion coefficient. The highly accurate approximates for the radial components of the $p$-type "half-space" orbitals and the corresponding occupation numbers (that decay like $R^{-6}$), which are available for the first time thanks to the development of the present formalism, have some unexpected properties.

physics.chem-ph↗

arXiv2023

Implementations of two Algorithms for the Threshold Synthesis Problem

A linear pseudo-Boolean constraint (LPB) is an expression of the form $a_1 \cdot \ell_1 + \dots + a_m \cdot \ell_m \geq d$, where each $\ell_i$ is a literal (it assumes the value 1 or 0 depending on whether a propositional variable $x_i$ is true or false) and $a_1, \dots, a_m, d$ are natural numbers. An LPB represents a Boolean function, and those Boolean functions that can be represented by exactly one LPB are called threshold functions. The problem of finding an LPB representation of a Boolean function if possible is called threshold recognition problem or threshold synthesis problem. The problem has an $O(m^7 t^5)$ algorithm using linear programming, where $m$ is the dimension and $t$ the number of terms in the DNF input. It has been an open question whether one can recognise threshold functions through an entirely combinatorial procedure. Smaus has developed such a procedure for doing this, which works by decomposing the DNF and "counting" the variable occurrences in it. We have implemented both algorithms as a thesis project. We report here on this experience. The most important insight was that the algorithm by Smaus is, unfortunately, incomplete.

cs.LO↗

arXiv2022

symQV: Automated Symbolic Verification of Quantum Programs

We present symQV, a symbolic execution framework for writing and verifying quantum computations in the quantum circuit model. symQV can automatically verify that a quantum program complies with a first-order specification. We formally introduce a symbolic quantum program model. This allows to encode the verification problem in an SMT formula, which can then be checked with a delta-complete decision procedure. We also propose an abstraction technique to speed up the verification process. Experimental results show that the abstraction improves symQV's scalability by an order of magnitude to quantum programs with 24 qubits (a 2^24-dimensional state space).

quant-ph↗

arXiv2022

An exact one-particle theory of bosonic excitations: From a generalized Hohenberg-Kohn theorem to convexified N-representability

Motivated by the Penrose-Onsager criterion for Bose-Einstein condensation we propose a functional theory for targeting low-lying excitation energies of bosonic quantum systems through the one-particle picture. For this, we employ an extension of the Rayleigh-Ritz variational principle to ensemble states with spectrum $\boldsymbol{w}$ and prove a corresponding generalization of the Hohenberg-Kohn theorem: The underlying one-particle reduced density matrix determines all properties of systems of $N$ identical particles in their $\boldsymbol{w}$-ensemble states. Then, to circumvent the $v$-representability problem common to functional theories, and to deal with energetic degeneracies, we resort to the Levy-Lieb constrained search formalism in combination with an exact convex relaxation. The corresponding bosonic one-body $\boldsymbol{w}$-ensemble $N$-representability problem is solved comprehensively. Remarkably, this reveals a complete hierarchy of bosonic exclusion principle constraints in conceptual analogy to Pauli's exclusion principle for fermions and recently discovered generalizations thereof.

quant-ph↗