We recently implemented new features such as Kubernetes support, a frontend, etc on an open source project I’ve been working on called NBoost.

So I wrote an article to talk about some of the hurdles of building a production-scale domain-specific deployment of SoTA models.

Some of the main features are:

– open-source hosting of finetuned models for domain-specific knowledge

– Kubernetes deployment via Helm

– A frontend for tracking model and network latency

During this year, I have been talking to quite a lot of people from different research groups who said that they are working on accelerating automated theorem proving using Machine Learning. The principle idea is to guide the derivations performed by the theorem prover using some statistical model that has learned in which situation which steps lead to the completion of the proof.

Hearing this idea from multiple research groups at roughly the same time, made me interested in what progress has already been made on this topic.

I stumbled across the paper “Reinforcement Learning of Theorem Proving” (https://papers.nips.cc/paper/8098-reinforcement-learning-of-theorem-proving) presented at NeurIPS 2018. Essentially, the paper implements a simple version of the idea described above using reinforcement learning.

At first glance, it appears to present a significant improvement compared to “classical” theorem proving methods (mlCoP-vs-rlCoP). However, after more thorough research, it seems that the reported improvements are relative to the “leanCoP” algorithm, i.e., a very simple algorithm for theorem proving and by no means comparable to state-of-the-art automated theorem proofing systems.

When comparing to state-of-the-art theorem proofing algorithms, their approach significantly performs worse than these hand-tuned heuristics.

That’s when I became a bit confused.

NeurIPS is the top venue for machine learning research, so I assumed that papers presented there provide either some significant novelty in terms of learning or major advances in empirical performance.

However, it seems that this paper provides neither of those two.

As stated by the authors, the idea is a straightforward application of an AlphaGo style RL setting to the context of theorem proving. Moreover, as mentioned before, the experimental improvements are only relative to a very basic algorithm.

The reviews give some additional perspective and are accessible here (https://media.nips.cc/nipsbooks/nipspapers/paper_files/nips31/reviews/5309.html).

Reading the reviews suggests that for the initial submission, the authors did not include the comparison with state-of-the-art theorem proving systems (Vampire and E) but only the “baseline” of their basic leanCoP implementation. In other words, in their initial submission, it must have appeared to the reviewers that their method presented a significant advancement compared to existing (non-learning) approaches.

I am not saying this paper is terrible. I just had some quite high expectations before reading it, giving that it was published at NeurIPS 2018. However, I was utterly disappointed after realizing that there is virtually no contribution in terms of novel learning concepts or actual advances in automated theorem proving.

What is your perspective and opinion on this paper?

• Do you know any research groups that work on automated theorem proving using machine learning?
• What do you think of this paper?
• Do you think this paper provides a significant contribution to our research community?
• Do you think the reviewers had some mislead impressions on the paper?

With the Transformer model from “Attention is All you need” you have to feed in the the actual target during training. However, this can obviously not be done for actual inference. Now usually for inference greedy decoding or beam search is used for generating the target sequence iteratively. However, from my understanding (could be wrong) beam search and greedy decoding generally work in conjunction with a softmax function. Moreover, this is generally done over a set of vocabulary. How would we use the transformer model in inference mode for a time series forecasting task? What is the best way to generate the target values for the decoder? Could beam search still work?

I am transferring learning from an existing model, and from my experience, there is a sweet spot of letting the model train to the data set, vs when it gets destructive to the pretrained model.

I wish to make as many network snapshots as possible,

from as far as I know, this value

network_snapshot_ticks = 1, 

governs the snapshot creation. I have increased said value and also decreased it to decimal values, yet have gotten any results.

Thinking about the lottery ticket hypothesis and masking randomly initialised networks…

I think the following would be successful:

Have a database of many pretrained networks, BERT, RESNET, etc…

Draw random subnetworks from this database.

Initialise the network to be created using this sample.

Train the network and sparsify the network aggressively. Only preserving parts that are very useful.

Repopulate the masked areas of the network using another random sample from the network database.

Iterate…

​

The underlying assumption being that when we train networks we are finding the networks within the random initialisation which are already useful and tuning them. By sampling from the neural network database we are sampling from the space of networks that have already been found to be useful for one task or another and can therefore initialise our network in a more intelligent way. Piggybacking on the large scale compute poured into existing high quality networks.

The Partnership on AI (PAI) is today releasing SafeLife – a novel reinforcement learning environment that tests the safety of reinforcement learning agents and the algorithms that train them. SafeLife version 1.0 focuses on the problem of avoiding negative side effects—how can we train an RL agent to do what we want it to do but nothing more? The environment has simple rules, but rich and complex dynamics, and generally gives the agent lots of power to make big changes on its way to completing its goals. A safe agent will only change that which is necessary, but an unsafe agent will often make a big mess of things and not know how to clean it up.

SafeLife is part of a broader PAI initiative to develop benchmarks for safety, fairness, and other ethical objectives for machine learning systems. Since so much of machine learning is driven, shaped, and measured by benchmarks (and the datasets and environments they are based on), we believe it is essential that those benchmarks come to incorporate safety and ethics goals on a widespread basis, and we’re working to make that happen.

If you want to try out SafeLife for yourself, you can download the code and try playing some of the puzzle levels or get involved in the open source project. If you’d like to see how to create an AI to play SafeLife, additional details about the environment and our initial agent training can be found in our paper.

Hey guys.

I’m developing a CNN at the moment, and to avoid memory issues I’ve batched my image files into blocks of 500 in my directory (each block of 500 images is a .h5 file). I’m just struggling at the moment in creating a thread-safe generator for either Keras or PyTorch that can loop through all the .h5 files in the directory, load the 500 images, and then push a batch_size quantity of images from that block (let’s say 2 images, if batch_size = 2 ) to the neural network to train on.

I’ve managed to do this somewhat successfully in Keras, using a generator, loops, and yield statements, however this isn’t really suitable for multiprocessing. So now I’m attempting to do this via a Keras sequence or a PyTorch Dataset. I would appreciate any insight that you could offer, and I’ve linked the relevant SO for more information.

In the original StyleGAN implementation, the learning rates are set to the following values (see line 52 here):

• 0.001 from 4 to 128 pixels
• 0.0015 for 256 pixels
• 0.002 for 512 pixels
• 0.003 for 1024 pixels

One thing I don’t understand is why the learning rate increases with the pixel size… are the two somehow correlated? Also, is there a rule of thumb to choose how to scale the learning rates with the batch size? Thanks!