skip to main content

Search for: All records

Creators/Authors contains: "First, Emily"

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

  1. Formally verified correctness is one of the most desirable properties of software systems. But despite great progress made via interactive theorem provers, such as Coq, writing proof scripts for verification remains one of the most effort-intensive (and often prohibitively difficult) software development activities. Recent work has created tools that automatically synthesize proofs or proof scripts. For example, CoqHammer can prove 26.6% of theorems completely automatically by reasoning using precomputed facts, while TacTok and ASTactic, which use machine learning to model proof scripts and then perform biased search through the proof-script space, can prove 12.9% and 12.3% of the theorems, respectively.more »Further, these three tools are highly complementary; together, they can prove 30.4% of the theorems fully automatically. Our key insight is that control over the learning process can produce a diverse set of models, and that, due to the unique nature of proof synthesis (the existence of the theorem prover, an oracle that infallibly judges a proof's correctness), this diversity can significantly improve these tools' proving power. Accordingly, we develop Diva, which uses a diverse set of models with TacTok's and ASTactic's search mechanism to prove 21.7% of the theorems. That is, Diva proves 68% more theorems than TacTok and 77% more than ASTactic. Complementary to CoqHammer, Diva proves 781 theorems (27% added value) that Coq-Hammer does not, and 364 theorems no existing tool has proved automatically. Together with CoqHammer, Diva proves 33.8% of the theorems, the largest fraction to date. We explore nine dimensions for learning diverse models, and identify which dimensions lead to the most useful diversity. Further, we develop an optimization to speed up Diva's execution by 40X. Our study introduces a completely new idea for using diversity in machine learning to improve the power of state-of-the-art proof-script synthesis techniques, and empirically demonstrates that the improvement is significant on a dataset of 68K theorems from 122 open-source software projects.« less
    Free, publicly-accessible full text available May 21, 2023
  2. Abstract Volcán Quizapu, Chile, is an under-monitored volcano that was the site of two historical eruptions: an effusive eruption in 1846–1847 and a Plinian eruption in 1932, both of which discharged ∼5 km3 (dense rock equivalent) of lava and/or tephra. The majority of material erupted in both cases is trachydacite, nearly identical for each event. We present H2O-saturated, phase equilibrium experiments on this end-member dacite magma, using a pumice sample from the 1932 eruption as the main starting material. At an oxygen fugacity (fO2) of ∼NNO + 0·2 (where NNO is the nickel–nickel oxide buffer), the phase assemblage of An25–30 plagioclase + amphibolemore »+ orthopyroxene, without biotite, is stable at 865 ± 10 °C and 110 ± 20 MPa H2O pressure (PH2O), corresponding to ∼4 km depth. At these conditions, experiments also reproduce the quenched glass composition of the starting pumice. At slightly higher PH2O and below 860 °C, biotite joins the equilibrium assemblage. Because biotite is not part of the observed Quizapu phase assemblage, its presence places an upper limit on PH2O. At the determined storage PH2O of ∼110 MPa, H2O undersaturation of the magma with XH2Ofluid = 0·87 would align Ptotal to mineral-based geobarometry estimates of ∼130 MPa. However, XH2Ofluid < 1 is not required to reproduce the Quizapu dacite phase assemblage and compositions. A second suite of experiments at lower fO2 shows that the stability fields of the hydrous silicates (amphibole and biotite) are significantly restricted at NNO – 2 relative to NNO + 0·2. Additional observations of Quizapu lava and pumice samples support the existing hypothesis that rapid pre-eruptive heating drove the effusive 1846–1847 eruption, with important refinements. We demonstrate that microlites in the end-member dacite lavas are consistent with in situ crystallization (during ascent), rather than transfer from an andesite. In one end-member dacite lava, newly identified reverse zoning in orthopyroxene and incipient destabilization of amphibole are consistent with small degrees of heating. Our work articulates a clear direction for future Quizapu studies, which are warranted given the active nature of the Cerro Azul–Descabezado Grande volcanic axis.« less