InternLM-Math-Plus

Stream: Machine Learning for Theorem Proving

[Zijian Wu]

We released a series of math LLM named InternLM-Math-Plus, of sizes 1.8B, 7B, 20B, and 8x22B. Our models are equipped with COT reasoning, code-interpreter reasoning, and LEAN 4 abilities (43.4% pass@1 on MiniF2F-test set).

Demo: https://huggingface.co/spaces/internlm/internlm2-math-7b

Model: https://huggingface.co/internlm/internlm2-math-plus-mixtral8x22b

Code: https://github.com/InternLM/InternLM-Math

Arxiv: https://arxiv.org/abs/2402.06332

[Huajian Xin]

Very good job! I would like to ask if pass@1 here refers to tree search once or model generation once?

[Zijian Wu]

It is tree search once (like HyperTree Proof Search's definition). In addition, the tree search width is 32, following the setting of llemma.