tensorflow / deepmath

Experiments towards neural network theorem proving

Documentation

TensorFlow is an end-to-end open source platform for machine learning. It has a comprehensive, flexible ecosystem of tools, libraries, and community resources that lets researchers push the state-of-the-art in ML and developers easily build and deploy ML-powered applications.

TensorFlow was originally developed by researchers and engineers working within the Machine Intelligence team at Google Brain to conduct research in machine learning and neural networks. However, the framework is versatile enough to be used in other areas as well.

TensorFlow provides stable Python and C++ APIs, as well as a non-guaranteed backward compatible API for other languages.

Keep up-to-date with release announcements and security updates by subscribing to [email protected]. See all the mailing lists.

Install

See the TensorFlow install guide for the pip package, to enable GPU support, use a Docker container, and build from source.

To install the current release, which includes support for CUDA-enabled GPU cards (Ubuntu and Windows):

$ pip install tensorflow

Other devices (DirectX and MacOS-metal) are supported using Device plugins.

A smaller CPU-only package is also available:

$ pip install tensorflow-cpu

To update TensorFlow to the latest version, add --upgrade flag to the above commands.

Nightly binaries are available for testing using the tf-nightly and tf-nightly-cpu packages on PyPi.

Try your first TensorFlow program

$ python

>>> import tensorflow as tf
>>> tf.add(1, 2).numpy()
3
>>> hello = tf.constant('Hello, TensorFlow!')
>>> hello.numpy()
b'Hello, TensorFlow!'

For more examples, see the TensorFlow tutorials.

Contribution guidelines

If you want to contribute to TensorFlow, be sure to review the contribution guidelines. This project adheres to TensorFlow's code of conduct. By participating, you are expected to uphold this code.

We use GitHub issues for tracking requests and bugs, please see TensorFlow Forum for general questions and discussion, and please direct specific questions to Stack Overflow.

The TensorFlow project strives to abide by generally accepted best practices in open-source software development.

Patching guidelines

Follow these steps to patch a specific version of TensorFlow, for example, to apply fixes to bugs or security vulnerabilities:

• Clone the TensorFlow repo and switch to the corresponding branch for your desired TensorFlow version, for example, branch r2.8 for version 2.8.
• Apply (that is, cherry-pick) the desired changes and resolve any code conflicts.
• Run TensorFlow tests and ensure they pass.
• Build the TensorFlow pip package from source.

Continuous build status

You can find more community-supported platforms and configurations in the TensorFlow SIG Build community builds table.

Official Builds

Build Type	Status	Artifacts
Linux CPU		PyPI
Linux GPU		PyPI
Linux XLA		TBA
macOS		PyPI
Windows CPU		PyPI
Windows GPU		PyPI
Android		Download
Raspberry Pi 0 and 1		Py3
Raspberry Pi 2 and 3		Py3
Libtensorflow MacOS CPU	Status Temporarily Unavailable	Nightly Binary Official GCS
Libtensorflow Linux CPU	Status Temporarily Unavailable	Nightly Binary Official GCS
Libtensorflow Linux GPU	Status Temporarily Unavailable	Nightly Binary Official GCS
Libtensorflow Windows CPU	Status Temporarily Unavailable	Nightly Binary Official GCS
Libtensorflow Windows GPU	Status Temporarily Unavailable	Nightly Binary Official GCS

Resources

• TensorFlow.org
• TensorFlow Tutorials
• TensorFlow Official Models
• TensorFlow Examples
• TensorFlow Codelabs
• TensorFlow Blog
• Learn ML with TensorFlow
• TensorFlow Twitter
• TensorFlow YouTube
• TensorFlow model optimization roadmap
• TensorFlow White Papers
• TensorBoard Visualization Toolkit
• TensorFlow Code Search

Learn more about the TensorFlow community and how to contribute.

Courses

• Coursera
• Udacity
• Edx

License

Apache License 2.0

deepmath's Issues

name resolution failure when running prover_options.textpb

ed@ed-Aspire-E5-575:/tmp/deepmath/deephol$ sudo docker run -it --network=holist_net -v /tmp/deepmath:/data gcr.io/deepmath/deephol --prover_options=/data/deephol/example/prover_options.textpb --output=/data/prooflog.textpb --proof_assistant_server_address=holist:2000
W0521 16:32:38.697212 139814335006464 prover_flags.py:122] builtin_library is deprecated. Do not provide.
I0521 16:32:38.697877 139814335006464 prover_flags.py:137] Using prover_options:
path_theorem_database: "/data/deephol/theorem_database_v1.0.textpb"
path_model_prefix: "/data/deephol/checkpoints/loop_tac_depend_5210000/model.ckpt-5210000"
path_tactics: "/data/deephol/example/hollight_tactics.textpb"
path_tactics_replace: "/data/deephol/example/hollight_tactics_replacements_nogen.textpb"
theorem_embeddings: "/data/loop_tac_depend_5210000__model.ckpt-5210000__v1.0__embedding.npy"
prover: "bfs"
bfs_options {
max_top_suggestions: 20
max_successful_branches: 5
max_explored_nodes: 120
}
splits_to_prove: VALIDATION
timeout_seconds: 120.0
model_architecture: PARAMETERS_CONDITIONED_ON_TAC
library_tags: "clifford.ml"

I0521 16:32:38.698731 139814335006464 prover_flags.py:155] Splits to prove: VALIDATION
I0521 16:32:38.698900 139814335006464 prover_flags.py:170] Library tags to prove: clifford.ml
I0521 16:32:38.709361 139814335006464 io_util.py:85] Successfully read tactics from "/data/deephol/example/hollight_tactics.textpb"
I0521 16:32:38.709577 139814335006464 io_util.py:118] Found 41 tactics.
I0521 16:32:38.711959 139814335006464 io_util.py:85] Successfully read replacements from "/data/deephol/example/hollight_tactics_replacements_nogen.textpb"
I0521 16:32:38.712185 139814335006464 io_util.py:123] Found 3 tactic replacements.
I0521 16:33:40.346311 139814335006464 io_util.py:134] Successfully read theorem database from /data/deephol/theorem_database_v1.0.textpb (31680 theorems).
I0521 16:33:40.346585 139814335006464 prover_util.py:490] Generating task list for theorem database.
I0521 16:33:40.412294 139814335006464 prover_flags.py:189] Number of prover tasks: 16
I0521 16:34:41.991417 139814335006464 io_util.py:134] Successfully read theorem database from /data/deephol/theorem_database_v1.0.textpb (31680 theorems).
I0521 16:34:42.002013 139814335006464 io_util.py:85] Successfully read tactics from "/data/deephol/example/hollight_tactics.textpb"
I0521 16:34:42.002218 139814335006464 io_util.py:118] Found 41 tactics.
I0521 16:34:42.003573 139814335006464 io_util.py:85] Successfully read replacements from "/data/deephol/example/hollight_tactics_replacements_nogen.textpb"
I0521 16:34:42.003768 139814335006464 io_util.py:123] Found 3 tactic replacements.
2019-05-21 16:34:42.014507: I external/org_tensorflow/tensorflow/core/platform/cpu_feature_guard.cc:142] Your CPU supports instructions that this TensorFlow binary was not compiled to use: SSE4.1 SSE4.2 AVX AVX2 FMA
I0521 16:34:42.015912 139814335006464 holparam_predictor.py:78] Importing from metagraph in /data/deephol/checkpoints/loop_tac_depend_5210000/export/best_exporter/1549098420/saved_model.pb.
W0521 16:34:45.323910 139814335006464 deprecation.py:323] From /home/main.runfiles/org_tensorflow/tensorflow/python/training/saver.py:1277: checkpoint_exists (from tensorflow.python.training.checkpoint_management) is deprecated and will be removed in a future version.
Instructions for updating:
Use standard file APIs to check for files with this prefix.
I0521 16:34:45.324696 139814335006464 saver.py:1281] Restoring parameters from /data/deephol/checkpoints/loop_tac_depend_5210000/model.ckpt-5210000
I0521 16:34:45.540045 139814335006464 embedding_store.py:86] Reading embeddings from "/data/loop_tac_depend_5210000__model.ckpt-5210000__v1.0__embedding.npy"
I0521 16:34:46.395910 139814335006464 prover.py:357] Setting up and registering theorems with proof assistant...
Traceback (most recent call last):
File "/home/main.runfiles/deepmath/deepmath/deephol/main.py", line 28, in
tf.app.run(main)
File "/home/main.runfiles/org_tensorflow/tensorflow/python/platform/app.py", line 40, in run
_run(main=main, argv=argv, flags_parser=_parse_flags_tolerate_undef)
File "/home/main.runfiles/absl_py/absl/app.py", line 300, in run
_run_main(main, args)
File "/home/main.runfiles/absl_py/absl/app.py", line 251, in _run_main
sys.exit(main(argv))
File "/home/main.runfiles/deepmath/deepmath/deephol/main.py", line 24, in main
prover_runner.run_pipeline(*prover_flags.process_prover_flags())
File "/home/main.runfiles/deepmath/deepmath/deephol/prover_runner.py", line 31, in run_pipeline
this_prover = prover.create_prover(prover_options)
File "/home/main.runfiles/deepmath/deepmath/deephol/prover.py", line 348, in create_prover
hol_wrapper = setup_prover(theorem_database)
File "/home/main.runfiles/deepmath/deepmath/deephol/prover.py", line 361, in setup_prover
proof_assistant_pb2.RegisterTheoremRequest(theorem=thm))
File "/home/main.runfiles/deepmath/deepmath/deephol/public/proof_assistant.py", line 42, in RegisterTheorem
return self.stub.RegisterTheorem(request)
File "/usr/local/lib/python3.5/dist-packages/grpc/_channel.py", line 549, in call
return _end_unary_response_blocking(state, call, False, None)
File "/usr/local/lib/python3.5/dist-packages/grpc/_channel.py", line 466, in _end_unary_response_blocking
raise _Rendezvous(state, None, None, deadline)
grpc._channel._Rendezvous: <_Rendezvous of RPC that terminated with:
status = StatusCode.UNAVAILABLE
details = "Name resolution failure"
debug_error_string = "{"created":"@1558456486.421764398","description":"Failed to create subchannel","file":"src/core/ext/filters/client_channel/client_channel.cc","file_line":2267,"referenced_errors":[{"created":"@1558456486.421761906","description":"Name resolution failure","file":"src/core/ext/filters/client_channel/request_routing.cc","file_line":166,"grpc_status":14}]}"

Training with GPUs

Hi, how can I use GPUs to train the model ? I noticed that TF_NEED_CUDA=0 in TF's configure, can I simply replace it with TF_NEED_CUDA=1 ? Why not use the official TF ?

No Dockerfile for deephol container. Dockerfile for deepmath doesn't build

We're trying to run DeepHOL Neural Prover, mentioned here:
https://sites.google.com/view/holist/home

We need to modify some of the code in the container to run it. The github link for this container points to:
https://www.google.com/url?q=https%3A%2F%2Fgithub.com%2Ftensorflow%2Fdeepmath%2Ftree%2Fmaster%2Fdeepmath%2Fdeephol&sa=D&sntz=1&usg=AFQjCNFf5v14MnxtBWeVcNgkqqPrfkwntQ

There's no dockerfile in that directory, but it appears that the container is using the Dockerfile in the deepmath directory from the interface.

However, this Dockerfile won't build.
The first error I get is a syntax error in pip.:
Traceback (most recent call last): File "<string>", line 1, in <module> File "/tmp/pip-build-fcwr468q/h5py/setup.py", line 38 f"numpy >={np_min}; python_version{py_condition}" ^ SyntaxError: invalid syntax

When I add:
pip3 install --update pip

to the Dockerfile it makes it further, but fails with:

ERROR: /root/.cache/bazel/_bazel_root/5b685c7ece7fdf4d574f01e62a56a6b7/external/org_tensorflow/tensorflow/core/kernels/BUILD:7127:1: no such package '@icu//': java.io.IOException: Error downloading [https://mirror.bazel.build/github.com/unicode-org/icu/archive/release-62-1.tar.gz, https://github.com/unicode-org/icu/archive/release-62-1.tar.gz] to /root/.cache/bazel/_bazel_root/5b685c7ece7fdf4d574f01e62a56a6b7/external/icu/release-62-1.tar.gz: Checksum was 86b85fbf1b251d7a658de86ce5a0c8f34151027cc60b01e1b76f167379acf181 but wanted e15ffd84606323cbad5515bf9ecdf8061cc3bf80fb883b9e6aa162e485aa9761 and referenced by '@org_tensorflow//tensorflow/core/kernels:unicode_script_op'

We've tried changing tensorflow and bazel versions, and some get further, but no combination we've found works.

About the "missing" sub-package in deephol/deephol_loop

Hi, I am currently working on the RL training loop. Is it possible that anyone can share with me the basic idea of what does deepmath.deephol.deephol_loop.missing.runner do in the training loop? Also, is the RL an online training or offline training? @kbansal

Missing Dataset

Hi,

I would like to download deep-hol proofs and training data by following the instruction from https://sites.google.com/view/holist/home, the prompt suggests that HTTP request sent, awaiting response... 404 Not Found. It seems like the specified bucket does not exist.

Is it possible to obtain the deep-hol data by other instructions or could you please help me figure it out? Thanks in advance!

S-expression generation

I can't find anything in the HOList paper about how you generated the S-expressions for the theorem database. I'm assuming they are just lightly processed terms from HOL-Light's internal representation? I would like to make my own mini database. Is there anywhere I can find more information on the conversion or a specification of the format?

Bazel Build Failed

In running the command: "bazel build ..."
I am seeing following error. Note sure what is causing it.
...........
ERROR: /private/var/tmp/_bazel_USER/3498234242c6f7373b6edebcb02e157b/external/io_bazel_rules_closure/closure/private/defs.bzl:27:16: The set constructor for depsets is deprecated and will be removed. Please use the depset constructor instead. You can temporarily enable the deprecated set constructor by passing the flag --incompatible_disallow_set_constructor=false.
ERROR: error loading package '': Extension file 'closure/private/defs.bzl' has errors.
ERROR: error loading package '': Extension file 'closure/private/defs.bzl' has errors.

Example?

Perhaps it would be helpful to provide an example usage? I have compiled the ZZ binary but I am unable to actually run anything besides the help screen.

Prove using multiple CPUs?

Is it possible to run the prover with multiple CPUs? I have 50 CPUs but only one is being used.

Unit tests for zz/HolLight

Theorem provers should have unit tests.

TensorFlow Fold crash

Background: deepmath has tensorflow and fold submodules. model_utils_test exercises fold features, and crashes on Mac with

Python(5066,0x7fffcaea83c0) malloc: *** error for object 0x10b2ba238: pointer being freed was not allocated

The stacktrace looks like

(lldb) bt
* thread #4: tid = 0xe86c7, 0x00007fffc2189dd6 libsystem_kernel.dylib`__pthread_kill + 10, queue = 'com.apple.main-thread', stop reason = signal SIGABRT
  * frame #0: 0x00007fffc2189dd6 libsystem_kernel.dylib`__pthread_kill + 10
    frame #1: 0x00007fffc2275787 libsystem_pthread.dylib`pthread_kill + 90
    frame #2: 0x00007fffc20ef420 libsystem_c.dylib`abort + 129
    frame #3: 0x00007fffc21df03f libsystem_malloc.dylib`free + 530
    frame #4: 0x000000010b1715cb _deserializing_weaver_op.so`tensorflow::OpDef::SharedDtor() + 107
    frame #5: 0x000000010b17141c _deserializing_weaver_op.so`tensorflow::OpDef::~OpDef() + 28
    frame #6: 0x000000010b10276d _deserializing_weaver_op.so`_GLOBAL__sub_I_deserializing_weaver_op.cc + 317
...

It looks like some TensorFlow symbols are duplicated in the _pywrapweaver.so file, but not all of them:

% nm ./org_fold/tensorflow_fold/loom/_pywrapweaver.so
...
0000000000070e50 T __ZN10tensorflow5OpDef10SharedDtorEv
...
             U __ZN10tensorflow11TensorShape9InsertDimEix

It's possible that proto symbols are being duplicated and non-proto symbols are not.

How is deepmath/hol/proofs-nat generated?

Hi there,

I noticed that there is a file deepmath/hol/proofs-nat that contains the trace of the proof. The trace.cc said that this file is generated "by HOL Light proofrecording". Can you elaborate on how to generate such a trace file using hol-light? I didn't find any instruction to do that.

Thanks very much!

Example prover_options file to run DeepHOL via docker?

I arrived at this repo via the HOList website. As someone with both knowledge of machine learning and HOL Light, I was hoping to play around with your new DeepHOL system. However, it looks like I need a prover options file to run it:

--prover_options=/tmp/example/prover_options.txt

Can you provide an example file either in this GitHub repo or via the HOList website? Thanks!

(Also, I noticed you recently gave two talks on this project at the 2019 AITP conference. It looks like many of the presenters shared their slides on the conference website. If you are willing to do the same, it would help a lot.)

can deephol solve inductive construction problem?

Hello, I am a new hand in the field of mathematical automated reasoning and it's my pleasure to read your paper HOList. I wonder whether deephol can solve the inductive problems and if the theorem database include PA? or Deephol can only solve the deductive problems like other SMT?

Question about the holstep dataset

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, how did your team generate statements from dependencies listed.
I read through the paper but found that the problem is barely described. Thus, I hope you can give some advice on this issue.
Thanks a lot! :）

Documentation for zz/HolLight

How to use pan, how to use the viewer, etc. Should be in markdown format in a g3doc directory (see e.g., https://github.com/tensorflow/tensorflow/tree/master/tensorflow/g3doc).

./configure for tensorflow

Hello, if Tensorflow is already installed on the system do we need to go through the ./configure commad as mentioned in the repo?