Satellite (Guangzhou)

Huajian Xin is currently a PhD student at the University of Edinburgh, supervised by Dr. Wenda Li, and is concurrently interning with the Seed team at ByteDance. His research focuses on automated theorem proving using large language models within formal mathematical environments. He specializes in autonomous agents capable of autoformalization and knowledge library learning, striving to advance deep integration and synergy between large language models and formal systems. His representative works include the leading open-source theorem proving model series DeepSeek Prover, and lemma decomposition and knowledge accumulation system LEGO-Prover, and proof engineering benchmark APE-Bench.

Liangming Pan is an Assistant Professor at the College of Information Science, University of Arizona. Previously, I was a postdoctoral scholar at the Natural Language Processing Group, University of California, Santa Barbara (UCSB), where I was fortunate to be advised by Prof. William Yang Wang. I completed my PhD from National University of Singapore in 2022, where I was advised by Prof. Min-Yen Kan and Prof. Tat-Seng Chua and worked on complex question answering and generation. His primary research lies in the area of natural language processing and machine learning. The overarching goal of my research is: how to build trustworthy large language models that are logical, truthful, and safe.