15 citations · 23 across the 4 of their papers we have counts for
5 papers
Machine-Learned Premise Selection for Lean
Bartosz Piotrowski, Ramon Fernández Mir, Edward Ayers
We introduce a machine-learning-based tool for the Lean proof assistant that suggests relevant premises for theorems being proved by a user. The design principles for the tool are…
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf +3
We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of…
Query-based Hard-Image Retrieval for Object Detection at Test Time
Edward Ayers, Jonathan Sadeghi, John Redford +2
There is a longstanding interest in capturing the error behaviour of object detectors by finding images where their performance is likely to be unsatisfactory. In real-world applic…
Proof Artifact Co-training for Theorem Proving with Language Models
Jesse Michael Han, Jason Rute, Yuhuai Wu +2
Labeled data for imitation learning of theorem proving in large libraries of formalized mathematics is scarce as such libraries require years of concentrated effort by human specia…
PaRoT: A Practical Framework for Robust Deep Neural Network Training
Edward Ayers, Francisco Eiras, Majd Hawasly +1
Deep Neural Networks (DNNs) are finding important applications in safety-critical systems such as Autonomous Vehicles (AVs), where perceiving the environment correctly and robustly…