Enable JavaScript to see more content
Recently hyped ML content linked in one simple page
Sources: reddit/r/{MachineLearning,datasets}, arxiv-sanity, twitter, kaggle/kernels, hackernews, awesome-datasets, sota changes
Made by: Deep Phrase HK Limited
|
1
|
|
|
[1909.11851v1] Mathematical Reasoning in Latent Space
Although it seems likely that these results can be significantly improved by better neural network architectures, hard negative mining and training on rewritten formulas, our methods showcases a simple and efficient general methodology for reasoning in the latent space
Abstract: We design and conduct a simple experiment to study whether neural networks
can perform several steps of approximate reasoning in a fixed dimensional
latent space. The set of rewrites (i.e. transformations) that can be
successfully performed on a statement represents essential semantic features of
the statement. We can compress this information by embedding the formula in a
vector space, such that the vector associated with a statement can be used to
predict whether a statement can be rewritten by other theorems. Predicting the
embedding of a formula generated by some rewrite rule is naturally viewed as
approximate reasoning in the latent space. In order to measure the
effectiveness of this reasoning, we perform approximate deduction sequences in
the latent space and use the resulting embedding to inform the semantic
features of the corresponding formal statement (which is obtained by performing
the corresponding rewrite sequence using real formulas). Our experiments show
that graph neural networks can make non-trivial predictions about the
rewrite-success of statements, even when they propagate predicted latent
representations for several steps. Since our corpus of mathematical formulas
includes a wide variety of mathematical disciplines, this experiment is a
strong indicator for the feasibility of deduction in latent space in general.
‹ Figure 1: Depiction of network architecture (Base Model Architecture and Training Methodology) Figure 4: Left: Comparison of Area under ROC curves for each embedding method. Right: Comparison of ROC curves for each embedding method after the fourth rewrite. (Evaluation of Rewrite Prediction Model) Figure 5: Left: Histogram of l2 distances between each embedding method and the true embedding for rewrite steps 1 and 4. Right: Plot showing the mean l2 distances across rewrite steps. Pred (One step): expected error kγ(R(T, P)) − α(e(γ0 (T), π0 (P)))k2 between the true embedding of the rewritten statement R(T, P) and that of the prediction network ω ◦ α one step ahead in Dk. Pred (Multi step): expected error for γ(R(...R(T, P1), ..., Pk)) in Dk after k approximate rewrites. Random baseline: expected l2 distance kγ(T1) − γ(T2)k2 between the “true” embeddings of two randomly chosen theorems from Dk. (Evaluation of Rewrite Prediction Model) Figure 6: Visualization of the embedding spaces produced by embedding prediction e0 in the latent space after 1, 2, 3 and 4 rewrite steps. The points are colored by their l2 -distance to the true embedding γ(T). Figure 7: Visualization of the embedding space γ(T) evolving over four rewrite steps. Theorems are colored by the area of mathematics they originate from, sourced from the theorem database. The brightness of the embeddings corresponds to the rewrite step in which it was generated, with more recent embeddings being darker. (Evaluation of Rewrite Prediction Model)›
|
|
Related: TFIDF
[1905.10006] Graph Representations for Higher-Order Logic and Theorem Proving[1905.10006v1] Graph Representations for Higher-Order Logic and Theorem Proving[1709.09994] Premise Selection for Theorem Proving by Deep Graph Embedding[1904.03241] HOList: An Environment for Machine Learning of Higher-Order Theorem Proving[1606.04442] DeepMath - Deep Sequence Models for Premise Selection[1703.00426] HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving[1905.10501] Learning to Reason in Large Theories without Imitation
|
|
Related: TFIDF
[1905.10006] Graph Representations for Higher-Order Logic and Theorem Proving[1905.10006v1] Graph Representations for Higher-Order Logic and Theorem Proving[1709.09994] Premise Selection for Theorem Proving by Deep Graph Embedding[1904.03241] HOList: An Environment for Machine Learning of Higher-Order Theorem Proving[1606.04442] DeepMath - Deep Sequence Models for Premise Selection[1703.00426] HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving[1905.10501] Learning to Reason in Large Theories without Imitation
