Neural and symbolic theorem proving
We develop theorem proving methods that leverage informal and formal representations. For example, Draft Sketch Prove uses language models to sketch formal proofs based on informal proofs, then fills in the gaps.
Related publications
2023

 In The Eleventh International Conference on Learning Representations , 2023
2022
 In Advances in Neural Information Processing Systems, 2022
2021
 In Thirtyfifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1), 2021