Engineering Papers⌕ Search

Engineering topics

Peng, Yuxiang

Publications and source records attributed to Peng, Yuxiang.

Elucidating the Transition of 3D Morphological Evolution of Binary Alloys in Molten Salts with Metal Ion Additives

Molten salts serve as effective high-temperature heat transfer fluids and thermal storage media used in a wide range of energy generation and storage facilities, including concentrated solar power plants, molten salt reactors and high-temperature batteries. However, at the salt–metal interfaces, a complex interplay of charge-transfer reactions involving various metal ions, generated either as fission products or through corrosion of structural materials, takes place. Simultaneously, there is a mass transport of ions or atoms within the molten salt and the parent alloys. The precise physical and chemical mechanisms leading to the diverse morphological changes in these materials remain unclear. Here, to address this knowledge gap, this work employed a combination of synchrotron X-ray nanotomography and electron microscopy to study the morphological and chemical evolution of Ni-20Cr in molten KCl-MgCl 2 , while considering the influence of metal ions (Ni 2+ , Ce 3+ , and Eu 3+ ) and variations in salt composition. Our research suggests that the interplay between interfacial diffusivity and reactivity determines the morphological evolution. The summary of the associated mass transport and reaction processes presented in this work is a step forward toward achieving a fundamental comprehension of the interactions between molten salts and alloys. Overall, the findings offer valuable insights for predicting the diverse chemical and structural alterations experienced by alloys in molten salt environments, thus aiding in the development of protective strategies for future applications involving molten salts.

36 - MATERIALS SCIENCE↗

A formally certified end-to-end implementation of Shor’s factorization algorithm

Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but it is useful only if computed answers are correct. While hardware-level decoherence errors have garnered significant attention, a less recognized obstacle to correctness is that of human programming errors—“bugs.” Techniques familiar to most programmers from the classical domain for avoiding, discovering, and diagnosing bugs do not easily transfer, at scale, to the quantum domain because of its unique characteristics. To address this problem, we have been working to adapt formal methods to quantum programming. With such methods, a programmer writes a mathematical specification alongside the program and semiautomatically proves the program correct with respect to it. The proof’s validity is automatically confirmed—certified—by a “proof assistant.” Formal methods have successfully yielded high-assurance classical software artifacts, and the underlying technology has produced certified proofs of major mathematical theorems. As a demonstration of the feasibility of applying formal methods to quantum programming, we present a formally certified end-to-end implementation of Shor’s prime factorization algorithm, developed as part of a framework for applying the certified approach to general applications. By leveraging our framework, one can significantly reduce the effects of human errors and obtain a high-assurance implementation of large-scale quantum applications in a principled way.

Science & Technology - Other Topics↗

Automating NISQ Application Design with Meta Quantum Circuits with Constraints (MQCC)

Near-term intermediate scale quantum (NISQ) computers are likely to have very restricted hardware resources, where precisely controllable qubits are expensive, error-prone, and scarce. Programmers of such computers must therefore balance trade-offs among a large number of (potentially heterogeneous) factors specific to the targeted application and quantum hardware. To assist them, we propose Meta Quantum Circuits with Constraints (MQCC), a meta-programming framework for quantum programs. Programmers express their application as a succinct collection of normal quantum circuits stitched together by a set of (manually or automatically) added meta-level choice variables, whose values are constrained according to a programmable set of quantitative optimization criteria. MQCC’s compiler generates the appropriate constraints and solves them via an SMT solver, producing an optimized, runnable program. We showcase a few MQCC’s applications for its generality including an automatic generation of efficient error syndrome extraction schemes for fault-tolerant quantum error correction with heterogeneous qubits and an approach to writing approximate quantum Fourier transformation and quantum phase estimation that smoothly trades off accuracy and resource use. We also illustrate that MQCC can easily encode prior one-off NISQ application designs-–multi-programming (MP), crosstalk mitigation (CM)—as well as a combination of their optimization goals (i.e., a combined MP-CM).

97 MATHEMATICS AND COMPUTING↗