Holophrasm: a neural Automated Theorem Prover for higher-order logic
Objective-C++ Other
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
searcher
.gitignore
LICENSE.txt
README
beam_search.py
build_payout_data_set.py
constructor_list.py
data_utils5.py
gen_model_batch.py
gen_model_beam_search.py
gen_model_train.py
generate_payout_data_script.py
interface.py
last_step.py
learning_history.py
models.py
multitrainer.py
naive_tree_search_problem.py
nnlibrary.py
payout_model_5_train.py
pred_model.py
proof_search.py
run_script_ordered.py
save_language_model.py
script_gen.py
script_payout.py
script_pred.py
set.mm
statement_to_tree.py
tree.py
tree_parse.py
tree_parser.py
tree_search_problem.py
withpool.py
write_all_proofs.py
write_proof.py

README

Holophrasm: a purely neural automated theorem prover for Metamath
https://arxiv.org/abs/1608.02644

To use the program, start by downloading the release, which includes the binary files for the language model and the trained model weights.  Then, from the root directory, using python 2.7, run

python run_script_ordered.py
python write_all_proofs.py

run_script_ordered.py will attempt to search for proofs for all the Metamath propositions in the test set, starting with the (expected) easiest proofs first.  Reasonable parameters for running the script are:
timeout: 5
num_passes: 10000
search beam width: 20
hyp bonus: 0 
Proofs are saved to searcher/proofs as soon as they are found.  The proofs that I found during my search are in searcher/proofs_baseline.

write_all_proofs.py will generate a modified_set.mm module file, which consists of the proofs from set.mm, with the found proofs replaced.  This can then be fed into Metamath and verified using the commands

READ modified_set.mm
VERIFY PROOF *

There's a known bug involving outputting the proofs that assigns the same additional dummy variable to multiple set variables, breaking the disjointness condition.
I think this is purely a problem with the proof writing, but I'm not confident, so I've excluded these proofs from my count of working proofs anyway.

#############################################

If you want to train from scratch, you can do the following.  I recommend having at least 64GB of RAM.

Step 0: (OS X only) deal with Accelerate and forking bug
#########
export VECLIB_MAXIMUM_THREADS=1
#########

Step 1: train gen and pred
#########
python script_gen.py
python script_pred.py
#########

Step 2: set up the files for the nn interface
#########
mkdir searcher
cp weights/gen/train.parameters searcher/gen.parameters
cp weights/gen/train.weights searcher/gen.weights
cp weights/pred/train.parameters searcher/pred.parameters
cp weights/pred/train.weights searcher/pred.weights
#########
NOTE: this will fail because the searcher currently expects payout to
already exist.  Fix that.

Step 3: save a copy of the language model somewhere by running
#########
python save_language_model.py
#########

Step 4: construct the payout data set and train the payout network
#########
python generate_payout_data_script.py
python script_payout.py
cp weights/pred/train.parameters searcher/payout.parameters
cp weights/pred/train.weights searcher/payout.weights
#########

Step 5: run the proof search (hyp bonus should be set to 0.0 for consistency with the paper)
#########
python run_script_ordered.py
#########

Step 6: verify the proofs
######### PYTHON CODE
import write_proof
write_proof.reset()
write_proof.write_all_known_proofs()
#########

Step 7: copy the modified_set.mm into the metamath folder and use the following commands to verify the proofs
######### METAMATH COMMANDS
ERASE
READ modified_set.mm
VERIFY PROOF *
#########