I started writing this article with code in mind. It wasn’t until I put the pieces together that I realized the repercussions. The two projects I write about allow one to specify and create the robots to start the robot apocalypse. Warning: you might need Robotic Studio as well!
Microsoft Research has a tendency to release things that require several cups of coffee to wrap my head around, and the TLA Toolbox is no exception. With it, you write PlusCal algorithms (get it right, it’s an algorithm language, not a programming language) which get’s translated to a TLA+ specification. TLA+ Toolbox can then run a model checker.
To get full usage of the tool, you should read the book, Specifying Systems. It’s available for purchase or free for download. This isn’t your typical evening computer book read though… Specifying Systems is full of mathematical symbols… it reads more like a thesis than a popular computer science book.
Hour Clock Specification formula from Chapter 2 of Specifying Systems
Being the three-letter acronym for three-letter acronyms, I had to sift through a few entries to figure out what TLA actually meant. I eventually found that it stands for temporal logic of actions. It describes behaviors in concurrent systems, which makes sense considering time is an element of concern in concurrent systems.
Mentioning concurrent systems, another project had a release today… SIGMA: Large-Scale and Parallel Machine-Learning Tool Kit. Here’s the summary:
The goal of SIGMA is to provide a group of parallel machine-learning algorithms that can meet the requirements of research work and applications typically with large-scale data or features. The tool kit includes more than 10 algorithms and it makes them run on single multicore machine or on a HPC cluster with hundreds of machines and thousands of CPU cores running.
Parallel machine-learning algorithms? I’ve watched too many science fiction movies to know where this is going.
Installing SIGMA gives you a program called MLUI3 Studio. As promised, there are 10 algorithms including some training data and other inputs for the tests. Some of these algorithms are your typical classification and decision making algorithms. For those of us who fear a robot apocalypse, three stand out.
Neural Networks: with this the possibility exists for all of our machines to combine into one giant processing unit.
Boosting: One processing unit not scary enough? Each individual machine is a poor learning. What if each individual machine on the neural network could provide synergy in boosting other’s learning ability.
Expectation-maximization: The one thing us humans had left going for us was our ability to be random and go with our “gut” instinct. These instincts are likely the combination of many factors we have trouble computing the correct decision, but our subconscious is lending us a hand (like when you’re in the zone and you do instead of think). With expectation-maximization, we have lost that advantage. The bots can now find the maximum likelihood based on probabilistic models, even when those models depend on unobserved latent variables.
We’re doomed. Cyberdyne is alive… and to think, Microsoft Research has even had a project called Terminator since 2004. How could no one see this coming?
Subscribe