Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

experiment: Proof search function from llemma_formal2formal #6

Draft
wants to merge 3 commits into
base: brando
Choose a base branch
from

Conversation

slimtune2023
Copy link

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
Copy link
Owner

lenianiva commented May 30, 2024

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.

Copy link
Owner

@lenianiva lenianiva left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@slimtune2023
Copy link
Author

slimtune2023 commented Jun 3, 2024

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
Copy link
Owner

lenianiva commented Jun 3, 2024

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
Copy link
Author

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
Copy link
Owner

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
Copy link
Owner

Take a look at this: #10

@lenianiva
Copy link
Owner

lenianiva commented Sep 7, 2024

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 lenianiva marked this pull request as draft October 6, 2024 05:36
@lenianiva
Copy link
Owner

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/...?

@lenianiva lenianiva added the experiment Experiments label Oct 12, 2024
@lenianiva lenianiva changed the title Implemented proof search function from llemma_formal2formal with pantograph experiment: Implemented proof search function from llemma_formal2formal with pantograph Oct 13, 2024
@lenianiva lenianiva changed the title experiment: Implemented proof search function from llemma_formal2formal with pantograph experiment: Proof search function from llemma_formal2formal Oct 13, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
experiment Experiments
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants