| Autoformalization with large language models Y Wu, AQ Jiang, W Li, M Rabe, C Staats, M Jamnik, C Szegedy Advances in Neural Information Processing Systems 35, 32353-32368, 2022 | 311 | 2022 |
| Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs AQ Jiang, S Welleck, JP Zhou, W Li, J Liu, M Jamnik, T Lacroix, Y Wu, ... arXiv preprint arXiv:2210.12283, 2022 | 280 | 2022 |
| Systems analysis of auxin transport in the Arabidopsis root apex LR Band, DM Wells, JA Fozard, T Ghetiu, AP French, MP Pound, ... The Plant Cell 26 (3), 862-875, 2014 | 256 | 2014 |
| Thor: Wielding hammers to integrate language models and automated theorem provers AQ Jiang, W Li, S Tworkowski, K Czechowski, T Odrzygóźdź, P Miłoś, ... Advances in Neural Information Processing Systems 35, 8360-8373, 2022 | 152 | 2022 |
| DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data H Xin, D Guo, Z Shao, Z Ren, Q Zhu, B Liu, C Ruan, W Li, X Liang arXiv preprint arXiv:2405.14333, 2024 | 147 | 2024 |
| Evaluating language models for mathematics through interactions KM Collins, AQ Jiang, S Frieder, L Wong, M Zilka, U Bhatt, T Lukasiewicz, ... Proceedings of the National Academy of Sciences 121 (24), e2318124121, 2024 | 120 | 2024 |
| LISA: Language models of ISAbelle proofs AQ Jiang, W Li, JM Han, Y Wu 6th Conference on Artificial Intelligence and Theorem Proving, 378-392, 2021 | 108 | 2021 |
| IsarStep: a Benchmark for High-level Mathematical Reasoning W Li, L Yu, Y Wu, LC Paulson International Conference on Learning Representations, 2021 | 92 | 2021 |
| Lime: Learning inductive bias for primitives of mathematical reasoning Y Wu, MN Rabe, W Li, J Ba, RB Grosse, C Szegedy International Conference on Machine Learning, 11251-11262, 2021 | 80 | 2021 |
| Formal mathematical reasoning: A new frontier in ai K Yang, G Poesia, J He, W Li, K Lauter, S Chaudhuri, D Song arXiv preprint arXiv:2412.16075, 2024 | 72 | 2024 |
| Don't Trust: Verify--Grounding LLM Quantitative Reasoning with Autoformalization JP Zhou, CE Staats, W Li, C Szegedy, KQ Weinberger, Y Wu The Twelfth International Conference on Learning Representations, 2023 | 66 | 2023 |
| Multilingual mathematical autoformalization AQ Jiang, W Li, M Jamnik arXiv preprint arXiv:2311.03755, 2023 | 43 | 2023 |
| Proving Theorems Recursively H Wang, H Xin, Z Liu, W Li, Y Huang, J Lu, Z Yang, J Tang, J Yin, Z Li, ... arXiv preprint arXiv:2405.14414, 2024 | 35 | 2024 |
| Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving X Zhao, W Li, L Kong arXiv preprint arXiv:2305.16366, 2023 | 32 | 2023 |
| End-to-end ontology learning with large language models A Lo, AQ Jiang, W Li, M Jamnik Advances in Neural Information Processing Systems 37, 87184-87225, 2024 | 27 | 2024 |
| Simple type theory is not too simple: Grothendieck’s schemes without dependent types A Bordg, L Paulson, W Li Experimental Mathematics 31 (2), 364-382, 2022 | 25 | 2022 |
| Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL W Li, GO Passmore, LC Paulson Journal of Automated Reasoning 62 (1), 69-91, 2019 | 22 | 2019 |
| Multi-language diversity benefits autoformalization AQ Jiang, W Li, M Jamnik Advances in Neural Information Processing Systems 37, 83600-83626, 2024 | 19 | 2024 |
| A formal proof of Cauchy’s residue theorem W Li, LC Paulson Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy …, 2016 | 18 | 2016 |
| A modular, efficient formalisation of real algebraic numbers W Li, LC Paulson Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016 | 16 | 2016 |
Albert Q. JiangMistral AIVerified email at mistral.ai
