Evaluating Language Models for Mathematics through Interactions
Published in arXiv, 2023
Paper link
Publications
Selected publications. My Semantic Scholar profile is much more complete (and up-to-date).
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
Published in The Eleventh International Conference on Learning Representations (ICLR) (Oral), 2023
Paper link
Magnushammer: A Transformer-based Approach to Premise Selection
Published in arxiv, 2023
What Christian had | What I heard
— Albert Jiang (@AlbertQJiang) March 9, 2023
in mind when he |
suggested the name | https://t.co/Ac7RExnCV9 pic.twitter.com/sVIMiKRafI
Paper link
Autoformalization with Large Language Models
Published in Thirty-sixth Conference on Neural Information Processing Systems (NeurIPS), 2022
Paper link
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
Published in Thirty-sixth Conference on Neural Information Processing Systems (NeurIPS), 2022
Paper link
Can Network Flatness Explain the Training Speed-Generalisation Connection?
Published in Bayesian Deep Learning Workshop at the Thirty-fifth Conference on Neural Information Processing Systems (NeurIPs), 2021
Paper link
LISA: Language models of ISAbelle proofs
Published in 6th Conference on Artificial Intelligence and Theorem Proving (AITP), 2021
We introduce an environment that allows interaction with an Is- abelle server in an incremental manner. With this environment, we mined the Isabelle standard library and the Archive of Formal Proofs (AFP) and extracted 183K lemmas and theorems. We built language models on this large corpus and showed their effectiveness in proving AFP theorems.
Paper link
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
Published in The Nineth International Conference on Learning Representations (ICLR), 2021
Paper link
Neural Theorem Proving on Inequality Problems
Published in 5th Conference on Artificial Intelligence and Theorem Proving (AITP), 2020
Paper link