How come that executing tactics is more expensive than generating them?

[brando90]

I saw this on the original paper:

We run all testing experiments on machines with 16GB RAM and two Intel Xeon Silver 4114 CPU Cores. We do not use GPUs for testing since the speed bottleneck is executing tactics rather than generating tactics.

I was very curious (and surprised) this was the case. From the paper, to generate tactics we do need a neural net (NN). So I assumed that generating tactics as a tree can't be cheap (but if your not using a GPU you must be generating a tactic with NN/decoder using cpu). Can more details be given on how come executing a tactic is more expensive than generating terms? For example in pseudo code:

proof_state = <local_context, goal, env>  # 1
tactic = ASTactic(proof_state)  # 2
coqgym.execute(tactic, proof_state) # 3

is step 3 the slow step? So just doing a single step (since ASTactic only generates atomic tactics as far as I understand it) of an atomic tactic takes longer than a single step of a tactic generation? Is this the correct interpretation? Can we have numbers on how long each of these lines take?

Related, how long does it take on average (or median) to complete a proof using ASTactic as the method to select tactics?

[yangky11]

The time for executing tactics actually includes the depth-first search (DFS) for exploring different tactic candidates. During testing, we generate 20 tactics at each step and use DFS to search for the correct proof. During DFS, the prover will execute many incorrect tactics before finding a proof (or the time expires). So most time is spent on searching, executing, and backtracking. Indeed, generating tactics is not fast since neural networks are involved, but it's still much faster than searching. If the correct tactics were known in advance, executing tactics would be much faster than running the neural network.

For the average time of proving a theorem, maybe Table 2 in the paper is what you're looking for.