Papers by Botao Li
Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4 (2026.acl-long)
Copied to clipboard
Chengwu Liu, Yichun Yin, Ye Yuan, Jiaxuan Xie, Botao Li, Siqi Li, Jianhao Shen, Yan Xu, Lifeng Shang, Ming Zhang
| Challenge: | Existing approaches to solving mathematical problems fall into two broad categories: informal methods and formal methods. |
| Approach: | They propose to use LLM natural-language reasoning to discover answers . they introduce Discover And Prove framework that rewrites Hard Mode statements into Easy Mode ones for existing ATP provers. |
| Outcome: | The proposed framework can be used to prove hard mode statements on ATP benchmarks. |
AutoSDT: Scaling Data-Driven Discovery Tasks Toward Open Co-Scientists (2025.emnlp-main)
Copied to clipboard
Yifei Li, Hanane Nour Moussa, Ziru Chen, Shijie Chen, Botao Yu, Mingyi Xue, Benjamin Burns, Tzu-Yao Chiu, Vishal Dey, Zitong Lu, Chen Wei, Qianheng Zhang, Tianyu Zhang, Song Gao, Xuhui Huang, Xia Ning, Nesreen K. Ahmed, Ali Payani, Huan Sun
| Challenge: | AutoSDT-5K is the only automatically collected and the largest open dataset for data-driven scientific discovery. |
| Approach: | They propose an automatic pipeline that collects high-quality coding tasks in real-world data-driven discovery workflows. |
| Outcome: | The proposed pipeline synthesizes accurate tasks and tasks from a dataset of 5,404 tasks covering four scientific disciplines and 756 Python packages. |
EMO-RL: Emotion-Rule-Based Reinforcement Learning Enhanced Audio-Language Model for Generalized Speech Emotion Recognition (2025.findings-emnlp)
Copied to clipboard
| Challenge: | Recent advances in reinforcement learning (RL) have shown promise in improving LALMs’ reasoning abilities, but their performance in affective computing tasks remains suboptimal. |
| Approach: | They propose a framework incorporating reinforcement learning with two key innovations: Emotion Similarity-Weighted Reward (ESWR) and Explicit Structured Reasoning (ESR). |
| Outcome: | The proposed framework improves LALMs' reasoning abilities on MELD and IEMOCAP datasets and shows strong generalization. |