AI-coder

Hi ,I am currently working on premise selection (HOLSTEP : A MACHINE LEARNING DATASET FOR HIGHER - ORDER LOGIC THEOREM PROVING), I questioned about this issue: for a conjecture instance,...

Illegal begin of top_parse

1

When I input " 'x+1' " in hol-light system , it responses "Illegal begin of top_parse", whats wrong with it ?, Thanks.

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:...