| 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 | 232 | 2014 |
| 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 | 172 | 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 | 143 | 2022 |
| 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 | 93 | 2022 |
| IsarStep: a Benchmark for High-level Mathematical Reasoning W Li, L Yu, Y Wu, LC Paulson International Conference on Learning Representations, 2021 | 76 | 2021 |
| 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 | 69 | 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 | 60 | 2021 |
| 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 | 59 | 2024 |
| 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 | 36 | 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 | 22 | 2023 |
| 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 | 22 | 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 |
| Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving X Zhao, W Li, L Kong arXiv preprint arXiv:2305.16366, 2023 | 18 | 2023 |
| Multilingual mathematical autoformalization AQ Jiang, W Li, M Jamnik arXiv preprint arXiv:2311.03755, 2023 | 17 | 2023 |
| 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 |
| A formal proof of Cauchy’s residue theorem W Li, LC Paulson Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy …, 2016 | 16 | 2016 |
| Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL W Li, LC Paulson Journal of Automated Reasoning 64 (2), 331-360, 2020 | 13 | 2020 |
| Modelling high-level mathematical reasoning in mechanised declarative proofs W Li, L Yu, Y Wu, LC Paulson arXiv preprint arXiv:2006.09265, 2020 | 12 | 2020 |
| The Sturm–Tarski theorem W Li Archive of Formal Proofs, 2014 | 7 | 2014 |
| 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 | 6 | 2024 |
Yuhuai(Tony) WuCo-Founder of xAIПодтвержден адрес электронной почты в домене x.ai