Papers by Haiming Wang
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. |