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

  1. Neural theorem proving tutorial
    Sean Welleck
    In IJCAI 2023 Tutorial, 2023
  2. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, and 6 more authors
    In The Eleventh International Conference on Learning Representations , 2023
    ICLR 2023 Oral

2022

  1. NaturalProver: Grounded Mathematical Proof Generation with Language Models
    Sean Welleck, Jiacheng Liu, Ximing Lu, and 2 more authors
    In Advances in Neural Information Processing Systems, 2022

2021

  1. NaturalProofs: Mathematical Theorem Proving in Natural Language
    Sean Welleck, Jiacheng Liu, Ronan Le Bras, and 3 more authors
    In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1), 2021
    NeurIPS 2021 Oral