Selsam on formal verification of machine learning

Here is the first result out of the project Verifying Deep Mathematical Properties of AI SystemsTechnical abstract available here. Note that David Dill has taken over as PI from Alex Aiken. funded through the Future of Life Institute.

Noisy data, non-convex objectives, model misspecification, and numerical instability can all cause undesired behaviors in machine learning systems. As a result, detecting actual implementation errors can be extremely difficult. We demonstrate a methodology in which developers use an interactive proof assistant to both implement their system and to state a formal theorem defining what it means for their system to be correct. The process of proving this theorem interactively in the proof assistant exposes all implementation errors since any error in the program would cause the proof to fail. As a case study, we implement a new system, Certigrad, for optimizing over stochastic computation graphs, and we generate a formal (i.e. machine-checkable) proof that the gradients sampled by the system are unbiased estimates of the true mathematical gradients. We train a variational autoencoder using Certigrad and find the performance comparable to training the same model in TensorFlow.

You can find discussion on HackerNews. The lead author was kind enough to answers some questions about this work.

Q: Is the correctness specification usually a fairly singular statement? Or will it often be of the form “The program satisfied properties A, B, C, D, and E”? (And then maybe you add “F” later.)

Daniel Selsam: There are a few related issues: how singular is a specification, how much of the functionality of the system is certified (coverage), and how close the specification comes to proving that the system actually does what you want (validation).… [continue reading]

Executive branch reasonable on AI

President Obama was directly asked in a Wired interview about the dangers Bostrom raises regarding AI. From the transcript:

DADICH: I want to center our conversation on artificial intelligence, which has gone from science fiction to a reality that’s changing our lives. When was the moment you knew that the age of real AI was upon us?

OBAMA: My general observation is that it has been seeping into our lives in all sorts of ways, and we just don’t notice; and part of the reason is because the way we think about AI is colored by popular culture. There’s a distinction, which is probably familiar to a lot of your readers, between generalized AI and specialized AI. In science fiction, what you hear about is generalized AI, right? Computers start getting smarter than we are and eventually conclude that we’re not all that useful, and then either they’re drugging us to keep us fat and happy or we’re in the Matrix. My impression, based on talking to my top science advisers, is that we’re still a reasonably long way away from that. It’s worth thinking about because it stretches our imaginations and gets us thinking about the issues of choice and free will that actually do have some significant applications for specialized AI, which is about using algorithms and computers to figure out increasingly complex tasks. We’ve been seeing specialized AI in every aspect of our lives, from medicine and transportation to how electricity is distributed, and it promises to create a vastly more productive and efficient economy. If properly harnessed, it can generate enormous prosperity and opportunity. But it also has some downsides that we’re gonna have to figure out in terms of not eliminating jobs.

[continue reading]

X-risk postdocs at Cambridge

The Centre for the Study of Existential Risk (CSER) in Cambridge is now taking applications for four 2-year postdocs to work on existential risks from technology.

As I’ve reported before, there are good reasons to think that the importance of such risks goes beyond the 7 billion lives that are immediately at stake. And we should expect the mitigation of these dangers to be undersupplied by the market.

It’s very exciting to see CSER go from an ambitious idea to a living, breathing, funded thing. As effective altruism becomes more mainstream, we should expect the obvious neglected causes to begin to dry up. If you care about existential risk, I have it on good authority that researchers are in short supply. So I encourage you to apply if you’re interested. (EDIT: The deadline is April 24th.)



DOUBLE EDIT: The Future of Humanity Institute in Oxford is also hiring for one postdoc, due April 27th.

The full CSER job posting is here:

Up to four full-time postdoctoral research associates to work on the project Towards a Science of Extreme Technological Risk (ETR) within the Centre for the Study of Existential Risk (CSER).

CSER’s research focuses on the identification, management and mitigation of possible extreme risks associated with future technological advances. We are currently based within the University’s Centre for Research in the Arts, Social Sciences and Humanities (CRASSH). Our goal is to bring together some of the best minds from academia, industry and the policy world to tackle the challenges of ensuring that powerful new technologies are safe and beneficial. We focus especially on under-studied high-impact risks – risks that might result in a global catastrophe, or even threaten human extinction, even if only with low probability.

[continue reading]

Musk donates $10M to Future of Life Institute

The Future of Life Institute (FLI) is a group of folks, mostly academics with a few notable celebrities, who are jointly concerned about existential risk, especially risks from technologies that are expected to emerge in the coming decades. In particular, prominent physicists Anthony Aguirre, Alan Guth, Stephen Hawking, Saul Perlmutter, Max Tegmark, and Frank Wilczek are on the advisory board. I attended their public launch event at MIT in May (a panel discussion), and I am lucky to be acquainted with a few of the members and supporters. Although not a self-described Effective Altruist (EA) organization, FLI has significant overlap in philosophy, methods, and personnel with other EA groups.

One of the chief risks that FLI is concerned with is the safe development of artificial intelligence in the long term. Oxford Philosopher Nick Bostrom has a new book out on this topic, which seems to have convinced nerd hero Elon Musk that AI risk is a valid concern. Yesterday, Musk made a $10 million donation to FLI to fund grants for researchers in this area.

This is a big deal for those who think that there is a huge underinvestment in this sort of work. It’s also good fodder for journalists who like to write about killer robots. I expect the quality of the public discussion about this to be…low.

EDIT: The grant application process is now open. … [continue reading]

Argument against EA warmth risk

When I’m trying to persuade someone that people ought to concentrate on effectiveness when choosing which charities to fund, I sometime hear the worry that this sort of emphasis on cold calculation risks destroying the crucial human warmth and emotion that should surround charitable giving. It’s tempting to dismiss this sort of worry out of hand, but it’s much more constructive to address it head on.I also think it gestures at a real aspect of “EA cultural”, although the direction of causality is unclear. It could just be that EA ideas are particularly attractive to us cold unfeeling robots. This situations happened to me today, and I struggled for a short and accessible response. I came up with the following argument later, so I’m posting it here.

It’s often noticed that many of the best surgeons treat their patients like a broken machine to be fixed, and lack any sort of bedside manner. Surgeons are also well known for their gallows humor, which has been thought to be a coping mechanism to deal with death and with the unnatural act of cutting open a living human body. Should we be worried that surgery dehumanizes the surgeon? Well, yes, this is a somewhat valid concern, which is even being addressed (with mixed results).

But in context this is only a very mild concern. The overwhelmingly most important thing is that the surgery is actually performed, and that it is done well. If someone said “I don’t think we should have doctors perform surgery because of the potential for it to take the human warmth out of medicine”, you’d rightly call them crazy! No one wants to die from a treatable appendicitis, no matter how comforting the warm and heartfelt doctors are.… [continue reading]

State of EA organizations

Below is a small document I prepared to summarize the current slate of organizations that are strongly related to effective altruismThere is a bit of arbitrariness about what to include.  There are some organizations that are strongly aligned with EA principles even if they do not endorse that name or the full philosophy.I am not including cause-level organization for mainstream causes, e.g. developing world health like Innovations for Poverty Action. I am including all existential risk organizations, since these are so unusual and potentially important for EA.. (A Google doc is available here, which can be exported to many other formats.) If I made a mistake please comment below or email me. Please feel free to take this document and build on it, especially if you would like to expand the highlights section.

By Category

Charity Evaluation

Existential risk

Meta

Former names

“Effective Fundraising” → Charity Science (Greatest Good Foundation)
“Singularity Institute” → Machine Intelligence Research Institute
“Effective Animal Activism” → Animal Charity Evaluators

Organizational relationships

FHI and CEA share office space at Oxford.  CEA is essentially an umbrella organization.  It contains GWWC and 80k, and formerly contained TLYCS and ACE.  Now the latter two organizations operate independently.

MIRI and CFAR currently share office space in Berkeley and collaborate from time to time.… [continue reading]

Impact discrepancies persist under uncertainty

[Tomasik has updated his essay to address some of these issues]

Brian Tomasik’s website, utilitarian-essays.com, contains many thoughtful pieces he has written over the years from the perspective of a utilitarian who is concerned deeply with wild animal suffering. His work has been a great resource of what is now called the effective altrusim community, and I have a lot of respect for his unflinching acceptance and exploration of our large obligations conditional on the moral importance of all animals.

I want to briefly take issue with a small but important part of Brain’s recent essay “Charity cost effectiveness in an uncertain world“. He discusses the difficult problem facing consequentialists who care about the future, especially the far future, on account of how difficult it is predict the many varied flow-through effects of our actions. In several places, he suggests that this uncertainty will tend to wash out the enormous differences in effectiveness attributed to various charities (and highlighted by effective altruists) when measured by direct impact (e.g. lives saved per dollar).

…When we consider flow-through effects of our actions, the seemingly vast gaps in cost-effectiveness among charities are humbled to more modest differences, and we begin to find more worth in the diversity of activities that different people are pursuing…

…For example, insofar as a charity encourages cooperation, philosophical reflection, and meta-thinking about how to best reduce suffering in the future — even if only by accident — it has valuable flow-through effects, and it’s unlikely these can be beaten by many orders of magnitude by something else…

…I don’t expect some charities to be astronomically better than others…

Although I agree on the importance of the uncertain implications of flow-through effects, I disagree with the suggestion that this should generally be expected to even out differences in effectiveness.… [continue reading]

Cosmology meets philanthropy

[This was originally posted at the Quantum Pontiff.]

People sometimes ask me what how my research will help society.  This question is familiar to physicists, especially those of us whose research is connected to every-day life only… shall we say…tenuously.  And of course, this is a fair question from the layman; tax dollars support most of our work.

I generally take the attitude of former Fermilab director Robert R. Wilson.  During his testimony before the Joint Committee on Atomic Energy in the US Congress, he was asked how discoveries from the proposed accelerator would contribute to national security during a time of intense Cold War competition with the USSR.  He famously replied “this new knowledge has all to do with honor and country but it has nothing to do directly with defending our country except to help make it worth defending.”

Still, it turns out there are philosophers of practical ethics who think a few of the academic questions physicists study could have tremendous moral implications, and in fact might drive key decisions we all make each day. Oxford philosopher Nick Bostrom has in particular written about the idea of “astronomical waste“.  As is well known to physicists, the universe has a finite, ever-dwindling supply of negentropy, i.e. the difference between our current low-entropy state and the bleak maximal entropy state that lies in our far future.  And just about everything we might value is ultimately powered by it.  As we speak (or blog), the stupendously vast majority of negentropy usage is directed toward rather uninspiring ends, like illuminating distant planets no one will ever see.

These resources can probably be put to better use.  … [continue reading]

Happier livestock through genetic bundling

Carl Shulman posted on OvercomingBias about an easier way to produce animals that suffer less: selective breeding.  In contrast to a lot of the pie-in-the-sky talk about genetically engineering animals to feel less pain, selective breeding is a proven and relatively cheap method that can produce animals with traits that increase a complicated weighted sum of many parameters.  As Shulman points out, the improvements are impressive, and breeding methods are likely to work just as well for reducing suffering as increasing milk output (although these goals may conflict in the same animal).

So suppose an animal-welfare organization is able to raise the resources necessary to run such a breeding program.  They immediately run up against the problem of how to induce large-scale farming operations to use their new breed of less-suffering chickens.  Indeed, in the comments to Shulman’s post, Gaverick Matheny pointed out that an example of a welfare-enhanced breed exists but is rarely used because it is less productive.

It’s true that there should be some low-hanging welfare fruit that has negligible effect on farm profits.  But even these are unlikely to be adopted due to economic frictions.  (Why would most farmers risk changing to an untested breed produced by an organization generally antagonistic toward them?)  So how can an animal-welfare organization induce adoption of their preferred breed?  My proposal is to bundle their welfare-enhancing modifications with productivity-enhancing modifications that are not already exploited because of inefficiencies in the market for livestock breeds.

The incentives which exist for businesses to invest in selective breeding almost certainly do not lead to the maximum total value.  Breeder businesses are only able to capture some of the value that accrues from their animal improvements.  … [continue reading]