Papers by Jianhao Shen
Aligning VLM Assistants with Personalized Situated Cognition (2025.acl-long)
Copied to clipboard
Yongqi Li, Shen Zhou, Xiaohu Li, Xin Miao, Jintao Wen, Mayi Xu, Jianhao Chen, Birong Pan, Hankun Kang, Yuanyuan Zhu, Ming Zhong, Tieyun Qian
| Challenge: | Existing studies on vision-language models aligned with general human objectives have not been successful because people with diversified backgrounds have different cognition even in the same situation. |
| Approach: | They propose to characterize individuals based on the sociological concept of Role-Set and then evaluate their actions to see whether personalized alignment is achieved. |
| Outcome: | The proposed framework constructs a cognition-aware and action-based reward model for personalized alignment. |
ComSearch: Equation Searching with Combinatorial Strategy for Solving Math Word Problems with Weak Supervision (2023.eacl-main)
Copied to clipboard
| Challenge: | Existing weakly-supervised methods for solving math word problems are expensive and time-consuming. |
| Approach: | They propose a weakly-supervised approach to solve math word problems . they propose 'comsearch' algorithm which compresses the search space by excluding mathematically equivalent equations. |
| Outcome: | The proposed algorithm can compress the search space by excluding mathematically equivalent equations. |
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. |
Joint Language Semantic and Structure Embedding for Knowledge Graph Completion (2022.coling-1)
Copied to clipboard
| Challenge: | Existing methods to complete knowledge triplets rely on structures or semantics, but use semantics to improve performance. |
| Approach: | They propose to embed semantics in the natural language description of knowledge triplets with their structure information. |
| Outcome: | The proposed method improves performance on knowledge graph benchmarks and on low-resource regimes. |
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. |
Generate & Rank: A Multi-task Framework for Math Word Problems (2021.findings-emnlp)
Copied to clipboard
| Challenge: | Existing studies formalize MWP as a generation task but mathematical expressions are prone to minor mistakes. |
| Approach: | They propose a ranking task for math word problem (MWP) that learns from its own mistakes and distinguishes between correct and incorrect expressions. |
| Outcome: | The proposed model outperforms baselines on the classical Math23k dataset and is 7% higher than the state-of-the-art. |
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. |
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. |