Wenda Li
Lecturer in Hybrid AI
Researches neuro-symbolic reasoning and AI for mathematics, including machine learning and language models for theorem proving.
Wenda Li's lab at Edinburgh works on reasoning & neuro-symbolic AI, large language models and reasoning & agents. 18 papers since 2023, 14 at top venues, mostly ICML and NeurIPS. 8 PhD students. 1 alumnus.
At a glance
- papers, 2023–2026
- 5/ year
- at T1 venues
- 78%
- PhD students
- 8
- MS students
- 0
- alumni listed
- 1
Papers by yearfrom the lab homepage, 2023–2026
- 7 papers2026 · T1 4 · collecting
- 2 papers2025 · T1 2
- 8 papers2024 · T1 7
- 1 papers2023 · T1 1
T1 venuesOtherVenues: ICML, NeurIPS, ICLR, ACL, PNAS
Research focuspaper titles that use each topic's words
- Large language models6 papers
- Reasoning & neuro-symbolic AI4 papers
- Reasoning & agents4 papers
- theorem4 papers
- proving3 papers
Paper list
From the lab homepage.
20267 papers
- ICML (T1)APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
- ICML (T1)Can I Have Your Order? Monte-Carlo Tree Search for Slot Filling Ordering in Diffusion Language Models
- International Conference on Interactive Theorem ProvingFaster Verified Real Root Isolation with Descartes’ Rule of Signs (Short Paper)
- International Conference on Interactive Theorem ProvingFrom Weierstraß to Dedekind: Formalising Foundations of Modular Forms
- ICLR (T1)Neural Theorem Proving for Verification Conditions: A Real-World Benchmark
- ICML (T1)Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics
- Findings of the Association for Computational LinguisticsPiCSAR: Probabilistic Confidence Selection And Ranking for Reasoning Chains
20252 papers
- ICML (T1)Formal Mathematical Reasoning: A New Frontier in AI
- ACL (T1)Theorem Prover as a Judge for Synthetic Data Generation
20248 papers
- ICML (T1)Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving
- ICLR (T1)Don’t Trust: Verify – Grounding LLM Quantitative Reasoning with Autoformalization
- NeurIPS (T1)End-to-End Ontology Learning with Large Language Models
- PNAS (T1)Evaluating Language Models for Mathematics through Interactions
- International Conference on Interactive Theorem ProvingFormalising Half of a Graduate Textbook on Number Theory
- NeurIPS (T1)Multi-language Diversity Benefits Autoformalization
- NeurIPS (T1)Proving Theorems Recursively
- NeurIPS (T1)Repurposing Language Models into Embedding Models: Finding the Compute-Optimal Recipe
20231 paper
- ICLR (T1)Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
Where alumni went1 listed
Apply to EdinburghFall 2027
Not announced yet
Informatics PhD
- Round
- Rolling (funding consideration)
- Opens
- —
- GRE
- See program page
- English
- See program page
- Fee
- none
Not yet confirmed for this intake.
Similar labsnearest by research summary
- CNTsinghua
Qingyao Ai
- Large language models
- USUCLA
Vwani Roychowdhury
- Language & society
- USUW
Pang Wei Koh
- Trustworthy & safe ML
- USMichigan
Lu Wang
- Interpretability, evaluation & safety of LMs
- GBEdinburgh
Pasquale Minervini
- Knowledge, QA & retrieval
- SGNUS
Tat-Seng Chua
- Large language models
Your notes
Save this lab to keep notes.
Data
Checked against the lab homepage.
- Collected
- Verified
- Papers
- The lab homepage
- Members
- Lab homepage
- Alumni
- Lab homepage
Tiers are venue classifications, not lab rankings.