Feature ideas

[LasseBlaauwbroek]

@Zhang-Liao I'd like to gather some ideas for modifications of the features that we could try. Below are two initial ideas:

• Use de Bruijn indices for bound variables instead of placeholders
• Anonymous features: For local variables, we can recursively replace it's identifier with the features of the type of the variable
• Limit the size of the feature vector for large proof states
• Don't append feature counts directly to the features, but instead give them as weights to the models

If you have other ideas, please list them here.

[Zhang-Liao]

Features that indicate the proof state is wrong, e.g., the size of the state is too large

[Zhang-Liao]

Different features for _k_NN and online random forests

[LasseBlaauwbroek]

Can you be more specific?

[Zhang-Liao]

Statistics of the proof states, like the number of nodes

[Zhang-Liao]

Can you be more specific?

I am not sure now. I think we need to run an ablation study on random forests.
I write it here because although my code of features is wrong, online random forests perform better with the wrong features than the correct ones. Meanwhile, the results in "offline-simulator" show that the top-1 accuracy of online forests is 3% better than kNN. However, with complex features, random forests are slightly worse than kNN. The above observation indicates the complex features may best suit kNN while not very appropriate for random forests.