QuantFactory/internlm2-step-prover-GGUF

pipeline_tag: text-generation license: other language:

• —en tags:
• —math

QuantFactory/internlm2-step-prover-GGUF

This is quantized version of internlm/internlm2-step-prover created using llama.cpp

Original Model Card

InternLM-Step-Prover

<div align="center">

<img src="https://raw.githubusercontent.com/InternLM/InternLM/main/assets/logo.svg" width="200"/> <div> </div> <div align="center"> <b><font size="5">InternLM-Math</font></b> ^{<a href="https://internlm.intern-ai.org.cn/"> <i><font size="4">HOT</font></i> </a>} <div> </div> </div>

A state-of-the-art LEAN4 step prover.

💻 Github 📊Dataset 📖 Paper </div>

InternLM-Step-Prover is a 7B language model trained on Lean-Github and multiple sythesis datasets. InternLM-Step-Prover achieves state-of-the-art performances on MiniF2F, ProofNet, and Putnam math benchmarks, showing its formal math proving ability in multiple domains.

Dialogue Example

### Input Example
DECL MyNat.mul_pow
GOAL a b n : N
⊢ (a * b) ^ n = a ^ n * b ^ n
### Output Example
PROOFSTEP induction n with t Ht

Performance

MiniF2F

Proofnet & Putnam

Citation and Tech Report

@misc{wu2024leangithubcompilinggithublean,
      title={LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover}, 
      author={Zijian Wu and Jiayu Wang and Dahua Lin and Kai Chen},
      year={2024},
      eprint={2407.17227},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/2407.17227}, 
}