tigeryi1998 / holophrasm Goto Github PK
View Code? Open in Web Editor NEWThis project forked from dwhalen/holophrasm
Holophrasm: a neural Automated Theorem Prover for higher-order logic
License: MIT License
This project forked from dwhalen/holophrasm
Holophrasm: a neural Automated Theorem Prover for higher-order logic
License: MIT License
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 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 `dtrucor` ignoring the disjointness conditions, which has been fixed with a temporary hack. In case the bug applies more generally, you should not assume any proof is valid until metamath verifies modified_set.mm. ############################################# 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. Neither of the training scripts exit automatically, so you will need to keyboard interrupt them at some point, preferably after the training rate decays to a sufficiently low value. All of these scripts may be run in parallel. ######### python script_gen.py # Train the generative network python script_pred.py # Train the prediction network python save_language_model.py # Save a copy of the language model somewhere ######### 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 ######### Step 3: construct the payout data set and train the payout network The first script takes days, but is highly parallelizable. Chunks may be run on different machines, and multiprocessing can be enabled by changing the "withpool.Pool(None)" to "withpool.Pool(n)", where n is the desired number of processes. WARNING: multiprocessing support may crash Windows machines. WARNING: if generate_payout_data_script.py does not run correctly, it may leave files payout_data_* of size 0. These need to be deleted before rerunning the script. ######### 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) The search will be much faster if you set "multi=True" in the searcher.run call, but this may break on Windows. ######### 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 * #########
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.