How does one select 10 premises in the environment during training time?

[brando90]

I saw in the paper that you choose 10 premises in the environment:

Encoding the goal and premises ASTactic encodes the current goal and premises into vectors. We include the entire local context and up to 10 premises in the environment, ex- cluding a large number of premises imported from libraries. A model could be more powerful if it is capable of selecting relevant premises from the entire environment, but that is left for future research.

I was wondering how during training you got those 10 premises. Do you pre-select them before training and that is how the data set was created so the a data loader can get a supervised learning data point (x=<local context, goal, env>, y=tac) ? Or did you do something else?

I guess I am unsure how you are getting the 10 premises from a static data set without the actual proving going with Coq during training (plus to select environment terms don't you need a premise selection model or something already to be able to choose them or how are you selecting the 10 premises for training/generating the data set)?

Thanks in advance Kaiyu!

[yangky11]

As shown here:

CoqGym/ASTactic/agent.py

Lines 34 to 41 in 37f93ce

	def filter_env(env):
	"Get the last 10 toplevel constants"
	filtered_env = []
	toplevel_consts = [const for const in env['constants'] if const['qualid'].startswith('SerTop')]
	for const in toplevel_consts[-10:]:
	ast = sexp_cache[const['sexp']]
	filtered_env.append({'qualid': const['qualid'], 'ast': term_parser.parse(ast)})
	return filtered_env

, we simply take the last 10 environment terms. This is motivated by the fact that terms defined close to the proof are more likely to be useful. However, this is indeed a very poor approximation. We did this because considering all environment terms is computationally infeasible.

[brando90]

So to make sure I understand, is that (last 10 premise selection) done when you create the data set (as a preprocessing step), right?

[yangky11]

It is called when extracting proof steps from the proofs.

CoqGym/ASTactic/extract_proof_steps.py

Line 50 in 37f93ce

def process_proof(filename, proof_data):

So the CoqGym dataset contains all environment terms, but we keep only the last 10 when preprocessing it into proof steps.