search

InternLM / InternLM-Math

Apache License 2.0
351 stars 20 forks source link

Impact of additional_imports on MiniF2F #33

Open njuyxw opened 6 days ago

njuyxw commented 6 days ago

I have a few questions regarding the 'additional_imports' argument. I noticed that the BFS prover sets additional_imports=['Mathlib.Tactics']. Could you please clarify if this has any positive impact on proving minif2f? I did not find any usage of it in Reprover (https://github.com/lean-dojo/ReProver). If additional_imports=[] is set, are there certain math problems in minif2f that cannot be proven? If so, why? Thank you very much for your assistance.

objecti0n commented 5 days ago

This code is internally used for testing MiniF2F and Compfiles. Compfiles use this as default import.

njuyxw commented 4 days ago

I encountered an issue while running proofsearch_internLM2-plus.py. When executing the line 'with Dojo(theorem, hard_timeout=timeout,additional_imports=["Mathlib.Tactic"]) as (dojo, init_state): ', lean_dojo throws an error: 'lean_dojo.interaction.dojo:_read_next_line:530 - MiniF2F/Test.lean:1:0: error: object file './.lake/packages/mathlib/.lake/build/lib/Mathlib/Tactic.olean' of module Mathlib.Tactic does not exist'

However, the code runs successfully when I remove 'additional_imports=[]'. This problem appears unrelated to the version of lean_dojo based on my troubleshooting efforts. I am utilizing the minif2f4.7.0 dataset with lean version 4.7.0. I am uncertain about the cause of this error, hence I asked about the impact of using 'additional_imports=["Mathlib.Tactic"]' and whether this is allowed when proving mathematical problems in minif2f4.7.0.