Skip to content

issues Search Results · repo:InternLM/InternLM-Math language:Python

Filter by

30 results
 (58 ms)

30 results

inInternLM/InternLM-Math (press backspace or delete to remove)

InternLM/InternLM-Math
opencompass版本

您好，请问你们使用的是哪个opencompass的版本，我下载了新版的测评时候报错，看样子应该是新旧版本的路径不一样
  • Castrol68
  • 1
  • Opened 
    on Feb 12
  • #47

InternLM/InternLM-Math
critic model on multiple goals

Hi, I am trying to reproduce the proof search using the critic model. May I check If the current state has multiple goals, then how do we use the critic model evaluate it? 1. just join all the goals ...
  • efessas
  • 2
  • Opened 
    on Dec 30, 2024
  • #46

InternLM/InternLM-Math
Release of REPL

Thanks for this excellent work. Is there any timeline for the release of the REPL? How do you use repl to check the correctness of our LEAN-Workbook? For our implemented repl, we are still working ...
  • DDDOH
  • Opened 
    on Nov 21, 2024
  • #45

InternLM/InternLM-Math
How to reproduce the results on ProofNet

Hello, thank you for your great work and I m trying to reproduce your results. However, it seems that you only released the code for MiniF2F, so I m wondering how to reproduce the results on ProofNet. ...
  • Car-pe
  • Opened 
    on Nov 15, 2024
  • #44

InternLM/InternLM-Math
How to set the prompt when trying to get the first line of proof

Thanks for this great work! I am trying to play with the model: 1. as mentioned in the paper (internlm2.5 step prover), the prompt consists of theorem name, proof before, and tactic state. I wonder ...
  • bhwangfy
  • 3
  • Opened 
    on Nov 1, 2024
  • #43

InternLM/InternLM-Math
About critic-guide search in InternLM2.5-StepProver

Thank you for your work on InternLM2.5-StepProver. I have two questions: 1. The difference between critic-guide search and BFS lies in using the critic model s score to guide the search process. ...
  • LuoKaiGSW
  • 6
  • Opened 
    on Oct 25, 2024
  • #42

InternLM/InternLM-Math
Kindly ask about the size of lean-workbook

Hi authors, You mentioned that Our dataset contains 57231 problems in the split of Lean Workbook and 82893 problems in the split of Lean Workbook Plus. We provide the natural language statement, answer, ...
  • freyaya123
  • 4
  • Opened 
    on Oct 17, 2024
  • #41

InternLM/InternLM-Math
Is the proof included in the Lean-workbook ensured to be correct?

I used the header you provided and integrated the formal_statement and proof. Only to find that some cases pass lean server and some don t. For example: theorem lean_workbook_26 (x : ℝ) (hx : 0 x) : x ...
  • yyyhz
  • 2
  • Opened 
    on Sep 20, 2024
  • #40

InternLM/InternLM-Math
Regarding the proofs (and theorems) in Lean-Github

The dataset is great! And It s nice of you to open source them. However, I don t understand the meaning of some of these fields very well, so to prevent misunderstandings I hope you can clarify further. ...
  • yyyhz
  • 1
  • Opened 
    on Aug 5, 2024
  • #39

InternLM/InternLM-Math
How to display a formal data set correctly

I have already configure LeanDojo. But I am not familiar with LEAN language, so when I use minif2f dataset, there are some errors like \u2115 with json. For example: { full_name : amc12a_2019_p21 , statement ...
  • yyyhz
  • 1
  • Opened 
    on Aug 1, 2024
  • #38
Issue origami icon

Learn how you can use GitHub Issues to plan and track your work.

Save views for sprints, backlogs, teams, or releases. Rank, sort, and filter issues to suit the occasion. The possibilities are endless.Learn more about GitHub Issues
ProTip! 
Restrict your search to the title by using the in:title qualifier.
Issue origami icon

Learn how you can use GitHub Issues to plan and track your work.

Save views for sprints, backlogs, teams, or releases. Rank, sort, and filter issues to suit the occasion. The possibilities are endless.Learn more about GitHub Issues
ProTip! 
Press the
/
key to activate the search input again and adjust your query.
Issue search results · GitHub