Search

Formal verification is a promising method for producing reliable software, but the difficulty of manually writing verification proofs severely limits its utility in practice. Recent methods have automated some proof synthesis by guiding a search through the proof space using a theorem prover. Unfortunately, the theorem prover provides only the crudest estimate of progress, resulting in effectively undirected search. To address this problem, we create QEDCartographer, an automated proof-synthesis tool that combines supervised and reinforcement learning to more effectively explore the proof space. QEDCartographer incorporates the proofs' branching structure, enabling reward-free search and overcoming the sparse reward problem inherent to formal verification. We evaluate QEDCartographer using the CoqGym benchmark of 68.5K theorems from 124 open-source Coq projects. QEDCartographer fully automatically proves 21.4% of the test-set theorems. Previous search-based proof-synthesis tools Tok, Tac, ASTactic, Passport, and Proverbot9001, which rely only on supervised learning, prove 9.6%, 9.8%, 10.9%, 12.5%, and 19.8%, respectively. Diva, which combines 62 tools, proves 19.2%. Comparing to the most effective prior tool, Proverbot9001, QEDCartographer produces 34% shorter proofs 29% faster, on average over the theorems both tools prove. Together, QEDCartographer and non-learning-based CoqHammer prove 30.3% of the theorems, while CoqHammer alone proves 26.6%. Our work demonstrates that reinforcement learning is a fruitful research direction for improving proof-synthesis tools' search mechanisms., Comment: Published in the International Conference on Software Engineering (ICSE) 2025: Alex Sanchez-Stern, Abhishek Varghese, Zhanna Kaufman, Dylan Zhang, Talia Ringer, and Yuriy Brun, QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning, in Proceedings of the 47th International Conference on Software Engineering (ICSE), 2025

Formally verifying system properties is one of the most effective ways of improving system quality, but its high manual effort requirements often render it prohibitively expensive. Tools that automate formal verification, by learning from proof corpora to suggest proofs, have just begun to show their promise. These tools are effective because of the richness of the data the proof corpora contain. This richness comes from the stylistic conventions followed by communities of proof developers, together with the logical systems beneath proof assistants. However, this richness remains underexploited, with most work thus far focusing on architecture rather than making the most of the proof data. In this paper, we develop Passport, a fully-automated proof-synthesis tool that systematically explores how to most effectively exploit one aspect of that proof data: identifiers. Passport enriches a predictive Coq model with three new encoding mechanisms for identifiers: category vocabulary indexing, subword sequence modeling, and path elaboration. We compare Passport to three existing base tools which Passport can enhance: ASTactic, Tac, and Tok. In head-to-head comparisons, Passport automatically proves 29% more theorems than the best-performing of these base tools. Combining the three Passport-enhanced tools automatically proves 38% more theorems than the three base tools together, without Passport's enhancements. Finally, together, these base tools and Passport-enhanced tools prove 45% more theorems than the combined base tools without Passport's enhancements. Overall, our findings suggest that modeling identifiers can play a significant role in improving proof synthesis, leading to higher-quality software.

Foundational verification allows programmers to build software which has been empirically shown to have high levels of assurance in a variety of important domains. However, the cost of producing foundationally verified software remains prohibitively high for most projects,as it requires significant manual effort by highly trained experts. In this paper we present Proverbot9001,a proof search system using machine learning techniques to produce proofs of software correctness in interactive theorem provers. We demonstrate Proverbot9001 on the proof obligations from a large practical proof project,the CompCert verified C compiler,and show that it can effectively automate what were previously manual proofs,automatically producing proofs for 27.5% of theorem statements in our test dataset, when combined with solver-based tooling. Without any additional solvers,we exhibit a proof completion rate that is a 4X improvement over prior state-of-the-art machine learning models for generating proofs in Coq., Comment: Condensed version to be published at MAPL 2020

SmB6 is a mixed valence Kondo insulator that exhibits a sharp increase in resistance following an activated behavior that levels off and saturates below 4K. This behavior can be explained by the proposal of SmB6 representing a new state of matter, a Topological Kondo insulator, in which a Kondo gap is developed and topologically protected surface conduction dominates low-temperature transport. Exploiting its non-linear dynamics, a tunable SmB6 oscillator device was recently demonstrated, where a small DC current generates large oscillating voltages at frequencies from a few Hz to hundreds of MHz. This behavior was explained by a theoretical model describing the thermal and electronic dynamics of coupled surface and bulk states. However, a crucial aspect of this model, the predicted temperature oscillation in the surface state, hasn't been experimentally observed to date. This is largely due to the technical difficulty of detecting an oscillating temperature of the very thin surface state. Here we report direct measurements of the time-dependent surface state temperature in SmB6 with a RuO micro-thermometer. Our results agree quantitatively with the theoretically simulated temperature waveform, and hence support the validity of the oscillator model, which will provide accurate theoretical guidance for developing future SmB6oscillators at higher frequencies., Comment: 6 pages, 6 figures

Floating-point arithmetic plays a central role in science, engineering, and finance by enabling developers to approximate real arithmetic. To address numerical issues in large floating-point applications, developers must identify root causes, which is difficult because floating-point errors are generally non-local, non-compositional, and non-uniform. This paper presents Herbgrind, a tool to help developers identify and address root causes in numerical code written in low-level C/C++ and Fortran. Herbgrind dynamically tracks dependencies between operations and program outputs to avoid false positives and abstracts erroneous computations to a simplified program fragment whose improvement can reduce output error. We perform several case studies applying Herbgrind to large, expert-crafted numerical programs and show that it scales to applications spanning hundreds of thousands of lines, correctly handling the low-level details of modern floating point hardware and mathematical libraries, and tracking error across function boundaries and through the heap., Comment: 15 pages published at PLDI 18

It has been long hoped that the realization of long-range ferromagnetic order in two-dimensional (2D) van der Waals (vdW) crystals, combined with their rich electronic and optical properties, would open up new possibilities for magnetic, magnetoelectric and magneto-optic applications. However, in 2D systems, the long-range magnetic order is strongly hampered by thermal fluctuations which may be counteracted by magnetic anisotropy, according to the Mermin-Wagner theorem. Prior efforts via defect and composition engineering, and proximity effect only locally or extrinsically introduce magnetic responses. Here we report the first experimental discovery of intrinsic long-range ferromagnetic order in pristine Cr2Ge2Te6 atomic layers by scanning magneto-optic Kerr microscopy. In such a 2D vdW soft ferromagnet, for the first time, an unprecedented control of transition temperature of ~ 35% - 57% enhancement is realized via surprisingly small fields (<= 0.3 Tesla in this work), in stark contrast to the stiffness of the transition temperature to magnetic fields in the three-dimensional regime. We found that the small applied field enables an effective anisotropy far surpassing the tiny magnetocrystalline anisotropy, opening up a sizable spin wave excitation gap. Confirmed by renormalized spin wave theory, we explain the phenomenon and conclude that the unusual field dependence of transition temperature constitutes a hallmark of 2D soft ferromagnetic vdW crystals. Our discovery of 2D soft ferromagnetic Cr2Ge2Te6 presents a close-to-ideal 2D Heisenberg ferromagnet for studying fundamental spin behaviors, and opens the door for exploring new applications such as ultra-compact spintronics., Comment: to appear in Nature

Superconductivity that spontaneously breaks time-reversal symmetry (TRS) has been found, so far, only in a handful of 3D crystals with bulk inversion symmetry. Here we report an observation of spontaneous TRS breaking in a 2D superconducting system without inversion symmetry: the epitaxial bilayer films of bismuth and nickel. The evidence comes from the onset of the polar Kerr effect at the superconducting transition in the absence of an external magnetic field, detected by the ultrasensitive loop-less fiber-optic Sagnac interferometer. Because of strong spin-orbit interaction and lack of inversion symmetry in a Bi/Ni bilayer, superconducting pairing cannot be classified as singlet or triplet. We propose a theoretical model where magnetic fluctuations in Ni induce superconducting pairing of the dxy = +- idx^2y^2 orbital symmetry between the electrons in Bi. In this model the order parameter spontaneously breaks the TRS and has a non-zero phase winding number around the Fermi surface, thus making it a rare example of a 2D topological superconductor., Comment: Accepted by Science Advances. Supplimental information can be found in the following URL: http://www.physics.uci.edu/~xia/X-lab/Publications_files/Supplementary_Information.pdf