Papers by Jianhao Ye
PALT: Parameter-Lite Transfer of Language Models for Knowledge Graph Completion (2022.findings-emnlp)
Copied to clipboard
| Challenge: | Pretrained language models (LMs) are a powerful transfer learning approach for knowledge graph (KG) completion. |
| Approach: | They propose a parameter-lite transfer learning approach for pretrained language models for knowledge graph (KG) completion. |
| Outcome: | The proposed model outperforms the state-of-the-art models on a knowledge graph completion benchmark by tuning 1% of the parameters. |
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models (2023.emnlp-main)
Copied to clipboard
Jing Xiong, Jianhao Shen, Ye Yuan, Haiming Wang, Yichun Yin, Zhengying Liu, Lin Li, Zhijiang Guo, Qingxing Cao, Yinya Huang, Chuanyang Zheng, Xiaodan Liang, Ming Zhang, Qun Liu
| Challenge: | Automated theorem proving (ATP) benchmarks focus on symbolic inference but rarely involve understanding complex number combination reasoning. |
| Approach: | They propose a benchmark that requires a model to reduce a trigonometric expression with step-by-step proof and evaluates a generative LM’s reasoning ability on formulas and ability to manipulate, group, and factor number terms. |
| Outcome: | The proposed benchmark evaluates a generative LM’s reasoning ability on formulas and ability to manipulate, group, and factor number terms. |
DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function (2023.acl-long)
Copied to clipboard
Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li, Xiaodan Liang
| Challenge: | Recent advances in neural theorem-proving resort to large language models and tree searches. |
| Approach: | They propose a Dynamic-Tree Driven Theorem Solver to accommodate general theoremes by guiding the search procedure with state confidence and proof-level values. |
| Outcome: | The proposed method outperforms state-of-the-art methods on two popular theorem-proving datasets with a 6.65% improvement on average in terms of success rate. |
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. |
Takin-VC: Expressive Zero-Shot Voice Conversion via Adaptive Hybrid Content Encoding and Enhanced Timbre Modeling (2025.acl-long)
Copied to clipboard
Yang Yuguang, Yu Pan, Jixun Yao, Xiang Zhang, Jianhao Ye, Hongbin Zhou, Lei Xie, Lei Ma, Jianjun Zhao
| Challenge: | Expressive zero-shot voice conversion (VC) aims to modify source timbre to match unseen speaker . existing zero- shot VC systems struggle to reproduce paralinguistic information in highly expressive speech . |
| Approach: | They propose a framework for expressive zero-shot voice conversion that uses hybrid content encoding and memory-augmented context-aware timbre modeling. |
| Outcome: | The proposed framework surpasses state-of-the-art VC systems in speech naturalness, speaker similarity, and speaker similarness. |
Measuring Social Norms of Large Language Models (2024.findings-naacl)
Copied to clipboard
| Challenge: | Existing datasets that evaluate a general understanding of social science are inadequate to understand social norms. |
| Approach: | They propose a multi-agent framework to improve large language models’ ability to understand social norms by comparing them to elementary students. |
| Outcome: | The proposed framework improves large language models to be on par with humans. |