TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models. Xiong, J., Shen, J., Yuan, Y., Wang, H., Yin, Y., Liu, Z., Li, L., Guo, Z., Cao, Q., Huang, Y., Zheng, C., Liang, X., Zhang, M., & Liu, Q. October, 2023. arXiv:2310.10180 [cs]
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [link]Paper  doi  abstract   bibtex   
Automated theorem proving (ATP) has become an appealing domain for exploring the reasoning ability of the recent successful generative language models. However, current ATP benchmarks mainly focus on symbolic inference, but rarely involve the understanding of complex number combination reasoning. In this work, we propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability on formulas and its capability to manipulate, group, and factor number terms. We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system. We then automatically generate additional examples from the annotated samples to expand the dataset. Furthermore, we develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model's generalization ability. Our extensive experiments show our proposed TRIGO poses a new challenge for advanced generative LM's including GPT-4 which is pre-trained on a considerable amount of open-source formal theorem-proving language data, and provide a new tool to study the generative LM's ability on both formal and mathematical reasoning.
@misc{xiong_trigo_2023,
	title = {{TRIGO}: {Benchmarking} {Formal} {Mathematical} {Proof} {Reduction} for {Generative} {Language} {Models}},
	shorttitle = {{TRIGO}},
	url = {http://arxiv.org/abs/2310.10180},
	doi = {10.48550/arXiv.2310.10180},
	abstract = {Automated theorem proving (ATP) has become an appealing domain for exploring the reasoning ability of the recent successful generative language models. However, current ATP benchmarks mainly focus on symbolic inference, but rarely involve the understanding of complex number combination reasoning. In this work, we propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability on formulas and its capability to manipulate, group, and factor number terms. We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system. We then automatically generate additional examples from the annotated samples to expand the dataset. Furthermore, we develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model's generalization ability. Our extensive experiments show our proposed TRIGO poses a new challenge for advanced generative LM's including GPT-4 which is pre-trained on a considerable amount of open-source formal theorem-proving language data, and provide a new tool to study the generative LM's ability on both formal and mathematical reasoning.},
	urldate = {2024-01-16},
	publisher = {arXiv},
	author = {Xiong, Jing and Shen, Jianhao and Yuan, Ye and Wang, Haiming and Yin, Yichun and Liu, Zhengying and Li, Lin and Guo, Zhijiang and Cao, Qingxing and Huang, Yinya and Zheng, Chuanyang and Liang, Xiaodan and Zhang, Ming and Liu, Qun},
	month = oct,
	year = {2023},
	note = {arXiv:2310.10180 [cs]},
	keywords = {artificial intelligence, computation and language, generative language model, uses sympy},
}
Downloads: 0
About
Documentation
Keywords
Search
Users
Terms and Conditions of Use
Privacy Policy
Sitemap
© BibBase.org 2021