david-a-wheeler
commented
5 years ago I re-ran the whole thing again, with 8 hours of training before killing (in the 3 cases where it had to be stopped), and I don't see a real difference. Here's the tail of the output:
training loss = 0.633, outputs = 65.5 63.5, model_time = 0.31677, 0.00000, 0.training loss = 0.633, outputs = 65.5 63.4, model_time = 0.31705, 0.00000, 0.31438, at 2018-12-29 23:46:56+ kill 4715
+ sleep 10
+ kill -0 4715
+ return 0
+ cp weights/pred/train.parameters searcher/payout.parameters
+ cp weights/pred/train.weights searcher/payout.weights
+ python3 run_script_ordered.py
tautologies: 12843
wff variables: 18
class variables: 27
set variables: 20
936 constructor axioms with arity 0
38 constructor axioms with arity 1
57 constructor axioms with arity 2
38 constructor axioms with arity 3
8 constructor axioms with arity 4
3 constructor axioms with arity 5
1 constructor axioms with arity 6
1 constructor axioms with arity 7
1 constructor axioms with arity 8
timeout (min) (default: 1)? num passes (default: 1000)?search beam width (default: 10)? hyp bonus (0 in the paper, but 10 may give better results) (default: 0)?proposition iin2 (24513): 0/2720 (with 0 steps)
None
Config(): added 1088 tokens to dictionary
Config(): added 1088 tokens to dictionary
Config(): added 1088 tokens to dictionary
{'statement_GRUb_forward_0.Wz', 'hyp_GRUb_forward_0.W', 'main_first_b', 'last_b_', 'main_b_0', 'attention_B', 'forward_h_start0', 'main_first_W', 'main_W_0', 'hyp_GRUb_forward_0.Wr', 'statement_GRUb_forward_0.br', 'statement_GRUb_forward_0.Wr', 'statement_GRUb_forward_0.W', 'statement_GRUb_forward_0.bz', 'last_W_', 'hyp_GRUb_forward_0.br', 'hyp_GRUb_forward_0.bz', 'hyp_GRUb_forward_0.Wz', 'L'}
{'W', 'main_hyp_GRUb_forward_0.bz', 'main_statement_GRUb_forward_0.br', 'main_first_b', 'main_hyp_GRUb_forward_0.W', 'prop_W_0', 'main_b_0', 'main_statement_GRUb_forward_0.bz', 'prop_forward_h_start0', 'main_statement_GRUb_forward_0.Wz', 'L', 'attention_B', 'prop_first_b', 'main_hyp_GRUb_forward_0.br', 'prop_first_W', 'main_first_W', 'main_statement_GRUb_forward_0.Wr', 'main_W_0', 'main_hyp_GRUb_forward_0.Wz', 'main_forward_h_start0', 'main_hyp_GRUb_forward_0.Wr', 'prop_b_0', 'main_statement_GRUb_forward_0.W'}
in saved but not new
{'W', 'prop_first_b', 'main_hyp_GRUb_forward_0.bz', 'main_statement_GRUb_forward_0.br', 'main_hyp_GRUb_forward_0.br', 'prop_first_W', 'main_statement_GRUb_forward_0.Wr', 'main_hyp_GRUb_forward_0.W', 'main_hyp_GRUb_forward_0.Wz', 'main_statement_GRUb_forward_0.W', 'prop_W_0', 'main_forward_h_start0', 'main_hyp_GRUb_forward_0.Wr', 'main_statement_GRUb_forward_0.bz', 'prop_forward_h_start0', 'prop_b_0', 'main_statement_GRUb_forward_0.Wz'}
in new but not saved
{'hyp_GRUb_forward_0.W', 'hyp_GRUb_forward_0.Wr', 'statement_GRUb_forward_0.br', 'last_b_', 'forward_h_start0', 'hyp_GRUb_forward_0.Wz', 'statement_GRUb_forward_0.Wr', 'statement_GRUb_forward_0.W', 'statement_GRUb_forward_0.bz', 'last_W_', 'hyp_GRUb_forward_0.br', 'hyp_GRUb_forward_0.bz', 'statement_GRUb_forward_0.Wz'}
missing hyp_GRUb_forward_0.Wz
False
['L', 'attention_B', 'main_hyp_GRUb_forward_0.Wz', 'main_hyp_GRUb_forward_0.bz', 'main_hyp_GRUb_forward_0.Wr', 'main_hyp_GRUb_forward_0.br', 'main_hyp_GRUb_forward_0.W', 'main_statement_GRUb_forward_0.Wz', 'main_statement_GRUb_forward_0.bz', 'main_statement_GRUb_forward_0.Wr', 'main_statement_GRUb_forward_0.br', 'main_statement_GRUb_forward_0.W', 'main_forward_h_start0', 'prop_forward_h_start0', 'W', 'main_first_W', 'prop_first_W', 'main_first_b', 'prop_first_b', 'main_W_0', 'main_b_0', 'prop_W_0', 'prop_b_0']
Traceback (most recent call last):
File "run_script_ordered.py", line 72, in <module>
run_all_props_with_current_settings(passes, timeout)
File "run_script_ordered.py", line 35, in run_all_props_with_current_settings
searcher = proof_search.ProofSearcher(prop, language_model, directory=directory, timeout=timeout)
File "/home/dwheeler/holophrasm-whalen/proof_search.py", line 698, in __init__
global_interface = ProofInterface(lm, directory=directory)
File "/home/dwheeler/holophrasm-whalen/interface.py", line 59, in __init__
self.payout_var.load(directory+'/payout.weights')
File "/home/dwheeler/holophrasm-whalen/models.py", line 197, in load
raise Warning('Some variables not replaced.')
Warning: Some variables not replaced.
+ python3
added 0 proofs
Traceback (most recent call last):
File "<stdin>", line 3, in <module>
File "/home/dwheeler/holophrasm-whalen/write_proof.py", line 172, in write_all_known_proofs
proof_list = os.listdir(new_directory)
FileNotFoundError: [Errno 2] No such file or directory: 'searcher/proofs'
+ metamath
Metamath - Version 0.171 13-Dec-2018 Type HELP for help, EXIT to exit.
MM> Metamath has been reset to the starting state.
MM> Reading source file "modified_set.mm"... 19080258 bytes
19080258 bytes were read into the source buffer.
The source has 132334 statements; 2117 are $a and 27220 are $p.
No errors were found. However, proofs were not checked. Type VERIFY PROOF *
if you want to check them.
MM> 0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%
..................................................
All proofs in the database were verified in 4.34 s.
MM> EXIT
I ran commit 24642f175b2361ba7047227df1c91f23fa9175a0 (Python3) on Ubuntu.
The training works (yay!). However, after training, run_script_ordered.py fails as follows (suggestions welcome):