-
Notifications
You must be signed in to change notification settings - Fork 40
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
Format state_before/state_after datapoints as partial updates #17
Format state_before/state_after datapoints as partial updates #17
Conversation
I didn't understand this data point generated by
Where is |
The idea is - we want the model to respond to two types of queries:
The datapoint without any new hypothesis is to serve the query 1) - i.e. user doesn't specify what hypothesis appear only the goal change, The other datapoint with
I'm not sure if the model would find it close to the |
That makes sense. Thanks for the explanation. I think it should be good as long as examples in testing are presented to the model in the same format as in training. I'll start training the model with updated data asap, which will finish in one week. |
@antonkov It looks like the code doesn't handle |
Oh right, good catch. Should be straightforward to add a check |
@antonkov I fixed this error, but there are other cases that cannot be handled by the parsing code. For example, |
An example goal that your current code cannot parse:
|
Yes thanks, I'll iterate to fix the errors and send a new PR |
Generate datapoints in the new format:
with following differences from simple state_before/state_after approach:
It's like a deepening lense, the model sees that it has a particular before state ⊢ p ∧ q, and it sees that it wants to have ⊢ p. The model does not care about anything else.
Examples:
trivial
new format
intro h
generates two datapointsapply And.intro
generates two data pointsrw [Nat.add_comm a b]
new format is two separate datapoints