Thoughts on prefixing tactic applications with 'all:'

[magmkri]

Hi!

As I understand it tactics are by default only applied to the first subgoal in a given proof state. However, this can be changed by superseding the tactic with the all: keyword. But because of the timeout included when sending tactics via eval_env.py the tactic application fails.

CoqGym/eval_env.py

Line 76 in cde1f3f

command = "timeout %d (%s)." % (time_left, command[:-1])

It turns out all: has to come before timout. A simple, ad-hoc, fix is:

if "all:" in command[:-1]:
	command = "all: timeout %d (%s)." % (time_left, command[:-1].replace("all: ", ""))
else:
	command = "timeout %d (%s)." % (time_left, command[:-1])

Drawing the proof tree for a (simple) agent's proof, this seems shorten the proof search somewhat:

Any thoughts on adding support for all: in ProofEnv? :)

As a related sidenote to this:
It also seems that checking only the first (sub)goal signature can make agent's struggle to prove certain theorems:

CoqGym/ASTactic/agent.py

Line 304 in cde1f3f

if sig in first_goal_signatures or len(script) >= self.opts.depth_limit:

Certain proof trees can become simpler by changing this to checking the concatenation of all subgoal signatures:


But again: in these kinds of proof states using all: fixes this implicitally, and the result is an even shorter proof tree:

Hope this makes sense :). Thanks in advance!

[yangky11]

Hi Magus,

That's an interesting point. But I cannot see the figures. Could you fix them?

[magmkri]

Hi,

Yes, of course! I think they should work now. Just in case, I'm attaching the last three ('checking first signature', 'checking all signatures', and 'using :all') here, as they illustrate the point. This is of course not a major thing at all – it was more something I was curious about, as it seems to be able to impact the search tree somewhat :).

Btw, if it seems strange why the yellow path in the first image does not explore the use of 'eauto', I belive it is because that would result in a (first subgoal) signature identical to the one obtained after applying 'constructor' to the root (hence why checking for a concatenation of the subgoal signatures generates a simpler proof tree in the second image: each state is "more strictly unique"). (The colors along the edges are not important. They just signal whenever the depth first search backtracks, and explores a new path).

[yangky11]

Thanks! How does the agent decide whether or not to use all:? Does it use all: for all tactics?

[magmkri]

I simply allowed the agent to use all: for all tactics, because I was mostly curious to see what impact it had out-of-the-box. But even though this might help an agent in the proof search, I decided not to include it in the agents I'm testing now. It didn't seem that interesting to help an agent using a "trick" likes this, when the goal is see the impact of different embedding strategies, training paradigms, etc.

However, perhaps it would be more interesting to include all: if it was something the agent had to make a decision about. For example having a model dedicated to predicting the usefullness of all:, or if using a context free grammar (as ASTactic does) perhaps somehow include it in the grammar. Of course, the agent would have to embedd not just a the first subgoal in a given state, but all goals in the state when deciding what to do with all:.

[yangky11]

I see, makes sense. I think for now people can just use the hacky way to support all: as you did earlier. And we'll see what's the best way of incorporating it if it turns out to be useful.

[magmkri]

Absolutely 👍🏽

Thanks!