
Understanding properties of deep neural networks is an important challenge in
deep learning. In this paper, we take a step in this direction by proposing a
rigorous way of verifying properties of a popular class of neural networks,
Binarized Neural Networks, using the welldeveloped means of Boolean
satisfiability. Our main contribution is a construction that creates a
representation of a binarized neural network as a Boolean formula. Our encoding
is the first exact Boolean representation of a deep neural network. Using this
encoding, we leverage the power of modern SAT solvers along with a proposed
counterexampleguided search procedure to verify various properties of these
networks. A particular focus will be on the critical property of robustness to
adversarial perturbations. For this property, our experimental results
demonstrate that our approach scales to mediumsize deep neural networks used
in image classification tasks. To the best of our knowledge, this is the first
work on verifying properties of deep neural networks using an exact Boolean
encoding of the network.

Despite efforts to increase the supply of organs from living donors, most
kidney transplants performed in Australia still come from deceased donors. The
age of these donated organs has increased substantially in recent decades as
the rate of fatal accidents on roads has fallen. The Organ and Tissue Authority
in Australia is therefore looking to design a new mechanism that better matches
the age of the organ to the age of the patient. I discuss the design,
axiomatics and performance of several candidate mechanisms that respect the
special online nature of this fair division problem.

Peer reviews, evaluations, and selections are a fundamental aspect of modern
science. Funding bodies the world over employ experts to review and select the
best proposals from those submitted for funding. The problem of peer selection,
however, is much more general: a professional society may want to give a subset
of its members awards based on the opinions of all members; an instructor for a
Massive Open Online Course (MOOC) or an online course may want to crowdsource
grading; or a marketing company may select ideas from group brainstorming
sessions based on peer evaluation.
We make three fundamental contributions to the study of peer selection, a
specific type of group decisionmaking problem, studied in computer science,
economics, and political science. First, we propose a novel mechanism that is
strategyproof, i.e., agents cannot benefit by reporting insincere valuations.
Second, we demonstrate the effectiveness of our mechanism by a comprehensive
simulationbased comparison with a suite of mechanisms found in the literature.
Finally, our mechanism employs a randomized rounding technique that is of
independent interest, as it solves the apportionment problem that arises in
various settings where discrete resources such as parliamentary representation
slots need to be divided proportionally.

There is significant concern that technological advances, especially in
Robotics and Artificial Intelligence (AI), could lead to high levels of
unemployment in the coming decades. Studies have estimated that around half of
all current jobs are at risk of automation. To look into this issue in more
depth, we surveyed experts in Robotics and AI about the risk, and compared
their views with those of nonexperts. Whilst the experts predicted a
significant number of occupations were at risk of automation in the next two
decades, they were more cautious than people outside the field in predicting
occupations at risk. Their predictions were consistent with their estimates for
when computers might be expected to reach human level performance across a wide
range of skills. These estimates were typically decades later than those of the
nonexperts. Technological barriers may therefore provide society with more
time to prepare for an automated future than the public fear. In addition,
public expectations may need to be dampened about the speed of progress to be
expected in Robotics and AI.

Sequential allocation is a simple mechanism for sharing multiple indivisible
items. We study strategic behavior in sequential allocation. In particular, we
consider Nash dynamics, as well as the computation and Pareto optimality of
pure equilibria, and Stackelberg strategies. We first demonstrate that, even
for two agents, better responses can cycle. We then present a lineartime
algorithm that returns a profile (which we call the "bluff profile") that is in
pure Nash equilibrium. Interestingly, the outcome of the bluff profile is the
same as that of the truthful profile and the profile is in pure Nash
equilibrium for \emph{all} cardinal utilities consistent with the ordinal
preferences. We show that the outcome of the bluff profile is Pareto optimal
with respect to pairwise comparisons. In contrast, we show that an assignment
may not be Pareto optimal with respect to pairwise comparisons even if it is a
result of a preference profile that is in pure Nash equilibrium for all
utilities consistent with ordinal preferences. Finally, we present a dynamic
program to compute an optimal Stackelberg strategy for two agents, where the
second agent has a constant number of distinct values for the items.

Motivated by the common academic problem of allocating papers to referees for
conference reviewing we propose a novel mechanism for solving the assignment
problem when we have a two sided matching problem with preferences from one
side (the agents/reviewers) over the other side (the objects/papers) and both
sides have capacity constraints. The assignment problem is a fundamental
problem in both computer science and economics with application in many areas
including task and resource allocation. We draw inspiration from multicriteria
decision making and voting and use order weighted averages (OWAs) to propose a
novel and flexible class of algorithms for the assignment problem. We show an
algorithm for finding a $\Sigma$OWA assignment in polynomial time, in contrast
to the NPhardness of finding an egalitarian assignment. Inspired by this
setting we observe an interesting connection between our model and the classic
proportional multiwinner election problem in social choice.

The recent surge in interest in ethics in artificial intelligence may leave
many educators wondering how to address moral, ethical, and philosophical
issues in their AI courses. As instructors we want to develop curriculum that
not only prepares students to be artificial intelligence practitioners, but
also to understand the moral, ethical, and philosophical impacts that
artificial intelligence will have on society. In this article we provide
practical case studies and links to resources for use by AI educators. We also
provide concrete suggestions on how to integrate AI ethics into a general
artificial intelligence course and how to teach a standalone artificial
intelligence ethics course.

We consider approvalbased committee voting, i.e. the setting where each
voter approves a subset of candidates, and these votes are then used to select
a fixedsize set of winners (committee). We propose a natural axiom for this
setting, which we call justified representation (JR). This axiom requires that
if a large enough group of voters exhibits agreement by supporting the same
candidate, then at least one voter in this group has an approved candidate in
the winning committee. We show that for every list of ballots it is possible to
select a committee that provides JR. However, it turns out that several
prominent approvalbased voting rules may fail to output such a committee. In
particular, while Proportional Approval Voting (PAV) always outputs a committee
that provides JR, Reweighted Approval Voting (RAV), a tractable approximation
to PAV, does not have this property. We then introduce a stronger version of
the JR axiom, which we call extended justified representation (EJR), and show
that PAV satisfies EJR, while other rules we consider do not; indeed, EJR can
be used to characterize PAV within the class of weighted PAV rules. We also
consider several other questions related to JR and EJR, including the
relationship between JR/EJR and core stability, and the complexity of the
associated algorithmic problems.

An author's profile on Google Scholar consists of indexed articles and
associated data, such as the number of citations and the Hindex. The author is
allowed to merge articles; this may affect the Hindex. We analyze the
(parameterized) computational complexity of maximizing the Hindex using
article merges. Herein, to model realistic manipulation scenarios, we define a
compatibility graph whose edges correspond to plausible merges. Moreover, we
consider several different measures for computing the citation count of a
merged article. For the measure used by Google Scholar, we give an algorithm
that maximizes the Hindex in linear time if the compatibility graph has
constantsize connected components. In contrast, if we allow to merge arbitrary
articles (that is, for compatibility graphs that are cliques), then already
increasing the Hindex by one is NPhard. Experiments on Google Scholar
profiles of AI researchers show that the Hindex can be manipulated
substantially only if one merges articles with highly dissimilar titles.

Computational Social Choice (ComSoc) is a rapidly developing field at the
intersection of computer science, economics, social choice, and political
science. The study of tournaments is fundamental to ComSoc and many results
have been published about tournament solution sets and reasoning in
tournaments. Theoretical results in ComSoc tend to be worst case and tell us
little about performance in practice. To this end we detail some experiments on
tournaments using real wold data from soccer and tennis. We make three main
contributions to the understanding of tournaments using real world data from
English Premier League, the German Bundesliga, and the ATP World Tour: (1) we
find that the NPhard question of finding a seeding for which a given team can
win a tournament is easily solvable in real world instances, (2) using detailed
and principled methodology from statistical physics we show that our real world
data obeys a lognormal distribution; and (3) leveraging our lognormal
distribution result and using robust statistical methods, we show that the
popular Condorcet Random (CR) tournament model does not generate realistic
tournament data.

The hindex is an important bibliographic measure used to assess the
performance of researchers. Dutiful researchers merge different versions of
their articles in their Google Scholar profile even though this can decrease
their hindex. In this article, we study the manipulation of the hindex by
undoing such merges. In contrast to manipulation by merging articles (van
Bevern et al. [Artif. Intel. 240:1935, 2016]) such manipulation is harder to
detect. We present numerous results on computational complexity (from
lineartime algorithms to parameterized computational hardness results) and
empirically indicate that at least small improvements of the hindex by
splitting merged articles are unfortunately easily achievable.

We propose a model of interdependent scheduling games in which each player
controls a set of services that they schedule independently. A player is free
to schedule his own services at any time; however, each of these services only
begins to accrue reward for the player when all predecessor services, which may
or may not be controlled by the same player, have been activated. This model,
where players have interdependent services, is motivated by the problems faced
in planning and coordinating largescale infrastructures, e.g., restoring
electricity and gas to residents after a natural disaster or providing medical
care in a crisis when different agencies are responsible for the delivery of
staff, equipment, and medicine. We undertake a gametheoretic analysis of this
setting and in particular consider the issues of welfare maximization,
computing best responses, Nash dynamics, and existence and computation of Nash
equilibria.

We consider Maxmin Share (MmS) allocations of items both in the case where
items are goods (positive utility) and when they are chores (negative utility).
We show that fair allocations of goods and chores have some fundamental
connections but differences as well. We prove that like in the case for goods,
an MmS allocation does not need to exist for chores and computing an MmS
allocation  if it exists  is strongly NPhard. In view of these nonexistence
and complexity results, we present a polynomialtime 2approximation algorithm
for MmS fairness for chores. We then introduce a new fairness concept called
optimal MmS that represents the best possible allocation in terms of MmS that
is guaranteed to exist. For both goods and chores, we use connections to
parallel machine scheduling to give (1) an exponentialtime exact algorithm and
(2) a polynomialtime approximation scheme for computing an optimal MmS
allocation when the number of agents is fixed.

There is both much optimism and pessimism around artificial intelligence (AI)
today. The optimists are investing millions of dollars, and even in some cases
billions of dollars into AI. The pessimists, on the other hand, predict that AI
will end many things: jobs, warfare, and even the human race. Both the
optimists and the pessimists often appeal to the idea of a technological
singularity, a point in time where machine intelligence starts to run away, and
a new, more intelligent species starts to inhabit the earth. If the optimists
are right, this will be a moment that fundamentally changes our economy and our
society. If the pessimists are right, this will be a moment that also
fundamentally changes our economy and our society. It is therefore very
worthwhile spending some time deciding if either of them might be right.

Sequential allocation is a simple and attractive mechanism for the allocation
of indivisible goods. Agents take turns, according to a policy, to pick items.
Sequential allocation is guaranteed to return an allocation which is efficient
but may not have an optimal social welfare. We consider therefore the relation
between welfare and efficiency. We study the (computational) questions of what
welfare is possible or necessary depending on the choice of policy. We also
consider a novel control problem in which the chair chooses a policy to improve
social welfare.

Sometime in the future we will have to deal with the impact of AI's being
mistaken for humans. For this reason, I propose that any autonomous system
should be designed so that it is unlikely to be mistaken for anything besides
an autonomous sysem, and should identify itself at the start of any interaction
with another agent.

We study computational problems for two popular parliamentary voting
procedures: the amendment procedure and the successive procedure. While finding
successful manipulations or agenda controls is tractable for both procedures,
our realworld experimental results indicate that most elections cannot be
manipulated by a few voters and agenda control is typically impossible. If the
voter preferences are incomplete, then finding which alternatives can possibly
win is NPhard for both procedures. Whilst deciding if an alternative
necessarily wins is coNPhard for the amendment procedure, it is
polynomialtime solvable for the successive one.

We consider the discrete assignment problem in which agents express ordinal
preferences over objects and these objects are allocated to the agents in a
fair manner. We use the stochastic dominance relation between fractional or
randomized allocations to systematically define varying notions of
proportionality and envyfreeness for discrete assignments. The computational
complexity of checking whether a fair assignment exists is studied for these
fairness notions. We also characterize the conditions under which a fair
assignment is guaranteed to exist. For a number of fairness concepts,
polynomialtime algorithms are presented to check whether a fair assignment
exists. Our algorithmic results also extend to the case of unequal entitlements
of agents. Our NPhardness result, which holds for several variants of
envyfreeness, answers an open question posed by Bouveret, Endriss, and Lang
(ECAI 2010). We also propose fairness concepts that always suggest a nonempty
set of assignments with meaningful fairness properties. Among these concepts,
optimal proportionality and optimal weak proportionality appear to be desirable
fairness concepts.

The probabilistic serial (PS) rule is a prominent randomized rule for
assigning indivisible goods to agents. Although it is well known for its good
fairness and welfare properties, it is not strategyproof. In view of this, we
address several fundamental questions regarding equilibria under PS. Firstly,
we show that Nash deviations under the PS rule can cycle. Despite the
possibilities of cycles, we prove that a pure Nash equilibrium is guaranteed to
exist under the PS rule. We then show that verifying whether a given profile is
a pure Nash equilibrium is coNPcomplete, and computing a pure Nash equilibrium
is NPhard. For two agents, we present a lineartime algorithm to compute a
pure Nash equilibrium which yields the same assignment as the truthful profile.
Finally, we conduct experiments to evaluate the quality of the equilibria that
exist under the PS rule, finding that the vast majority of pure Nash equilibria
yield social welfare that is at least that of the truthful profile.

We discuss how to generate singled peaked votes uniformly from the Impartial
Culture model.

We study an online model of fair division designed to capture features of a
real world charity problem. We consider two simple mechanisms for this model in
which agents simply declare what items they like. We analyse several axiomatic
properties of these mechanisms like strategyproofness and envyfreeness.
Finally, we perform a competitive analysis and compute the price of anarchy.

The probabilistic serial (PS) rule is one of the most prominent randomized
rules for the assignment problem. It is wellknown for its superior fairness
and welfare properties. However, PS is not immune to manipulative behaviour by
the agents. We initiate the study of the computational complexity of an agent
manipulating the PS rule. We show that computing an expected utility better
response is NP hard. On the other hand, we present a polynomialtime algorithm
to compute a lexicographic best response. For the case of two agents, we show
that even an expected utility best response can be computed in polynomial time.
Our result for the case of two agents relies on an interesting connection with
sequential allocation of discrete objects.

Multiwinner voting rules based on approval ballots have received increased
attention in recent years. In particular Satisfaction Approval Voting (SAV) and
its variants have been proposed. In this note, we show that the winning set can
be determined in polynomial time for two prominent and natural variants of SAV.
We thank Arkadii Slinko for suggesting these problems in a talk at the Workshop
on Challenges in Algorithmic Social Choice, Bad Belzig, October 11, 2014.

A simple mechanism for allocating indivisible resources is sequential
allocation in which agents take turns to pick items. We focus on possible and
necessary allocation problems, checking whether allocations of a given form
occur in some or all mechanisms for several commonly used classes of sequential
allocation mechanisms. In particular, we consider whether a given agent
receives a given item, a set of items, or a subset of items for five natural
classes of sequential allocation mechanisms: balanced, recursively balanced,
balanced alternating, strictly alternating and all policies. We identify
characterizations of allocations produced balanced, recursively balanced,
balanced alternating policies and strictly alternating policies respectively,
which extend the wellknown characterization by Brams and King [2005] for
policies without restrictions. In addition, we examine the computational
complexity of possible and necessary allocation problems for these classes.

We propose and evaluate a number of solutions to the problem of calculating
the cost to serve each location in a singlevehicle transport setting. Such
cost to serve analysis has application both strategically and operationally in
transportation. The problem is formally given by the traveling salesperson game
(TSG), a cooperative total utility game in which agents correspond to locations
in a traveling salesperson problem (TSP). The cost to serve a location is an
allocated portion of the cost of an optimal tour. The Shapley value is one of
the most important normative division schemes in cooperative games, giving a
principled and fair allocation both for the TSG and more generally. We consider
a number of direct and samplingbased procedures for calculating the Shapley
value, and present the first proof that approximating the Shapley value of the
TSG within a constant factor is NPhard. Treating the Shapley value as an ideal
baseline allocation, we then develop six proxies for that value which are
relatively easy to compute. We perform an experimental evaluation using
Synthetic Euclidean games as well as games derived from realworld tours
calculated for fastmoving consumer goods scenarios. Our experiments show that
several computationally tractable allocation techniques correspond to good
proxies for the Shapley value.