Milind Tambe on game theory in security applications

 |   |  Conversations

Milind Tambe portraitMilind Tambe is Helen N. and Emmett H. Jones Professor in Engineering at the University of Southern California (USC). He is a fellow of AAAI (Association for Advancement of Artificial Intelligence) and ACM (Association for Computing Machinery), as well as recipient of the ACM/SIGART Autonomous Agents Research Award, Christopher Columbus Fellowship Foundation Homeland security award, the INFORMS Wagner prize for excellence in Operations Research Practice, the Rist Prize of the Military Operations Research Society, IBM Faculty Award, Okawa Foundation Faculty Research Award, RoboCup scientific challenge award, USC Associates Award for Creativity in Research and USC Viterbi School of Engineering use-inspired research award.

Prof. Tambe has contributed several foundational papers in agents and multiagent systems; this includes areas of multiagent teamwork, distributed constraint optimization (DCOP) and security games. For this research, he has received the “influential paper award” from the International Foundation for Agents and Multiagent Systems (IFAAMAS), as well as with his research group, best paper awards at a number of premier Artificial Intelligence Conferences and workshops; these have included multiple best paper awards at the International Conference on Autonomous Agents and Multiagent Systems and International Conference on Intelligent Virtual Agents.

In addition, the “security games” framework and algorithms pioneered by Prof. Tambe and his research group are now deployed for real-world use by several agencies including the US Coast Guard, the US Federal Air Marshals service, the Transportation Security Administration, LAX Police and the LA Sheriff’s Department for security scheduling at a variety of US ports, airports and transportation infrastructure. This research has led to him and his students receiving the US Coast Guard Meritorious Team Commendation from the Commandant, US Coast Guard First District’s Operational Excellence Award, Certificate of Appreciation from the US Federal Air Marshals Service and special commendation given by the Los Angeles World Airports police from the city of Los Angeles. For his teaching and service, Prof. Tambe has received the USC Steven B. Sample Teaching and Mentoring award and the ACM recognition of service award. Recently, he co-founded ARMORWAY, a company focused on risk mitigation and security resource optimization, where he serves on the board of directors. Prof. Tambe received his Ph.D. from the School of Computer Science at Carnegie Mellon University.

Luke Muehlhauser: In Tambe et al. (2013), you and your co-authors give an overview of game theory in security applications, saying:

Game theory is well-suited to adversarial reasoning for security resource allocation and scheduling problems. Casting the problem as a Bayesian Stackelberg game, we have developed new algorithms for efficiently solving such games to provide randomized patrolling or inspection strategies.

You then give many examples of game-theoretic algorithms used for security at airports, borders, etc.

Is there evidence to suggest that the introduction of these systems has improved the security of the airports, borders, etc. relative to whatever security processes they were using before?

Read more »

New report: “Loudness: On priors over preference relations”

 |   |  News

loudness first pageToday we release the first technical report from our May 2014 workshop: “Loudness: on priors over preference relations” by Benja Fallenstein and Nisan Stiennon. Other technical reports from that workshop are also in progress. Here’s the abstract for this report:

This is a quick writeup of a problem discussed at the May 2014 MIRI workshop: how to formally deal with uncertainty about preferences. We assume that the true preferences satisfy the von Neumann-Morgenstern (VNM) axioms, and can therefore be represented by a utility function. It may seem that we should then simply maximize the expectation of this function. However, in the absence of more information, this is not well-defined; in this setting, different choices of utility functions representing the same VNM preferences can lead the agent to make different choices. We give a formalization of this problem and show that the choice of a prior probability distribution over VNM preference relations together with the choice of a representative for each of these distributions is in a certain sense equivalent to the choice of a single number for every preference relation, which we call its “loudness”. (Mathematically, a “loudness prior” can be seen as a probability distribution over preference relations, but this object does not have an epistemic interpretation.)

MIRI wants to fund your independently-organized Friendly AI workshop

 |   |  News

mirix_smallTo support Friendly AI research around the world, our new MIRIx program funds mathematicians, computer scientists, and formal philosophers to organize their own Friendly AI workshops.

A MIRIx workshop can be as simple as gathering some of your friends to read MIRI papers together, talk about them, eat some snacks, scribble some ideas on whiteboards, and go out to dinner together. Or it can be a multi-day research workshop pursuing a specific line of attack on a particular problem. It’s up to you.

Apply for funding here. In some cases we’ll be able to send a MIRI research fellow to your first meeting to give tutorials and answer questions, or perhaps they’ll Skype in to your workshop to do the same.

Aaron Tomb on crowd-sourced formal verification

 |   |  Conversations

Aaron Tomb portrait Aaron Tomb is a Principal Investigator at Galois, where his work includes research, development, and project leadership in the area of automated and semi-automated techniques for analysis of software, including type systems, defect detection tools, formal verification, and more general software development tools based on deep analysis of program semantics. He joined Galois in 2007, and received a Ph.D. in Computer Science from the University of California, Santa Cruz on a technique for identifying inconsistent assumptions in software source code.

Luke Muehlhauser: DARPA’s Crowd Sourced Formal Verification (CSFV) program “aims to investigate whether large numbers of non-experts can perform formal verification faster and more cost-effectively than conventional processes.” To that end, the program created Verigames.com, the home of several free online puzzle games.

Read more »

Lennart Beringer on the Verified Software Toolchain

 |   |  Conversations

Lennart Beringer portrait Lennart Beringer is an Associate Research Scholar at Princeton University, where he uses interactive proof assistants to develop provably correct compilers, program analyses, and other software verification tools. Previously, he held research appointments at the Ludwig-Maximilians-University Munich and the University of Edinburgh, where he developed proof-carrying-code techniques for mobile code architectures, focusing on properties of resource consumption and information flow security. He received his PhD degree from the University of Edinburgh for a language-based analysis of an idealized asynchronous processor architecture. In 2012, he served as the co-chair of the Third International Conference on Interactive Theorem Proving (ITP).

Read more »

Johann Schumann on high-assurance systems

 |   |  Conversations

Johann Schumann portraitDr. Johann Schumann is a member of the Robust Software Engineering Group RSE at NASA Ames. He obtained his habilitation degree (2000) from the Technische Universität München, Germany on application of automated theorem provers in Software Engineering. His PhD thesis (1991) was on high-performance parallel theorem provers. Dr. Schumann is engaged in research on software and system health management, verification and validation of advanced air traffic control algorithms and adaptive systems, statistical data analysis of air traffic control systems and UAS incident data, and the generation of reliable code for data analysis and state estimation. Dr. Schumann’s general research interests focus on the application of formal and statistical methods to improve design and reliability of advanced safety- and security-critical software.

He is employed by SGT, Inc. as Chief Scientist Computational Sciences.

Read more »

Sandor Veres on autonomous agents

 |   |  Conversations

Sandor Veres portrait Professor Sandor Veres was born and educated in Hungary as applied mathematician. He completed his PhD in dynamical modelling of stochastic systems in 1983 and worked in industry on computer controlled systems. In 1987-1988 he received two consecutive scholarships at Imperial College London and at Linacre College Oxford.

Between 1989-1999 he was lecturer at the Electronic and Electrical engineering department at the University of Birmingham and pursued research in system identification, adaptive control and embedded electronic control systems. In 2000 he joined the University of Southampton to do work in the areas of active vibration control systems, adaptive and learning systems, satellite formation flying and autonomous control. Since 2002 he has held a chair in control systems engineering and was chairman of IFAC Technical Committee of Adaptive and Learning Systems.

At Southampton he has established the Centre for Complex Autonomous Systems Engineering where he is now visiting professor. Today his main research interest is agent-based control systems and he is leading the Autonomous Systems and Robotics Group at the Department of Automatic Control at the University of Sheffield since 2013. He published about 200 papers, authored 4 books and co-authored numerous software packages.

Read more »

New Paper: “Program Equilibrium in the Prisoner’s Dilemma via Löb’s Theorem”

 |   |  News

robust cooperation first pageWe’ve released a new paper recently accepted to the MIPC workshop at AAAI-14: “Program Equilibrium in the Prisoner’s Dilemma via Löb’s Theorem” by LaVictoire et al. This paper is essentially a shortened version of Barasz et al. (2014). For the history of the key results therein, see Robust Cooperation: A Case Study in Friendly AI Research.

Abstract of the new paper:

Applications of game theory often neglect that real-world agents normally have some amount of out-of-band information about each other. We consider the limiting case of a one-shot Prisoner’s Dilemma between algorithms with read access to one anothers’ source code. Previous work has shown that cooperation is possible at a Nash equilibrium in this setting, but existing constructions require interacting agents to be identical or near-identical. We show that a natural class of agents are able to achieve mutual cooperation at Nash equilibrium without any prior coordination of this sort.

 

As featured in:     Business Week   Good   MSNBC   NY Times   Technology Review