Calling all MIRI supporters for unique giving opportunity!

 |   |  News

Update: We are liveblogging the fundraiser here.

Read our strategy below, then give here!

SVGives logo lrg


As previously announced, MIRI is participating in a massive 24-hour fundraiser on May 6th, called SV Gives. This is a unique opportunity for all MIRI supporters to increase the impact of their donations. To be successful we’ll need to pre-commit to a strategy and see it through. If you plan to give at least $10 to MIRI sometime this year, during this event would be the best time to do it!

The plan

We need all hands on deck to help us win the following prize as many times as possible:

$2,000 prize for the nonprofit that has the most individual donors in an hour, every hour for 24 hours.

To paraphrase, every hour, there is a $2,000 prize for the organization that has the most individual donors during that hour. That’s a total of $48,000 in prizes, from sources that wouldn’t normally give to MIRI. 

The minimum donation is $10, and an individual donor can give as many times as they want. Therefore we ask our supporters to:

  1. give $10 an hour, during every hour of the fundraiser that they are awake (I’ll be up and donating for all 24 hours!);
  2. for those whose giving budgets won’t cover all those hours, see below for list of which hours you should privilege; and
  3. publicize this effort as widely as possible.

International donors, we especially need your help!

MIRI has a strong community of international supporters, and this gives us a distinct advantage! While North America sleeps, you’ll be awake, ready to target all of the overnight $2,000 hourly prizes.

Hours to target in order of importance

To increase our chances of winning these prizes we want to preferentially target the hours that will see the least donation traffic from donors of other participating organizations. Below are the top 12 hours we’d like to target in order of importance. Remember that all times are in Pacific Time. (Click on an hour to see what time it is in your timezone.)

For the 5 pm hour there is an additional prize I think we can win:

$1,000 golden ticket added to the first 50 organizations receiving gifts in the 5 pm hour.

So if you are giving in the 5 pm hour try and give right at the beginning of the hour.

Bottom line, for every hour you are awake, give $10 an hour.

 Give preferentially to the hours above, if unable to give during all waking hours.

We also have plans to target the $300,000 in matching funds up for grabs during the event. If you would like to contribute $500 or more to this effort, shoot me an email at

For those who want to follow along and contribute to the last minute planning, as well as receive updates and giving reminders during the event, sign up below.

Kasper Stoy on self-reconfigurable robots

 |   |  Conversations

Kasper Støy portrait Kasper Stoy is a robotics and embodied artificial intelligence researcher holding an associate professor position at the Software and Systems Section of the IT University of Copenhagen. He is interested in the construction and design of complete robot systems, but being a computer scientist he has made most of his personal contributions in distributed control of multi-robot systems and modular robotics. He has published more than sixty papers in international conference proceedings or journals and is the author of the book “Self-Reconfigurable Robots: An Introduction” published by MIT Press. He also co-founded Universal Robots, a company focuses on user-friendly robot arms for industry. He is an active player in the international robot research community and reviews for all major journals and conferences in robotics. He has stayed for extended periods at University of Southern California, Harvard University, University of Tarapacá (Chile), and Seam Reap (Cambodia). He holds a M.Sc. degree in computer science and physics from the University of Aarhus, Denmark (1999) and a Ph.D. degree in computer system engineering from the University of Southern Denmark (2003) where he also worked as assistant professor (2003-2006) and associate professor (2006-2013). He is married and has two kids.

Luke Muehlhauser: In Larsen et al. (2013), you and your co-authors write:

Using a bottom-up, model-free approach when building robots [is] often seen as a less scientific way, compared to a top-down model-based approach, because the results are not easily generalizable to other systems… In this paper we will show how the use of well-known experimental methods from bio-mechanics are used to measure and locate weaknesses in our bottom-up, model-free implementation of a quadruped walker and come up with a better solution.

From looking at the paper I could see how your experimental method allowed you to find a better solution for your walker robot, but I couldn’t understand how you addressed the challenge of generalizing the solution to other systems despite the bottom-up, model-free approach. Could you explain that part?

Kasper Stoy: The problem is that researchers who are doing cutting edge robotics want to explore how materials and their interaction can aid the movement of the robot. For instance, researchers have been working on passive-dynamic walkers for a long time now that exploit the mechanical system to achieve walking without using sensors or actuators. The energy comes from walking downhill and the control is open-looped – the mechanical system itself is self-stabilising. For these systems our current engineering approach is ok, but not great. We can just about model these kinds of walkers so we can get a good guess of the initial parameters to get the system walking, but there is still an extended phase of tinkering before the system actually walks. It is in this tinkering phase that our precise motion capture as used in biomechanics comes into play. Given measured paths of all parts of the robot we can analyse the data and come up with reasonable hypotheses about how to improve the robot. Hence, the tinkering becomes much more systematic even though the underlying physical processes are too complex to be modelled. It may not be apparent, but just modelling the impact of a foot with the ground which takes all types of frictions into account, the deformation of the foot, the spring effect, and so on is largely intractable. Hence, the underlying assumption of our work is that all models of locomotion are fundamentally wrong. They may give a high-level picture of what is going on, but fundamentally they cannot be used to predict what will happen just two steps later. However, if we turn this around and we have gotten our robot to walk and we record the data of how it walks. Although difficult, we can build a model that match this data which is based on the ground truth and where there is no modelling bias on the part of the researcher. We now have a better informed model that can be used to build the next generation of robots. Hence, the model is a generalisation of our specific implementation which you can copy, but you can also replace elements of which you have better implementations. In locomotion research like many other fields the models and physical systems are drifting apart because it is researchers with different skill and interests who work on them. In our work, we are clearly working on physical systems and just provide a hint to how our experimental results can be generalised in a way that is meaningful to modelling oriented researchers. We hope.
Read more »

MIRI’s May 2014 Newsletter

 |   |  Newsletters

Machine Intelligence Research Institute

On May 6th, there is $250,000+ in matching funds and prizes available from sources that normally wouldn’t contribute to MIRI at all. Details here.

Research Updates

News Updates

Other Updates

As always, please don’t hesitate to let us know if you have any questions or comments.

Luke Muehlhauser
Executive Director


New Paper: “The errors, insights, and lessons of famous AI predictions”

 |   |  News

AI predictions paperDuring his time as a MIRI researcher, Kaj Sotala contributed to a paper now published in the Journal of Experimental & Theoretical Artificial Intelligence: “The errors, insights and lessons of famous AI predictions – and what they mean for the future.”


Predicting the development of artificial intelligence (AI) is a difficult project – but a vital one, according to some analysts. AI predictions are already abound: but are they reliable? This paper starts by proposing a decomposition schema for classifying them. Then it constructs a variety of theoretical tools for analysing, judging and improving them. These tools are demonstrated by careful analysis of five famous AI predictions: the initial Dartmouth conference, Dreyfus’s criticism of AI, Searle’s Chinese room paper, Kurzweil’s predictions in the Age of Spiritual Machines, and Omohundro’s ‘AI drives’ paper. These case studies illustrate several important principles, such as the general overconfidence of experts, the superiority of models over expert judgement and the need for greater uncertainty in all types of predictions. The general reliability of expert judgement in AI timeline predictions is shown to be poor, a result that fits in with previous studies of expert competence.

Suresh Jagannathan on higher-order program verification

 |   |  Conversations

Suresh Jagannathan portrait Dr. Suresh Jagannathan joined DARPA in September 2013. His research interests include programming languages, compilers, program verification, and concurrent and distributed systems.

Prior to joining DARPA, Dr. Jagannathan was a professor of computer science at Purdue University. He has also served as visiting faculty at Cambridge University, where he spent a sabbatical year in 2010; and as a senior research scientist at the NEC Research Institute in Princeton, N.J.

Dr. Jagannathan has published more than 125 peer-reviewed conference and journal publications and has co-authored one textbook. He holds three patents. He serves on numerous program and steering committees, and is on the editorial boards of several journals.

Dr. Jagannathan holds Doctor of Philosophy and Master of Science degrees in Electrical Engineering and Computer Science from the Massachusetts Institute of Technology. He earned a Bachelor of Science degree in Computer Science from the State University of New York, Stony Brook.

Luke Muehlhauser: From your perspective, what are some of the most interesting or important developments in higher-order verification in the past decade?

Suresh Jagannathan: I would classify the developments of the past decade into four broad categories:

  1. The development of higher-order recursion schemes (or higher-order model checking). This approach is based on defining a language semantics in terms of a (recursive) tree grammar. We can now ask whether the tree generated by the grammar satisfies a particular safety property. Because recursion schemes are very general and expressive structures, they can be viewed as natural extensions of model checkers based on pushdown automata or finite-state systems. In the past decade, there have been substantial advances that have made higher-order model checking a practical endeavor, accompanied by realistic implementations.
  2. Liquid Types combine facets of classic type inference techniques found in functional language with predicate abstraction techniques used in model checkers to automatically infer dependent type refinements with sufficient precision to prove useful safety properties about higher-order functional programs. Implementations of this approach found in OCaml, SML, and Haskell have demonstrated that it is indeed to possible to verify non-trivial program properties without significant type annotation burden.
  3. There have been substantial advances in the development of new languages built around rich dependent type systems that enable the expression and static verification of rich safety and security specifications and properties of higher-order programs. These include the languages that support mechanized proof assistants like Coq, Agda, or Epigram, languages like F* geared towards secure distributed programming, libraries like Ynot that encapsulate imperative (stateful) features and Hoare-logic pre/post-conditions within a higher-order dependent type framework, and features such as GADTs and type classes found in languages like GHC.
  4. Polyvariant control-flow analyses like CFA2 or higher-order contracts are two techniques that facilitate verification and analysis of dynamic higher-order languages. CFA2 adopts pushdown models used in program analyses for first-order languages to a higher-order setting, enabling precise matching of call/return sequences. Higher-order contracts allow runtime verification and blame assignment of higher-order programs and are fully incorporated into Racket, a multi-paradigm dialect of Lisp/Scheme.

Read more »

Ruediger Schack on quantum Bayesianism

 |   |  Conversations

Ruediger Schack portrait Ruediger Schack is a Professor at the Department of Mathematics at Royal Holloway, University of London. He obtained his PhD in Theoretical Physics at the University of Munich in 1991 and held postdoctoral positions at the Max Planck Institute for Quantum Optics, the University of Southern California, the University of New Mexico, and Queen Mary and Westfield College before joining Royal Holloway in 1995. His research interests are quantum information theory, quantum cryptography and quantum Bayesianism.

Luke Muehlhauser: In Fuchs et al. (2013), you and your co-authors provide an introduction to quantum Bayesianism aka “QBism,” which you more or less co-invented with Carlton Caves and Christopher Fuchs. But before I ask about QBism, let me ask one of the questions asked of the interviewees in Elegance and Enigma: The Quantum Interviews (including Fuchs): “What first stimulated your interest in the foundations of quantum mechanics?”

Ruediger Schack: I can trace the beginning of my interest in quantum foundations to reading one paper: “Where do we stand on maximum entropy?” by Ed Jaynes, and one book: Du Microscopique au Macroscopique by Roger Balian. Jaynes’s paper introduced me to Bayesian probability theory, and Balian’s book taught me that one can think of quantum states as representing Bayesian probabilities.

Read more »

David J. Atkinson on autonomous systems

 |   |  Conversations

David J. Atkinson portrait David J. Atkinson, Ph.D, is a Senior Research Scientist at the Florida Institute for Human and Machine Cognition (IHMC). His current area of research envisions future applications of intelligent, autonomous agents, perhaps embodied as robots, who work alongside humans as partners in teamwork or provide services. Dr. Atkinson’s major focus is on fostering appropriate reliance and interdependency between humans and agents, and the role of social interaction in building a foundation for mutual trust between humans and intelligent, autonomous agents. He is also interested in cognitive robotics, meta-reasoning, self-awareness, and affective computing. Previously, he held several positions at California Institute of Technology, JPL (a NASA Center), where his work spanned basic research in artificial intelligence, autonomous systems and robotics with applications to robotic spacecraft, control center automation, and science data analysis. Recently, Dr. Atkinson delivered an invited plenary lecture on the topic of “Trust Between Humans and Intelligent Autonomous Agents” at the 2013 IEEE/WIC/ACM International Conference on Web Intelligence and Intelligent Agent Technology (WI-IAT 2013). Dr. Atkinson holds a Bachelor’s degree in Psychology from University of Michigan, dual Master of Science and Master of Philosophy degrees in Computer Science (Artificial Intelligence) from Yale University, and the Doctor of Technology degree (d.Tekn) in Computer Systems Engineering from Chalmers University of Technology in Sweden.

Luke Muehlhauser: One of your projects at IHMC is “The Role of Benevolence in Trust of Autonomous Systems“:

The exponential combinatorial complexity of the near-infinite number of states possible in autonomous systems voids the applicability of traditional verification and validation techniques for complex systems. New and robust methods for assessing the trustworthiness of autonomous systems are urgently required if we are to have justifiable confidence in such applications both pre-deployment and during operations…  The major goal of the proposed research is to operationalize the concept of benevolence as it applies to the trustworthiness of an autonomous system…

Some common approaches for ensuring desirable behavior from AI systems include testing, formal methods, hybrid control, and simplex architectures. Where does your investigation of “benevolence” in autonomous systems fit into this landscape of models and methods?

Read more »

Help MIRI in a Massive 24-Hour Fundraiser on May 6th

 |   |  News

Update: We’re now liveblogging the fundraiser here.

On May 6th, MIRI is participating in Silicon Valley Gives. We were selected to participate along with other local Bay Area charities by the Silicon Valley Community Foundation. On this day, we recommend donors make gifts to MIRI through the SV Gives portal so we can qualify for some of the matching and bonus funds provided by dozens of Bay Area philanthropists.

Why is this exciting for supporters of MIRI? Many reasons, but here are a few:

  • Over $250,000 of matching funds and prizes up for grabs, from sources that normally wouldn’t contribute to MIRI:
    • Kick-off Match! Two-to-one dollar match up to $50,000 during the midnight hour.
    • $2,000 prize for the nonprofit that has the most individual donors in an hour, every hour for 24 hours.
    • Golden Ticket of $150 added to a random donation each hour, every hour, for 24 hours.
    • Dollar for Dollar match up to $35,000 during the 7 AM hour.
    • Dollar for Dollar match up to $15,000 during the 8 AM hour.
    • Dollar for Dollar match up to $50,000 during the 12 noon hour.
    • Dollar for Dollar match up to $50,000 during the 6 PM hour.
    • Dollar for Dollar match up to $50,000 during the 7 PM hour.
  • Local NBC stations, local radio stations, many local business, and lots of Bay Area foundations will be promoting the Silicon Valley Day of Giving on May 6th. So if MIRI is making a splash with our fundraising that day, it’s possible we’ll draw attention from media and by extension new donors.

We need your help to make the most of this opportunity!

Making the most of this opportunity will require some cleverness and a lot of coordination. We are going to need all the help we can get. Here are some ways you can help:

  1. We are currently thinking through how to best take advantage of  this unique opportunity. If you have any ideas and/or want to join the planning team (currently Malo, Louie, Luke, and long-time MIRI supporter Alexei Andreev), shoot Malo an email at
  2. If you are interested in supporting MIRI with a  donation of $500 or more during the fundraiser, we’d love to coordinate with you to make it count as much as possible. Get in touch with Malo at
  3. All MIRI supporters (not just donors) have the potential to make a big impact if we can all work together in a coordinated manner. Sign up below to receive updates on our strategy leading up to the event, and updates throughout the fundraiser on the best times to give and promote the event. Follow along with the excitement and be on the inside of what’s going on all day!

As featured in:     CNN Money   Forbes   Gizmodo   The Guardian   TIME