search

InternLM / InternLM-Math

State-of-the-art bilingual open-sourced Math reasoning LLMs.
Apache License 2.0
410 stars 25 forks source link

Can InternLM2-Step-Prover be used to solve MATH or GMS8K with Lean? #37

Closed yyyhz closed 1 month ago

yyyhz commented 1 month ago

I wonder if I can use InternLM2-Step-Prover to solve MATH or GMS8K with Lean. Or the Lean can only be used to solve problems like minF2F? And also I find some models can solve the formal and informal problems at the same time. I would like to know what programming language is used for one model to reason both types of problems, is it python for reasoning formal problems and Lean for reasoning informal problems?

objecti0n commented 1 month ago

If you can formalize problems in LEAN, you can use InternLM2-Step-Prover to try to prove it. MiniF2F has a large overlap with MATH algebra and MATH number theory.

For our models which can solve formal and informal problems at the same time. It use LEAN 4 to solve formal problems and use natural languages or Python to solve informal problems.

yyyhz commented 1 month ago

If you can formalize problems in LEAN, you can use InternLM2-Step-Prover to try to prove it. MiniF2F has a large overlap with MATH algebra and MATH number theory.

For our models which can solve formal and informal problems at the same time. It use LEAN 4 to solve formal problems and use natural languages or Python to solve informal problems.

Thank you so much for your sincere reply! And I still have some questions:

  1. Can I translate math problems' cot answers from natural language to LEAN with your models? If can, which model is better?
  2. What are the definitions of formal and informal math problems? And how can I can formalize problems in LEAN? I can't wait to try and see if LEAN can solve problems like GMS8K.
objecti0n commented 1 month ago
  1. Use InternLM-Math-Plus series for translation via "https://github.com/InternLM/InternLM-Math/blob/main/leanworkbook/inference_translate_answer.py"
  2. We simply consider formal math problems are stated via LEAN, Coq, or Isabelle language as formal problems. If it is stated via natural language, it is informal. If you use the old version of InternLM-Math (instead of InternLM-Math-Plus), it can solve gsm8k by LEAN 3. An example: Example