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.

selected publications

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

@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 = {To appear at 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}
}