Proverbot Report

13 files processed

Commit: a13e20f0 Allow not using CUDA in predictor and encoder even when available

Run on 2024-01-26 19:27:24.794498

Proofs Completed: 26.18% (133/508)

Time taken: 2:41:47

scrape_file: data/compcert-scrape.txt
save_file: data/polyarg-weights.dat
context_filter: (goal-args+((tactic:induction+tactic:destruct)%numeric-args)+hyp-args+rel-lemma-args)%maxargs:1%default
truncate_semicolons: True
use_substitutions: True
normalize_numeric_args: True
num_epochs: 20
batch_size: 128
print_every: 5
learning_rate: 0.4
epoch_step: 3
hidden_size: 128
num_layers: 3
gamma: 0.8
optimizer: SGD
max_premises: 20
num_keywords: 60
tokenizer: no-fallback
num_relevance_samples: 1000
load_tokens: tokens.txt
num_tactic_keywords: 50
save_tactic_keywords: data/tactic-keywords.dat
load_tactic_keywords: data/tactic-keywords.dat
num_head_keywords: 100
save_head_keywords: data/head-keywords.dat
load_head_keywords: data/head-keywords.dat
max_length: 30
max_string_distance: 50
max_beam_width: 10
lemma_args: True
hyp_features: True
features: True
hyp_rnn: True
goal_rnn: True
training loss: 2.174219928275455
# epochs: 20
predictor: polyarg
report type: search
search width: 5
search depth: 6

Filename	Number of Proofs in File	% Proofs Completed	% Proofs Incomplete	% Proofs Failed	Details
./common/Globalenvs.v	112	17.86	75.89	6.25	Details
./lib/Parmov.v	89	35.96	61.80	2.25	Details
./x86/SelectOpproof.v	67	37.31	62.69	0.00	Details
./backend/Selectionproof.v	61	11.48	83.61	4.92	Details
./flocq/Core/Zaux.v	57	35.09	59.65	5.26	Details
./flocq/Calc/Round.v	40	2.50	97.50	0.00	Details
./backend/Locations.v	31	58.06	41.94	0.00	Details
./cfrontend/Cop.v	25	28.00	72.00	0.00	Details
./backend/RTL.v	10	10.00	90.00	0.00	Details
./MenhirLib/Validator_complete.v	7	14.29	85.71	0.00	Details
./flocq/Prop/Mult_error.v	7	0.00	100.00	0.00	Details
./lib/Wfsimpl.v	2	50.00	0.00	50.00	Details
Total	508	26.18	70.67	3.15

Trained as: ['/work/zhannakaufma_umass_edu/proverbot9001/./src/proverbot9001.py', 'train', 'polyarg', 'data/compcert-scrape.txt', 'data/polyarg-weights.dat', '--load-tokens=tokens.txt', '--context-filter=(goal-args+((tactic:induction+tactic:destruct)%numeric-args)+hyp-args+rel-lemma-args)%maxargs:1%default']
Reported as: ['/work/pi_brun_umass_edu/asanchezster/proverbot9001/src//search_report.py', 'dfs-report-noshellwrap', '-p', '.']
Weights hash: b'04852baafc0092f80f636a62f4e7b8c52693670d95415ad6e2fc07fd3403147a data/polyarg-weights-zhanna.dat\n'