Elamur Research⌕
☰
home / papers / 2023 / TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models

TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models

Paper · 2023 · Jing Xiong, Jianhao Shen, Ye Yuan et al.

Summary

TRIGO is a benchmark for testing whether generative language models can perform formal proof reduction that depends on numerical manipulation, such as grouping and factoring terms or substituting equivalent angle values. The authors argue that existing automated theorem proving benchmarks rarely test this skill and mostly test symbolic inference. They collected trigonometric simplification problems from the Chinese problem bank "tiku" and from other websites. Using custom interactive software, they annotated each reduction step against a bank of 85 transformation rules and converted the proofs into Lean. A Lean-Gym-based generator then produced synthetic problems of controlled difficulty and distribution.

Models generate tactics step by step, and Lean-Gym checks them. Real-world problems remain difficult: pass rates are only around 23–33% on TRIGO-real and 21–26% on TRIGO-web. GPT-4 invents tactics that do not exist in Lean. Every model scores zero when angle values are larger than those seen in training. The benchmark therefore exposes clear limits in both formal and numerical reasoning.

Key points

  • Data splits:
    • TRIGO-real has 427 manually annotated problems from "tiku".
    • TRIGO-web has 453 deduplicated web problems and serves as the test set.
    • TRIGO-gen has three synthetic subsets (TG-1/2/3) that vary in proof length and difficulty.
  • Annotation: Each annotated step is parsed with sympy and matched as an expression tree against the 85-rule bank. For comparison, earlier work used 18 axioms and 9 transformations.
  • Decoding and search:
    • Sampling beats beam search, reaching 32.55 on TRIGO-real versus 23.25.
    • BFS clearly beats MCTS on TRIGO-gen, with 77.29 versus 51.59 on TG-1. The authors attribute this to MCTS lacking a good value function.
  • Expert iteration: Seven rounds of expert iteration with GPT-2 L-PACT raise pass rates on all TG subsets. The largest gain is 10.9% on TG-2.
  • Out-of-distribution test: Angles were extended to values such as π/5 and π/7, and the maximum K rose from 100 to 1000. On this test, all models, including the strongest baseline GPT-2 L-PACT-D, scored a 0 pass rate.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Peking UniversityBeijing · China335 works · 43,758 citations🎓Chinese University of Hong KongHong Kong · China176 works · 17,536 citations🏢Huawei TechnologiesShenzhen · China105 works · 15,705 citations🎓Sun Yat-sen UniversityGuangzhou · China80 works · 9,799 citations🎓City University of Hong KongHong Kong · China62 works · 3,563 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksArts and Humanities · 17,959 worksLanguage and Linguistics · 17,789 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as 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 and Qun Liu. 2023. TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models. Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2023.emnlp-main.711 · arXiv 2310.10180

@inproceedings{xiong2023trigo,
  title = {{TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models}},
  author = {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 and Qun Liu},
  booktitle = {Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing},
  year = {2023},
  doi = {10.18653/v1/2023.emnlp-main.711},
  eprint = {2310.10180},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.18653/v1/2023.emnlp-main.711}
}

References

39 references, 31 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Bruce Abramson and Richard E Korf. 1987. A model of two-player evaluation functions. In AAAI, pages 90–94. find
  2. Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. 2019a. HOList: An environment for machine learning of higher order logic theorem proving. In ICML, pages 454–463. PMLR.
  3. Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, and Christian Szegedy. 2019b. Learning to reason in large theories without imitation. arXiv preprint arXiv:1905.10501.
  4. Yoshua Bengio, Réjean Ducharme, and Pascal Vincent. 2000. A neural probabilistic language model. NeurIPS, pages 932–938. find
  5. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. 2021. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168.
  6. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The lean theorem prover (system description). In ICAD, pages 378–388. find
  7. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. 2021. Proof artifact co-training for theorem proving with language models. In ICLR.
  8. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. Measuring mathematical problem solving with the MATH dataset. In NeurIPS.
  9. Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. 2022. Thor: Wielding hammers to integrate language models and automated theorem provers. NeurIPS, 35:8360– 8373.
  10. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In ICLR.
  11. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. 2021. Isarstep: a benchmark for high-level mathematical reasoning. In ICLR.
  12. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. 2023. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.04295.
  13. Pan Lu, Ran Gong, Shibiao Jiang, Liang Qiu, Siyuan Huang, Xiaodan Liang, and Song-Chun Zhu. 2021. Inter-GPS: Interpretable geometry problem solving with formal language and symbolic reasoning. In ACL, pages 6774–6786.
  14. Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, et al. 2023. Self-refine: Iterative refinement with self-feedback. arXiv preprint arXiv:2303.17651. mathlib. 2020. The lean mathematical library. In Proceedin…
  15. Norman Megill and David A Wheeler. 2019. Metamath: a computer language for mathematical proofs. Lulu. com.
  16. OpenAI. 2023. GPT-4 technical report. arXiv preprint arXiv:2303.08774.
  17. Arkil Patel, Satwik Bhattamishra, and Navin Goyal. 2021. Are NLP models really able to solve simple math word problems? In ACL, pages 2080–2094.
  18. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. 2023. Formal mathematics statement curriculum learning. In ICLR.
  19. Stanislas Polu and Ilya Sutskever. 2020. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393.
  20. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al. 2019. Language models are unsupervised multitask learners. OpenAI blog, page 9. find
  21. Diederik P. Kingma and Jimmy Ba. 2015. Adam: A method for stochastic optimization. In ICLR.
  22. David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. 2019. Analysing mathematical reasoning abilities of neural models. In ICLR.
  23. Rik Koncel-Kedziorski, Subhro Roy, Aida Amini, Nate Kushman, and Hannaneh Hajishirzi. 2016. MAWPS: A math word problem repository. In ACL, pages 1152–1157. find
  24. Jianhao Shen, Yichun Yin, Lin Li, Lifeng Shang, Xin Jiang, Ming Zhang, and Qun Liu. 2021. Generate & rank: A multi-task framework for math word problems. In Findings of EMNLP, pages 2269–2279. find
  25. Guillaume Lample, Timothée Lacroix, Marie-Anne Lachaux, Aurélien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. 2022. Hypertree proof search for neural theorem proving. In NeurIPS, pages 26337–26349.
  26. David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. 2017. Mastering the game of go without human knowledge. nature, 550(7676):354–359. find
  27. Yan Wang, Xiaojiang Liu, and Shuming Shi. 2017. Deep neural solver for math word problems. In EMNLP, pages 845–854. find
  28. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2022. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. In ICLR.
  29. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hanna Hajishirzi, Yejin Choi, and Kyunghyun Cho. 2021. Naturalproofs: Mathematical theorem proving in natural language. In NeurIPS.
  30. Yuhuai Wu, Albert Q. Jiang, Jimmy Ba, and Roger Baker Grosse. 2021a. INT: an inequality benchmark for evaluating generalization in theorem proving. In ICLR.
  31. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with large language models. NeurIPS, pages 32353–32368.
  32. Yuhuai Wu, Markus N. Rabe, Wenda Li, Jimmy Ba, Roger B. Grosse, and Christian Szegedy. 2021b. LIME: learning inductive bias for primitives of mathematical reasoning. In ICML, pages 11251–11262.
  33. Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. 2023. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656.
  34. Jing Xiong, Chengming Li, Min Yang, Xiping Hu, and Bin Hu. 2022. Expression syntax information bottleneck for math word problems. In SIGIR, pages 2166–2171.
  35. Jiong Xiong, Zixuan Li, Chuanyang Zheng, Zhijiang Guo, Yichun Yin, Enze Xie, Zhicheng Yang, Qingxing Cao, Haiming Wang, Xiongwei Han, Jing Tang, Chengming Li, and Xiaodan Liang. 2023. Dq-lore: Dual queries with low rank approximation re-ranking for in-context learning. arXiv preprint arXiv:2310.0295…
  36. Kaiyu Yang and Jia Deng. 2019. Learning to prove theorems via interacting with proof assistants. In ICML, pages 6984–6994.
  37. Kaiyu Yang, Aidan M Swope, Alex Gu, Rahul Chala-mala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2023. Leandojo: Theorem proving with retrieval-augmented language models. arXiv preprint arXiv:2306.15626.
  38. Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. 2023. Metamath: Bootstrap your own mathematical questions for large language models. arXiv preprint arXiv:2309.12284.
  39. Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. 2023. Lyra: Orchestrating dual correction in automated theorem proving. arXiv preprint arXiv:2309.15806.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/xiong-2023-trigo-benchmarking-formal-mathematical-proof/