Searcharxiv⌕ Search

arXiv subjects

Yotam M. Y. Feldman

Publications and source records attributed to Yotam M. Y. Feldman.

15 recordsLinked to original sources

An Exact Formulation of Phase-Space Electronic Structure Theory in One Dimension by Exploiting the Zero Curvature Condition

We show that, for the unique case of a system of electrons and nuclei in one dimension, the $\hGamma$ operator in phase space electronic structure theory has a zero non-Abelian curl. Using this fact, we are able to show that a phase space electronic structure framework in Wigner space has a one-to-one mapping to the exact fully quantum vibronic Hamiltonian. In other words, one loses no information by working within the framework of phase space electronic structure theory rather than Born-Huang theory; the only difference is that, whereas Born-Huang theory represents the total vibronic Hamiltonian as a quadratic order expansion in $\hbar$, the Hamiltonian becomes an infinite order expansion in $\hbar$ within a phase space electronic structure framework (a so-called "Generalized Born-Huang" approach). That being said, numerical results at first or second order demonstrate that, for a limited number of electronic states, phase space electronic structure theory strongly outperforms Born-Huang theory -- a result that justifies a great deal more research into this novel electronic structure approach.

physics.chem-ph↗

Bosonic Condensed Phase Real-time Dynamics from Ring Polymer Molecular Dynamics

We present a method for approximating real-time correlation functions and quantum transport coefficients of bosonic condensed phases. The direct evaluation of quantum real-time correlation functions in the path integral formulation is impossible due to a severe dynamical sign problem. Evaluating imaginary-time correlation functions and inverting them using analytic continuation is famously ill-posed. Ring polymer molecular dynamics (RPMD) provides an alternative approach resulting in accurate approximations for real-time correlation functions of condensed phases but neglects exchange effects. In this work, we develop a bosonic RPMD method, which is exact in the harmonic, short time, and high temperature limits. A critical enabling observation is that the Kubo-transformed correlation function for bosons is real only when the correlated observables are symmetric under exchange. We benchmark the method on harmonic and anharmonic model systems and then use it to directly obtain the Lieb-Liniger gas density-density real-time correlation functions at various temperatures and momentum transfers. This work enables the direct simulation of finite-temperature, real-time dynamics of large bosonic condensed phases using RPMD for the first time.

physics.chem-ph↗

fix pimd/langevin: An Efficient Implementation of Path Integral Molecular Dynamics in LAMMPS

Path integral molecular dynamics (PIMD), which maps a quantum particle onto a fictitious classical system of ring polymers and propagates the "beads" of this extended classical system using molecular dynamics, is widely used to capture nuclear quantum effects (NQEs) in molecular simulations. Accurate PIMD calculations typically require a large number of beads and are therefore computationally demanding. While software packages such as i-PI offer comprehensive PIMD functionality, the high efficiency of simulations driven by machine learning interatomic potentials, such as Deep Potential (DP), calls for more efficient PIMD implementations that fully exploit modern massively parallel supercomputers. Here we present fix pimd/langevin, an efficient PIMD implementation in LAMMPS that supports commonly used features and leverages the Message Passing Interface architecture of LAMMPS to achieve high computational efficiency. We demonstrate the usage and validate the correctness of our code using liquid water as a representative example, and provide a comprehensive overview of the supported features. Then we discuss several important technical aspects of the implementation. Using DP simulations of water as a benchmark, we show that our implementation achieves several-fold acceleration compared to i-PI. Finally, we report strong and weak scaling results that demonstrate the favorable parallel performance of our code.

physics.chem-ph↗

Defect Positioning in Combinatorial Metamaterials

Combinatorial mechanical metamaterials are made of anisotropic, flexible blocks, such that multiple metamaterials may be constructed using a single block type, and the system's response depends on the frustration (or its absence) due to the mutual orientations of the blocks within the lattice. Specifically, any minimal loop of blocks that may not simultaneously deform in their softest mode defines a mechanical defect at the vertex (in two dimensions) or edge (in three dimensions) that the loop encircles. Defects stiffen the metamaterial, and allow to design the spatial patterns of stress and deformation as the system is externally loaded. We study the ability to place defects at arbitrary positions in metamaterials made of a family of block types that we recently introduced for the square, honeycomb, and cubic lattices. Alongside blocks for which we show that any defect configuration is possible, we identify situations in which not all sets are realizable as defects. One of the restrictions is that in three dimensions, defected edges form closed curves. Even in cases when not all geometries of defect lines are possible, we show how to produce defect lines of arbitrary knottedness.

cond-mat.soft↗

Quadratic Scaling Bosonic Path Integral Molecular Dynamics

Bosonic exchange symmetry leads to fascinating quantum phenomena, from exciton condensation in quantum materials to the superfluidity of liquid Helium-4. Unfortunately, path integral molecular dynamics (PIMD) simulations of bosons are computationally prohibitive beyond $\mathord{\sim} 100$ particles, due to a cubic scaling with the system size. We present an algorithm that reduces the complexity from cubic to quadratic, allowing the first simulations of thousands of bosons using PIMD. Our method is orders of magnitude faster, with a speedup that scales linearly with the number of particles and the number of imaginary time slices (beads). Simulations that would have otherwise taken decades can now be done in days. In practice, the new algorithm eliminates most of the added computational cost of including bosonic exchange effects, making them almost as accessible as PIMD simulations of distinguishable particles.

physics.comp-ph↗

Periodic Boundary Conditions for Bosonic Path Integral Molecular Dynamics

We develop an algorithm for bosonic path integral molecular dynamics (PIMD) simulations with periodic boundary conditions (PBC) that scales quadratically with the number of particles. Path integral methods are a powerful tool to simulate bosonic condensed phases, which exhibit fundamental physical phenomena such as Bose--Einstein condensation and superfluidity. Recently, we developed a quadratic scaling algorithm for bosonic PIMD, but employed an ad hoc treatment of PBC. Here we rigorously enforce PBC in bosonic PIMD. It requires summing over the spring energies of all periodic images in the partition function, and a naive implementation scales exponentially with the system size. We present an algorithm for bosonic PIMD simulations of periodic systems that scales only quadratically. We benchmark our implementation on the free Bose gas and a model system of cold atoms in optical lattices. We also study an approximate treatment of PBC based on the minimum-image convention, and derive a numerical criterion to determine when it is valid.

physics.chem-ph↗

i-PI 3.0: a flexible and efficient framework for advanced atomistic simulations

Atomic-scale simulations have progressed tremendously over the past decade, largely due to the availability of machine-learning interatomic potentials. These potentials combine the accuracy of electronic structure calculations with the ability to reach extensive length and time scales. The i-PI package facilitates integrating the latest developments in this field with advanced modeling techniques, thanks to a modular software architecture based on inter-process communication through a socket interface. The choice of Python for implementation facilitates rapid prototyping but can add computational overhead. In this new release, we carefully benchmarked and optimized i-PI for several common simulation scenarios, making such overhead negligible when i-PI is used to model systems up to tens of thousands of atoms using widely adopted machine learning interatomic potentials, such as Behler-Parinello, DeePMD and MACE neural networks. We also present the implementation of several new features, including an efficient algorithm to model bosonic and fermionic exchange, a framework for uncertainty quantification to be used in conjunction with machine-learning potentials, a communication infrastructure that allows deeper integration with electronic-driven simulations, and an approach to simulate coupled photon-nuclear dynamics in optical or plasmonic cavities.

physics.chem-ph↗

Proving Highly-Concurrent Traversals Correct

Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any synchronization. As a result, however, these algorithms are notoriously difficult to prove linearizable, which requires identifying a point in time in which the traversal's result is correct. The problem is that traversing the data structure as it undergoes modifications leads to complex behaviors, necessitating intricate reasoning about all interleavings of reads by traversals and writes mutating the data structure. In this paper, we present a general proof technique for proving unsynchronized traversals correct in a significantly simpler manner, compared to typical concurrent reasoning and prior proof techniques. Our framework relies only on sequential properties} of traversals and on a conceptually simple and widely-applicable condition about the ways an algorithm's writes mutate the data structure. Establishing that a target data structure satisfies our condition requires only simple concurrent reasoning, without considering interactions of writes and reads. This reasoning can be further simplified by using our framework. To demonstrate our technique, we apply it to prove several interesting and challenging concurrent binary search trees: the logical-ordering AVL tree, the Citrus tree, and the full contention-friendly tree. Both the logical-ordering tree and the full contention-friendly tree are beyond the reach of previous approaches targeted at simplifying linearizability proofs.

cs.DC↗

Invariant Inference With Provable Complexity From the Monotone Theory

Invariant inference algorithms such as interpolation-based inference and IC3/PDR show that it is feasible, in practice, to find inductive invariants for many interesting systems, but non-trivial upper bounds on the computational complexity of such algorithms are scarce, and limited to simple syntactic forms of invariants. In this paper we achieve invariant inference algorithms, in the domain of propositional transition systems, with provable upper bounds on the number of SAT calls. We do this by building on the monotone theory, developed by Bshouty for exact learning Boolean formulas. We prove results for two invariant inference frameworks: (i) model-based interpolation, where we show an algorithm that, under certain conditions about reachability, efficiently infers invariants when they have both short CNF and DNF representations (transcending previous results about monotone invariants); and (ii) abstract interpretation in a domain based on the monotone theory that was previously studied in relation to property-directed reachability, where we propose an efficient implementation of the best abstract transformer, leading to overall complexity bounds on the number of SAT calls. These results build on a novel procedure for computing least monotone overapproximations.

cs.PL↗

Property-Directed Reachability as Abstract Interpretation in the Monotone Theory

Inferring inductive invariants is one of the main challenges of formal verification. The theory of abstract interpretation provides a rich framework to devise invariant inference algorithms. One of the latest breakthroughs in invariant inference is property-directed reachability (PDR), but the research community views PDR and abstract interpretation as mostly unrelated techniques. This paper shows that, surprisingly, propositional PDR can be formulated as an abstract interpretation algorithm in a logical domain. More precisely, we define a version of PDR, called $Λ$-PDR, in which all generalizations of counterexamples are used to strengthen a frame. In this way, there is no need to refine frames after their creation, because all the possible supporting facts are included in advance. We analyze this algorithm using notions from Bshouty's monotone theory, originally developed in the context of exact learning. We show that there is an inherent overapproximation between the algorithm's frames that is related to the monotone theory. We then define a new abstract domain in which the best abstract transformer performs this overapproximation, and show that it captures the invariant inference process, i.e., $Λ$-PDR corresponds to Kleene iterations with the best transformer in this abstract domain. We provide some sufficient conditions for when this process converges in a small number of iterations, with sometimes an exponential gap from the number of iterations required for naive exact forward reachability. These results provide a firm theoretical foundation for the benefits of how PDR tackles forward reachability.

cs.PL↗

Learning the Boundary of Inductive Invariants

We study the complexity of invariant inference and its connections to exact concept learning. We define a condition on invariants and their geometry, called the fence condition, which permits applying theoretical results from exact concept learning to answer open problems in invariant inference theory. The condition requires the invariant's boundary---the states whose Hamming distance from the invariant is one---to be backwards reachable from the bad states in a small number of steps. Using this condition, we obtain the first polynomial complexity result for an interpolation-based invariant inference algorithm, efficiently inferring monotone DNF invariants with access to a SAT solver as an oracle. We further harness Bshouty's seminal result in concept learning to efficiently infer invariants of a larger syntactic class of invariants beyond monotone DNF. Lastly, we consider the robustness of inference under program transformations. We show that some simple transformations preserve the fence condition, and that it is sensitive to more complex transformations.

cs.PL↗

Complexity and Information in Invariant Inference

This paper addresses the complexity of SAT-based invariant inference, a prominent approach to safety verification. We consider the problem of inferring an inductive invariant of polynomial length given a transition system and a safety property. We analyze the complexity of this problem in a black-box model, called the Hoare-query model, which is general enough to capture algorithms such as IC3/PDR and its variants. An algorithm in this model learns about the system's reachable states by querying the validity of Hoare triples. We show that in general an algorithm in the Hoare-query model requires an exponential number of queries. Our lower bound is information-theoretic and applies even to computationally unrestricted algorithms, showing that no choice of generalization from the partial information obtained in a polynomial number of Hoare queries can lead to an efficient invariant inference procedure in this class. We then show, for the first time, that by utilizing rich Hoare queries, as done in PDR, inference can be exponentially more efficient than approaches such as ICE learning, which only utilize inductiveness checks of candidates. We do so by constructing a class of transition systems for which a simple version of PDR with a single frame infers invariants in a polynomial number of queries, whereas every algorithm using only inductiveness checks and counterexamples requires an exponential number of queries. Our results also shed light on connections and differences with the classical theory of exact concept learning with queries, and imply that learning from counterexamples to induction is harder than classical exact learning from labeled examples. This demonstrates that the convergence rate of Counterexample-Guided Inductive Synthesis depends on the form of counterexamples.

cs.PL↗

Bounded Quantifier Instantiation for Checking Inductive Invariants

We consider the problem of checking whether a proposed invariant $φ$ expressed in first-order logic with quantifier alternation is inductive, i.e. preserved by a piece of code. While the problem is undecidable, modern SMT solvers can sometimes solve it automatically. However, they employ powerful quantifier instantiation methods that may diverge, especially when $φ$ is not preserved. A notable difficulty arises due to counterexamples of infinite size. This paper studies Bounded-Horizon instantiation, a natural method for guaranteeing the termination of SMT solvers. The method bounds the depth of terms used in the quantifier instantiation process. We show that this method is surprisingly powerful for checking quantified invariants in uninterpreted domains. Furthermore, by producing partial models it can help the user diagnose the case when $φ$ is not inductive, especially when the underlying reason is the existence of infinite counterexamples. Our main technical result is that Bounded-Horizon is at least as powerful as instrumentation, which is a manual method to guarantee convergence of the solver by modifying the program so that it admits a purely universal invariant. We show that with a bound of 1 we can simulate a natural class of instrumentations, without the need to modify the code and in a fully automatic way. We also report on a prototype implementation on top of Z3, which we used to verify several examples by Bounded-Horizon of bound 1.

cs.LO↗

Inferring Inductive Invariants from Phase Structures

Infinite-state systems such as distributed protocols are challenging to verify using interactive theorem provers or automatic verification tools. Of these techniques, deductive verification is highly expressive but requires the user to annotate the system with inductive invariants. To relieve the user from this labor-intensive and challenging task, invariant inference aims to find inductive invariants automatically. Unfortunately, when applied to infinite-state systems such as distributed protocols, existing inference techniques often diverge, which limits their applicability. This paper proposes user-guided invariant inference based on phase invariants, which capture the different logical phases of the protocol. Users conveys their intuition by specifying a phase structure, an automaton with edges labeled by program transitions; the tool automatically infers assertions that hold in the automaton's states, resulting in a full safety proof.The additional structure from phases guides the inference procedure towards finding an invariant. Our results show that user guidance by phase structures facilitates successful inference beyond the state of the art. We find that phase structures are pleasantly well matched to the intuitive reasoning routinely used by domain experts to understand why distributed protocols are correct, so that providing a phase structure reuses this existing intuition.

cs.PL↗

Order out of Chaos: Proving Linearizability Using Local Views

Proving the linearizability of highly concurrent data structures, such as those using optimistic concurrency control, is a challenging task. The main difficulty is in reasoning about the view of the memory obtained by the threads, because as they execute, threads observe different fragments of memory from different points in time. Until today, every linearizability proof has tackled this challenge from scratch. We present a unifying proof argument for the correctness of unsynchronized traversals, and apply it to prove the linearizability of several highly concurrent search data structures, including an optimistic self-balancing binary search tree, the Lazy List and a lock-free skip list. Our framework harnesses {\em sequential reasoning} about the view of a thread, considering the thread as if it traverses the data structure without interference from other operations. Our key contribution is showing that properties of reachability along search paths can be deduced for concurrent traversals from such interference-free traversals, when certain intuitive conditions are met. Basing the correctness of traversals on such \emph{local view arguments} greatly simplifies linearizability proofs. To apply our framework, the user proves that the data structure satisfies two conditions: (1) acyclicity of the order on memory, even when it is considered across intermediate memory states, and (2) preservation of search paths to locations modified by interfering writes. Establishing the conditions, as well as the full linearizability proof utilizing our proof argument, reduces to simple concurrent reasoning. The result is a clear and comprehensible correctness proof, and elucidates common patterns underlying several existing data structures.

cs.DC↗