FormulaNet

FormulaNet copied to clipboard

The command `python src/data_util/generate_hol_dataset.py data/hol_raw_data data/hol_data` throws an error because the path `data/hol_raw_data` does not exist. The only way I got it to work was `python src/data_util/generate_hol_dataset.py data/raw_data data/hol_data`.

javipus

Hi, when I ran the batch_test.py, the command is " python batch_test.py --model FormulaNet-basic --log log_test.txt --dict_file data/dicts/hol_train_dict",but an error occured . The infomation is " size mismatch for l1.weight:...

AI-coder

Premise selection/Proof step classification?

2

From reading [0] it seems that you compare your approach to HolStep's baselines which operate on the task of "proof step classification" (not premise selection) as stated in [1]. Wouldn't...

spolu