experiment: Proof search function from llemma_formal2formal

[slimtune2023]

Hello! I implemented the proof search function from Welleck's llemma_formal2formal project and tested it on some base theorems (the ones used in the pantograph/server.py tests).

The main additions are listed below:

• Implemented and verified proof search function capabilities using pantograph
• Verified logging capabilities with general and detailed theorem-specific logs supported
• Added support for proof search with the OpenAI LLM API (in addition to the previous support already there for vllm-based models)

Thank you!

[lenianiva]

I'll put this branch on hold before the NeurIPS deadline since you weren't added to the authors list. We can aim for the workshop paper for TACAS.

NeurIPS has extended the deadline for adding authors. You can join the author list if we get this experiment going.

[lenianiva]

On proof_search.py:287, the first goal of a given state is handled. When do you handle other goals?

[slimtune2023]

I am not sure if this is exactly how the GoalState variable works with pantograph and Lean 4 in general, but I was under the impression that when a goal is complete, it is removed from the list of goals in the given GoalState variable. Then, with multi-goal states, it would go through the goals individually until the entire state is solved. Then, just focusing the on the first goal of a given state would be sufficient in proving the entire theorem.

[lenianiva]

I am not sure if this is exactly how the GoalState variable works with pantograph and Lean 4 in general, but I was under the impression that when a goal is complete, it is removed from the list of goals in the given GoalState variable. Then, with multi-goal states, it would go through the goals individually until the entire state is solved.

No that is not how it works. I intentionally designed it so that each goal has to be solved individually, so if a state has goal 0,1,2, there would be calls to goal_tactic(state, 0|1|2, ...). This is (mostly) an and-or tree

[slimtune2023]

Just to confirm, when a goal is proved, it is removed from the GoalState goals array right? Would the index of the remaining goals then be shifted up? I guess one confusing thing is that the is_solved function for the GoalState returns whether the goals array is empty or not, so it seems like the goals are deleted as they are proved.

[lenianiva]

Just to confirm, when a goal is proved, it is removed from the GoalState goals array right? Would the index of the remaining goals then be shifted up? I guess one confusing thing is that the is_solved function for the GoalState returns whether the goals array is empty or not, so it seems like the goals are deleted as they are proved.

every time you execute a tactic on a goal state, the state itself doesn't change, but it produces a new state which can have 0 or more goals. if it has 0 goals and isn't coupled (i think i didn't implement this part), the state is solved.

[lenianiva]

Take a look at this: #10

[lenianiva]

Were you able to get this to work? If you have trouble with the proof search loop, I'm about to add a new feature where Pantograph will automatically give the next goal to the user to solve. #11

[lenianiva]

I modified the pantograph/ library and removed all non-essential dependencies from there (as should any good python package). Could you move your experimental code into experiments/...?