Conversation with Holden Karnofsky about Future-Oriented Philanthropy

 |   |  Conversations

Recently, Eliezer and I had an email conversation with Holden Karnofsky to discuss future-oriented philanthropy, including MIRI. The participants were:

We then edited the email conversation into a streamlined conversation, available here.

See also four previous conversations between MIRI and Holden Karnofsky: on existential risk, on MIRI strategy, on transparent research analyses, and on flow-through effects.

John Baez on Research Tactics

 |   |  Conversations

John Baez portraitJohn Baez is a professor of mathematics at U.C. Riverside. Until recently he worked on higher category theory and quantum gravity. His internet column This Week’s Finds dates back to to 1993 and is sometimes called the world’s first blog. In 2010, concerned about climate change and the future of the planet, he switched to working on more practical topics and started the Azimuth Project, an international collaboration to create a focal point for scientists and engineers interested in saving the planet. His research now focuses on the math of networks and information theory, which should help us understand the complex systems that dominate biology and ecology.

Luke Muehlhauser: In a previous interview, I asked Scott Aaronson which “object-level research tactics” he finds helpful when trying to make progress in theoretical research, and I provided some examples. Do you have any comments on the research tactics that Scott and I listed? Which recommended tactics of your own would you add to the list?

John Baez: What do you mean by “object-level” research tactics? I’ve got dozens of tactics. Some of them are ways to solve problems. But equally important, or maybe more so, are tactics for coming up with problems to solve: problems that are interesting but still easy enough to solve. By “object-level”, do you mean the former?
Read more »

2013 in Review: Friendly AI Research

 |   |  MIRI Strategy

This is the 4th part of my personal and qualitative self-review of MIRI in 2013, in which I review MIRI’s 2013 Friendly AI (FAI) research activities.1

Friendly AI research in 2013

  1. In early 2013, we decided to shift our priorities from research plus public outreach to a more exclusive focus on technical FAI research. This resulted in roughly as much public-facing FAI research in 2013 as in all past years combined.
  2. Also, our workshops succeeded in identifying candidates for hire. We expect to hire two 2013 workshop participants in the first half of 2014.
  3. During 2013, I learned many things about how to create an FAI research institute and FAI research field. In particular…
  4. MIRI needs to attract more experienced workshop participants.
  5. Much FAI research can be done by a broad community, and need not be labeled as FAI research. But, more FAI progress is made when the researchers themselves conceive of the research as FAI research.
  6. Communication style matters a lot.

Read more »

  1. What counts as “Friendly AI research” is, naturally, a matter of debate. For most of this post I’ll assume “Friendly AI research” means “what Yudkowsky thinks of as Friendly AI research,” with the exception of intelligence explosion microeconomics, for reasons given in this post. ↩

MIRI’s February 2014 Newsletter

 |   |  Newsletters

Machine Intelligence Research Institute

Dear friends, 

See below for news on our new ebook, new research, new job openings, and Google’s new AI ethics board.

Research Updates

News Updates

Other Updates

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

 

Best,
Luke Muehlhauser
Executive Director

New eBook: ‘Smarter Than Us’

 |   |  News

SmarterThanUsCover-Angled-200pxWe are pleased to release a new ebook, commissioned by MIRI and written by Oxford University’s Stuart Armstrong, and available in EPUB, MOBI, PDF, and from the Amazon and Apple ebook stores.

What happens when machines become smarter than humans? Forget lumbering Terminators. The power of an artificial intelligence (AI) comes from its intelligence, not physical strength and laser guns. Humans steer the future not because we’re the strongest or the fastest but because we’re the smartest. When machines become smarter than humans, we’ll be handing them the steering wheel. What promises—and perils—will these powerful machines present? Stuart Armstrong’s new book navigates these questions with clarity and wit.

Head over to intelligence.org/smarter-than-us/ to grab a copy.

André Platzer on Verifying Cyber-Physical Systems

 |   |  Conversations

André Platzer portraitAndré Platzer is an Assistant Professor of Computer Science at Carnegie Mellon University. He develops the logical foundations of cyber-physical systems to characterize their fundamental principles and to answer the question how we can trust a computer to control physical processes. He received an M.Sc. from the University of Karlsruhe (TH), Germany, in 2004 and a Ph.D. in Computer Science from the University of Oldenburg, Germany, in 2008, after which he joined CMU as an Assistant Professor.

Dr. Platzer received a number of awards for his research on logic of dynamical systems, cyber-physical systems, programming languages, and theorem proving, including an NSF CAREER Award and ACM Doctoral Dissertation Honoroable Mention Award. He was also named one of the Brilliant 10 Young Scientists by the Popular Science magazine and one of the AI’s 10 to Watch by the IEEE Intelligent Systems magazine.

Highlights of Platzer’s thoughts, from the interview below:

  • KeYmaera is a formal verification tool for cyber-physical systems. It has seen many real-world applications, e.g. verifying non-collision in the European Train Control System.
  • KeYmaera’s capability comes from Platzer’s “differential dynamic logic,” which builds on earlier work in (e.g.) dynamic logic.
  • Contra Levitt, Platzer isn’t convinced that autonomous robots will need to use decision theory, though they may.
  • Platzer contrasts formal verification (“did I build the system right?”) with formal validation (“did I build the right system?”). One way to make progress on the latter is to develop what Rushby called “deep assumption tracking.”

Read more »

Gerwin Klein on Formal Methods

 |   |  Conversations

Gerwin Klein portraitGerwin Klein is a Senior Principal Researcher at NICTA, Australia’s National Centre of Excellence for ICT Research, and Conjoint Associate Professor at the University of New South Wales in Sydney, Australia. He is leading NICTA’s Formal Methods research discipline and was the leader of the L4.verified project that created the first machine-checked proof of functional correctness of a general-purpose microkernel in 2009. He joined NICTA in 2003 after receiving his PhD from Technische Universität München, Germany, where he formally proved type-safety of the Java Bytecode Verifier in the theorem prover Isabelle/HOL.

His research interests are in formal verification, programming languages, and low-level systems. Gerwin has won a number of awards together with his team, among them the 2011 MIT TR-10 award for the top ten emerging technologies world-wide, NICTA’s Richard E. Newton impact award for the kernel verification work, the best paper award from SOSP’09 for the same, and an award for the best PhD thesis in Germany in 2003 for his work on bytecode verification. When he is not proving theorems and working on trustworthy software, he enjoys travelling and dabbling in martial arts and photography. Together with Tobias Nipkow he has just published an online draft of the text book Concrete Semantics that teaches programming language semantics using the Isabelle theorem prover.

Highlights of Klein’s thoughts, from the interview below:

  • Verifying code not designed for verification is very difficult and costly. Such “post-mortem verification” has other disadvantages as well.
  • Program designers can use abstraction, modularity, and explicit architecture choices to help make complex systems transparent to humans.
  • There are two ways probability can play a role in verification: (1) direct probabilistic reasoning, in the logic or in a setting where the program itself is probabilistic, or (2) standard non-probabilistic reasoning paired with subjectively uncertain reasoning about what a guarantee means for the overall probability that the system will work as intended.
  • Truly autonomous systems seem to be a long ways off, but if you could make a system with truly unexpected behavior, then you couldn’t make it safe.

Luke Muehlhauser: In your forthcoming paper “Comprehensive Formal Verification of an OS Microkernel,” you and your co-authors describe the kernel design (seL4) you used to ensure its verification would be tractable. You also discuss the process of keeping the formal proof current “as the requirements, design and implementation of the system [changed] over almost a decade.”

How “micro” is the seL4 microkernel? That is, what standard functionality does it provide, and what functionality (that is common in larger OS kernels) does it not provide?

Gerwin Klein: It is pretty micro: it is a true micro-kernel in the L4 tradition. This means it is very small compared to traditional monolithic OS kernels: Linux has on the order of a few million lines of code, seL4 has on the order of 10,000 lines of C. seL4 provides only the core mechanisms that you need to build an OS. These include threads and scheduling, virtual memory, interrupts and asynchronous signals, as well as synchronous message passing. The maybe most important feature of seL4 is its strong access control mechanism that can be used together with the rest to build isolated components with controlled communication between them. These components could be small isolated device drivers or an entire Linux guest OS, the developer can choose the granularity.

The philosophy is: if a mechanism strictly needs privileged hardware access to be implemented, it is in the kernel, but if it can be implemented using the other mechanisms as a user-level task, it is outside the kernel. A surprising amount of features can be outside: device drivers, for instance, graphics, files and file systems, network stacks, even disk paging is not provided by seL4, but can be implemented on top of it. What you (hopefully) get is that tricky complexity is concentrated in the kernel, and user-level OS components become more modular.

Read more »

Conversation with Jacob Steinhardt about MIRI Strategy

 |   |  Conversations, MIRI Strategy

On January 21st, 2014, MIRI met with Jacob Steinhardt to discuss MIRI strategy. Participants were:

We recorded and transcribed much of the conversation, and then edited and paraphrased the transcript for clarity, conciseness, and to protect the privacy of some content. The resulting edited transcript is available in full here (6 pages).

Topics discussed include research communication style, inferential distance, FAI research directions, and Knightian uncertainty.