Paulo Tabuada on program synthesis for cyber-physical systems

 |   |  Conversations

Paulo Tabuada portrait Paulo Tabuada was born in Lisbon, Portugal, one year after the Carnation Revolution. He received his “Licenciatura” degree in Aerospace Engineering from Instituto Superior Tecnico, Lisbon, Portugal in 1998 and his Ph.D. degree in Electrical and Computer Engineering in 2002 from the Institute for Systems and Robotics, a private research institute associated with Instituto Superior Tecnico. Between January 2002 and July 2003 he was a postdoctoral researcher at the University of Pennsylvania. After spending three years at the University of Notre Dame, as an Assistant Professor, he joined the Electrical Engineering Department at the University of California, Los Angeles, where he established and directs the Cyber-Physical Systems Laboratory.

Paulo Tabuada’s contributions to cyber-physical systems have been recognized by multiple awards including the NSF CAREER award in 2005, the Donald P. Eckman award in 2009 and the George S. Axelby award in 2011. In 2009 he co-chaired the International Conference Hybrid Systems: Computation and Control (HSCC’09) and in 2012 he was program co-chair for the 3rd IFAC Workshop on Distributed Estimation and Control in Networked Systems (NecSys’12). He also served on the editorial board of the IEEE Embedded Systems Letters and the IEEE Transactions on Automatic Control. His latest book, on verification and control of hybrid systems, was published by Springer in 2009.

Luke Muehlhauser: In “Abstracting and Refining Robustness for Cyber-Physical Systems,” you and your co-author write that:

…we present a design methodology for robust cyber-physical systems (CPS) [which]… captures two intuitive aims of a robust design: bounded disturbances have bounded consequences and the effect of sporadic disturbances disappears as time progresses.

You use an “abstraction and refinement” procedure for this. How does an abstraction and refinement procedure work, in this context?

Paulo Tabuada: Cyber-physical systems are notoriously difficult to design and verify because of the complex interactions between the cyber and the physical components. Although control theorists have developed powerful techniques for designing and analyzing physical components, say described by differential equations, and computer scientists have developed powerful techniques for designing and analyzing cyber components, say described by finite-state models, these techniques are for the most part incompatible. The latter rely on discrete mathematics while the former rely on continuous mathematics. Our approach is based on replacing all the physical components by cyber abstractions so that all the remaining design and verification tasks can be done in the cyber world. The construction of these abstractions is based on rigorous numerical simulation combined with an analysis of the differential equation models to guarantee that the original physical components and its abstractions are equivalent up to a desired precision. Technically, “equivalent up to a desired precision” means approximately bisimilar and intuitively this means that both models generate the same set of behaviors up to a desired precision.
Read more »

Diana Spears on the safety of adaptive agents

 |   |  Conversations

Diana Spears portrait Diana Spears is an Owner and Research Scientist at Swarmotics, LLC. Previously, she worked at US government laboratories (Goddard, NIST, NRL) and afterwards she was an Associate Professor of Computer Science at the University of Wyoming. She received both the MS and PhD (1990) degrees in Computer Science from the University of Maryland, College Park.

Dr. Spears’s research interests include machine learning, adaptive swarm robotic sensing networks/grids, computational fluid dynamics based algorithms for multi-robot chemical/biological plume tracing and plume mapping, and behaviorally-assured adaptive and machine learning systems. Dr. Spears pioneered the field of safe adaptive agents with her award-winning (2001 NRL Alan Berman Research Publication Award) publication entitled, “Asimovian adaptive agents.” Most recently she and her husband co-edited the book Physicomimetics: Physics-Based Swarm Intelligence,” published by Springer-Verlag in 2012.

Luke Muehlhauser: In Spears (2006) and other publications, you’ve discussed the challenge of ensuring the safety of adaptive (learning) agents:

a designer cannot possibly foresee all circumstances that will be encountered by the agent. Therefore, in addition to supplying an agent with a plan, it is essential to also enable the agent to learn and modify its plan to adapt to unforeseen circumstances. The introduction of learning, however, often makes the agent’s behavior significantly harder to predict. The goal of this research is to verify the behavior of adaptive agents. In particular, our objective is to develop efficient methods for determining whether the behavior of learning agents remains within the bounds of prespecified constraints… after learning…

…Our results include proofs that… with respect to important classes of properties… if the [safety] property holds for the agent’s plan prior to learning, then it is guaranteed to still hold after learning. If an agent uses these “safe” learning operators, it will be guaranteed to preserve the properties with no reverification required. This is the best one could hope for in an online situation where rapid response time is critical. For other learning operators and property classes our a priori results are negative. However, for these cases we have developed incremental reverification algorithms that can save time over total reverification from scratch.

What do you mean by “incremental” reverification algorithms, as in the last sentence I quoted?

Diana Spears: Verification (model checking, in particular) consists of proving that a computer program satisfies a desirable property/constraint and, if it does not, a counterexample is provided. In my work, I assume that this program is a (multi)agent plan for action.  In most real-world applications, plans are typically enormous and therefore verification may be quite time-consuming. Suppose the safety property/constraint that agent A must always obey is that “agent A should always be at least M units away from agent B” (to prevent collisions). Let’s assume that initial verification proved that the entire plan (consisting of all action sequences that agent A could ever possibly take) is guaranteed to obey this property in all circumstances. Furthermore, let’s assume that adaptation is required after the agent has been fielded, where adaptation consists of applying a machine learning operator to modify the plan. For example, suppose a specific part of the plan states that agent A should “move from location 3 to location 4 if there is a clear path between 3 and 4, the ground is fairly level (e.g., nowhere higher than X or lower than Y between locations 3 and 4), and if the schedule permits such movement at this time.” Then an example machine learning operator might change the “4″ to “6″ based on new information about the task being performed.

Note that this learning operator only modifies one condition in one miniscule portion of the entire plan.Therefore, why re-verify that the entire plan still satisfies the desired property after learning? Why not re-verify only the specific portion of the plan that was modified, as well as any parts of the plan that depend on the modified portion?  That is what “incremental re-verification” does. It localizes post-adaptation verification to only those parts of the plan that are essential to re-verify.  In doing so, it improves the time complexity of re-verification. Time complexity is a very important and practical consideration for online systems – especially those that operate in real-time or in time-critical situations. In my research I ran numerous experiments comparing the CPU time of re-verifying an entire plan versus localized incremental re-verification of the plan after learning. My results showed as much as a 1/2-billion-fold speedup using incremental re-verification! And that’s using a plan that’s tiny compared to what agents would typically use in the real world.
Read more »

Will MacAskill on normative uncertainty

 |   |  Conversations

William MacAskill portrait Will MacAskill recently completed his DPhil at Oxford University and, as of October 2014 will be a Research Fellow at Emmanuel College, Cambridge.

He is the cofounder of Giving What We Can and 80,000 Hours. He’s currently writing a book, Effective Altruism, to be published by Gotham (Penguin USA) in summer 2015.

Luke Muehlhauser: In MacAskill (2014) you tackle the question of normative uncertainty:

Very often, we are unsure about what we ought to do… Sometimes, this uncertainty arises out of empirical uncertainty: we might not know to what extent non-human animals feel pain, or how much we are really able to improve the lives of distant strangers compared to our family members. But this uncertainty can also arise out of fundamental normative uncertainty: out of not knowing, for example, what moral weight the wellbeing of distant strangers has compared to the wellbeing of our family; or whether non-human animals are worthy of moral concern even given knowledge of all the facts about their biology and psychology.

…one might have expected philosophers to have devoted considerable research time to the question of how one ought to take one’s normative uncertainty into account in one’s decisions. But the issue has been largely neglected. This thesis attempts to begin to fill this gap.

In the first part of your thesis you argue that when the moral theories to which an agent assigns some credence are cardinally measurable (as opposed to ordinal-scale) and they are intertheoretically comparable, the agent should choose an action which “maximizes expected choice-worthiness” (MEC), which is akin to maximizing expected value across multiple uncertain theories of what is desirable.

I suspect that result will be intuitive to many, so let’s jump forward to where things get more interesting. You write:

Sometimes, [value] theories are merely ordinal, and, sometimes, even when theories are cardinal, choice-worthiness is not comparable between them. In either of these situations, MEC cannot be applied. In light of this problem, I propose that the correct metanormative theory is sensitive to the different sorts of information that different theories provide. In chapter 2, I consider how to take normative uncertainty into account in conditions where all theories provide merely ordinal choice-worthiness, and where choice-worthiness is noncomparable between theories, arguing in favour of the Borda Rule.

What is the Borda Rule, and why do you think it’s the best action rule under these conditions?

Will MacAskill: Re: “I suspect that result will be intuitive to many.” Maybe in your circles that’s true! Many, or even most, philosophers get off the boat way before this point. They say that there’s no sense of ‘ought’ according to which what one ought to do takes normative uncertainty into account. I’m glad that I don’t have to defend that for you, though, as I think it’s perfectly obvious that the ‘no ought’ position is silly.

As for the Borda Rule: the Borda Rule is a type of voting system, which works as follows. For each theory, an option’s Borda Score is equal to the number of options that rank lower in the theory’s choice-worthiness ordering than that option. An option’s Credence-Weighted Borda Score is equal to the sum, across all theories, of the decision-maker’s credence in the theory multiplied by the Borda Score of the option, on that theory.

So, for example, suppose I have 80% credence in Kantianism and 20% credence in Contractualism. (Suppose I’ve had some very misleading evidence….) Kantianism says that option A is the best option, then option B, then option C. Contractualism says that option C is the best option, then option B, then option A.

The Borda scores, on Kantianism, are:
A = 2
B = 1
C = 0

The Borda scores, on Contractualism, are:
A = 0
B = 1
C = 2

Each option’s Credence-Weighted Borda Score is:
A = 0.8*2 + 0.2*0 = 1.6
B = 0.8*1 + 0.2*1 = 1
C = 0.8*0 + 0.2*2 = 0.4

So, in this case, the Borda Rule would say that A is the most appropriate option, followed by B, and then C.

The reason we need to use some sort of voting system is because I’m considering, at this point, only ordinal theories: theories that tell you that it’s better to choose A over B (alt: that “A is more choice-worthy than B”), but won’t tell you how much more choice-worthy A is than B. So, in these conditions, we have to have a theory of how to take normative uncertainty into account that’s sensitive only to each theory’s choice-worthiness ordering (as well as the degree of credence in each theory), because the theories I’m considering don’t give you anything more than an ordering.

The key reason why I think the Borda Rule is better than any other voting system is that it satisfies a condition I call Updating Consistency. The idea is that increasing your credence in some particular theory T1 shouldn’t make the appropriateness ordering (that is, the ordering of options in terms of what-you-ought-to-do-under-normative-uncertainty) worse by the lights of T1.

This condition seems to me to be very plausible indeed. But, surprisingly, very few voting systems satisfy that property, and those others that do have other problems.
Read more »

Erik DeBenedictis on supercomputing

 |   |  Conversations

Erik DeBenedictis portrait Erik DeBenedictis works for Sandia’s Advanced Device Technologies department. He has been a member of the International Technology Roadmap for Semiconductors since 2005.

DeBenedictis has received Ph.D. in computer science from Caltech. As a grad student and post-doc, he worked on the hardware that turned into the first hypercube multiprocessor computer. Later dubbed the “Cosmic Cube,” it ran for more than a decade after he left the university and was copied over and over. It’s considered the ancestor of most of today’s supercomputers.

In the 1980s, then working for Bell Labs in Holmdel, N.J., DeBenedictis was part of a consortium competing for the first Gordon Bell award. The team got the second place award, the first place going to Sandia. During the 1990s, he ran NetAlive, Inc., a company developing information management software for desktops and wireless systems. Starting in 2002, DeBenedictis was one of the project leads on the Red Storm supercomputer.

Read more »

2013 in Review: Fundraising

 |   |  MIRI Strategy

Update 04/16/2014: At a donors request I have replaced the Total Donations per Year chart with one that shows which proportion of the donations were from new and returning donors. Some tweaks were also made to our donation database since the publication of this post, so I have updated the post to reflect these changes.


This is the 5th part of my personal and qualitative self-review of MIRI in 2013, in which I review MIRI’s 2013 fundraising activities.

For this post, “fundraising” includes donations and grants, but not other sources of revenue.1



  1. Our funding in 2013 grew by about 75% compared to 2012, though comparing to past years is problematic because MIRI is now a very different organization than it was in 2012 and earlier.
  2. We began to apply for grants in late 2013. We haven’t received money from any of these grantmakers yet, but several of our grant applications are pending.
  3. MIRI’s ability to spend money on its highest-value work is much greater than it was one year ago, and we plan to fundraise heavily to meet our 2014 fundraising goal of $1.7 million.

Read more »

  1. I didn’t include other sources of revenue in this analysis because they don’t seem likely to play a significant role in our ongoing funding strategy in the forseeable future. For example, revenue from ebook sales is marginal, and we don’t plan to sell tickets to a new conference. 

Lyle Ungar on forecasting

 |   |  Conversations

Lyle Ungar portrait Dr. Lyle Ungar is a Professor of Computer and Information Science at the University of Pennsylvania, where he also holds appointments in multiple departments in the schools of Engineering, Arts and Sciences, Medicine, and Business. He has published over 200 articles and is co-inventor on eleven patents. His research areas include machine learning, data and text mining, and psychology, with a current focus on statistical natural language processing, spectral methods, and the use of social media to understand the psychology of individuals and communities.

Luke Muehlhauser: One of your interests (among many) is forecasting. Some of your current work is funded by IARPA’s ACE program — one of the most exciting research programs happening anywhere in the world, if you ask me.

One of your recent papers, co-authored with Barbara Mellers, Jonathan Baron, and several others, is “Psychological Strategies for Winning a Geopolitical Forecasting Tournament.” The abstract is:

Five university-based research groups competed to assign the most accurate probabilities to events in two geopolitical forecasting tournaments. Our group tested and found support for three psychological drivers of accuracy: training, teaming, and tracking. Training corrected cognitive biases, encouraged forecasters to use reference classes, and provided them with heuristics, such as averaging when multiple estimates were available. Teaming allowed forecasters to share information and discuss the rationales behind their beliefs. Tracking placed the highest performers (top 2% from Year 1) in elite teams that worked together. Results showed that probability training improved calibration. Team collaboration and tracking enhanced both calibration and resolution. Forecasting is often viewed as a statistical problem; but it is also a deep psychological problem. Behavioral interventions improved the accuracy of forecasts, and statistical algorithms improved the accuracy of aggregations. Our group produced the best forecasts two years in a row by putting statistics and psychology to work.

In these experiments, some groups were given scenario training or probability training, which “took approximately 45 minutes, and could be examined throughout the tournament.”

Are these modules available to the public online? If not, can you give us a sense of what they were like? And, do you suspect that significant additional probability or scenario training would further reduce forecasting errors, e.g. if new probability training content was administered to subjects for 30 minutes every two weeks?

Read more »

Anil Nerode on hybrid systems control

 |   |  Conversations

Anil Nerode portrait Dr. Anil Nerode is a Goldwin Smith Professor of Mathematics and Computer Science at the Cornell University. He is “a pioneer in mathematical logic, computability, automata theory, and the understanding of computable processes, both theoretical and practical for over half a century, whose work comes from a venerable and distinguished mathematical tradition combined with the newest developments in computing and technology.”

His 50 Ph.D.’s and their students occupy many major university and industrial positions world-wide in mathematics, computer science, software engineering, electrical engineering, etc. He and Wolf Kohn founded the discipline of hybrid systems in 1992 which has become a major area of research in mathematics, computer science, and many branches of engineering. Their work on modeling control of macroscopic systems as relaxed calculus of variations problems on Finsler manifolds is the ground for their current efforts in quantum control and artificial photosynthesis. His research has been supported consistently by many entities, ranging from NSF (50 years) to ADWADC, AFOSR, ARO, USEPA, etc. He has been a consultant on military development projects since 1954. He received his Ph.D. in Mathematics from the University of Chicago under Saunders MacLane (1956).

Luke Muehlhauser: In Nerode (2007), you tell the origin story of hybrid systems control. A 1990 DARPA meeting in Pacifica seems to have been particularly seminal. As you describe it:

the purpose of the meeting was to explore how to clear a major bottleneck, the control of large military systems such as air-land-sea forces in battle space.

Can you describe in more detail what DARPA’s long-term objectives for that meeting seemed to be? Presumably they hoped the meeting would spur new lines of research that would allow them to solve particular control problems in the next 5-20 years?

Read more »

Michael Carbin on integrity properties in approximate computing

 |   |  Conversations

Michael Carbin portraitMichael Carbin is a Ph.D. Candidate in Electrical Engineering and Computer Science at MIT. His interests include the design of programming systems that deliver improved performance and resilience by incorporating approximate computing and self-healing.

His work on program analysis at Stanford University as an undergraduate received an award for Best Computer Science Undergraduate Honors Thesis. As a graduate student, he has received the MIT Lemelson Presidential and Microsoft Research Graduate Fellowships. His recent research on verifying the reliability of programs that execute on unreliable hardware received a best paper award at OOPSLA 2013.

Luke Muehlhauser: In Carbin et al. (2013), you and your co-authors present Rely, a new programming language that ”enables developers to reason about the… probability that [a program] produces the correct result when executed on unreliable hardware.” How is Rely different from earlier methods for achieving reliable approximate computing?

Michael Carbin: This is a great question. Building applications that work with unreliable components has been a long-standing goal of the distributed systems community and other communities that have investigated how to build systems that are fault-tolerant. A key goal of a fault tolerant system is to deliver a correct result even in the presence of errors in the system’s constituent components.

This goal stands in contrast to the goal of the unreliable hardware that we have targeted in my work. Specifically, hardware designers are considering new designs that will — purposely — expose components that may silently produce incorrect results with some non-negligible probability. These hardware designers are working in a subfield that is broadly called approximate computing.

The key idea of the approximate computing community is that many large-scale computations (e.g., machine learning, big data analytics, financial analysis, and media processing) have a natural trade-off between the quality of their results and the time and resources required to produce a result. Exploiting this fact, researchers have devised a number of techniques that take an existing application and modify it to trade the quality of its results for increased performance or decreased power consumption.

One example that my group has worked on is simply skipping parts of a computation that we have demonstrated — through testing — can be elided without substantially affecting the overall quality of the application’s result. Another approach is executing portions of an application that are naturally tolerant of errors on these new unreliable hardware systems.

A natural follow-on question to this is, how have developers previously dealt with approximation?

These large-scale applications are naturally approximate because exact solutions are often intractable or perhaps do not even exist (e.g., machine learning). The developers of these applications therefore often start from an exact model of how to compute an accurate result and then use that model as a guide to design a tractable algorithm and a corresponding implementation that returns a more approximate solution. These developers have therefore been manually applying approximations to their algorithms (and their implementations) and reasoning about the accuracy of their algorithms for some time. A prime example of this is the field of numerical analysis and its contributions to scientific computing.

The emerging approximate computing community represents the realization that programming languages, runtime systems, operating systems, and hardware architectures can not only help developers navigate the approximations they need to make when building these applications, but also that these systems can incorporate approximations themselves. So for example, the hardware architecture may itself export unreliable hardware components that an application’s developers can then use as one of their many tools for performing approximation.
Read more »

As featured in:     Forbes   Good   Popular Science   SF Weekly   WIRED