Wenda Li

Department of Computer Science and Technology,

University of Cambridge,

William Gates Building,

15 JJ Thomson Avenue,

Cambridge CB3 0FD, UK

I am a research associate at University of Cambridge, working with Prof. Larry Paulson. My research interest includes

machine learning for theorem proving,
interactive theorem proving,
verified symbolic computing,
and mechanised mathematics.

I believe modern machine learning techniques will revolutionise the way people do mechanised proofs, so that we can build more reliable systems.

I will be joining the University of Edinburgh as a lecturer (equivalent to assistant professor in the US) in September. I will have full scholarships for home and international students - if you want to pursue a PhD with me, please get in touch.

selected publications

arXiv

Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving

Xueliang Zhao, Wenda Li, and Lingpeng Kong

2023

Bib HTML PDF

@misc{zhao2023decomposing,
  title = {Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving},
  author = {Zhao, Xueliang and Li, Wenda and Kong, Lingpeng},
  year = {2023},
  eprint = {2305.16366},
  archiveprefix = {arXiv},
  primaryclass = {cs.CL},
}

ICLR (oral)

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

Bib PDF

@inproceedings{jiang2023draft,
  title = {Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs},
  author = {Jiang, Albert Qiaochu and Welleck, Sean and Zhou, Jin Peng and Lacroix, Timothee and Liu, Jiacheng and Li, Wenda and Jamnik, Mateja and Lample, Guillaume and Wu, Yuhuai},
  booktitle = {The Eleventh International Conference on Learning Representations },
  year = {2023},
  url = {https://openreview.net/forum?id=SMa9EAovKMC}
}

NeurIPS

Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers

Albert Q Jiang, Wenda Li, Szymon Tworkowski, and 5 more authors

2022

Bib HTML PDF

@article{jiang2022thor,
  title = {Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers},
  author = {Jiang, Albert Q and Li, Wenda and Tworkowski, Szymon and Czechowski, Konrad and Odrzyg{\'o}{\'z}d{\'z}, Tomasz and Mi{\l}o{\'s}, Piotr and Wu, Yuhuai and Jamnik, Mateja},
  booktitle = {Conference on Neural Information Processing Systems,},
  year = {2022}
}

ICML

Lime: Learning inductive bias for primitives of mathematical reasoning

Yuhuai Wu, Markus N Rabe, Wenda Li, and 3 more authors

In International Conference on Machine Learning, 2021

Bib PDF

@inproceedings{wu2021lime,
  title = {Lime: Learning inductive bias for primitives of mathematical reasoning},
  author = {Wu, Yuhuai and Rabe, Markus N and Li, Wenda and Ba, Jimmy and Grosse, Roger B and Szegedy, Christian},
  booktitle = {International Conference on Machine Learning,},
  pages = {11251--11262},
  year = {2021},
  organization = {PMLR}
}

ICLR

IsarStep: a Benchmark for High-level Mathematical Reasoning

Wenda Li, Lei Yu, Yuhuai Wu, and 1 more author

In International Conference on Learning Representations, 2021

Bib HTML PDF Code

@inproceedings{li2021isarstep,
  title = {IsarStep: a Benchmark for High-level Mathematical Reasoning},
  author = {Li, Wenda and Yu, Lei and Wu, Yuhuai and Paulson, Lawrence C.},
  booktitle = {International Conference on Learning Representations,},
  year = {2021},
}

JAR

Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL

Wenda Li, and Lawrence C Paulson

Journal of Automated Reasoning 2020

Bib HTML PDF

@article{li2020evaluating,
  title = {Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL},
  author = {Li, Wenda and Paulson, Lawrence C},
  journal = {Journal of Automated Reasoning},
  volume = {64},
  number = {2},
  pages = {331--360},
  year = {2020},
  publisher = {Springer}
}

JAR

Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL

Wenda Li, Grant Olney Passmore, and Lawrence C Paulson

Journal of Automated Reasoning, 2019

Bib HTML PDF Code

@article{li2019deciding,
  title = {Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL},
  author = {Li, Wenda and Passmore, Grant Olney and Paulson, Lawrence C},
  journal = {Journal of Automated Reasoning,},
  volume = {62},
  number = {1},
  pages = {69--91},
  year = {2019},
  publisher = {Springer}
}