| Summary: | Reduction of nuclear arms in a verifiable manner that is trusted by two or more parties is a hard but important problem. Nations and organisations that wish to engage in such arms control verification activities need to be able to design procedures and control mechanisms that let them compute pertinent degrees of belief. Crucially, they also will need methods for reliably assessing their confidence in such beliefs, in situations with little or no contextual data to apply data-driven learning techniques on. This motivates the investigation of alternative methods of modelling beliefs. This thesis will cover three key models: a probabilistic Bayesian Network (BN) model for an arms control inspection scenario; a dynamical system that models an arms race with dynamics reflecting verification activities; and mathematical games, which are used for understanding the design space of treaties that constrain inspection schedules. We extend our models beyond their conventional computational abilities, and encode uncertainty over variables and probabilities within the models. This thesis explores the techniques required to enable such computations and to use these to answer questions of interest to decision making. In doing so, we also show that these abstractions can mitigate against the risk that lack of prior data represents for modelling and analysis. A main contribution of the thesis is to not only develop such methods for dealing with uncertainty, but to also extend these models with external constraints that reflect beliefs, knowledge or assumptions. We extend BNs to constrained Bayesian Networks, and relax the requirement of declaring Real valued probabilities of events. This then enables us to analyse marginal probabilities of interest symbolically, or develop metrics that check for agreement in outputs between multiple different models, and even optimise such metrics over the uncertainty. Whereas Stochastical Optimisation and other utility based techniques would enable an analysis of likelihoods, this work employs Robust Optimisation. This means that we are assessing 'best case', 'worst case' or 'is this ever possible' events, which are important to our arms control verification domain. For dynamical systems, we are able to leave initial parameters of the model as unknown, and then compute an optimum inspection routine (based on any arbitrarily set metric) that holds true despite the uncertainty. This allows us to provide decision-support regarding the best timings for rationing out a limited number of inspections, and how such an inspection regime should be the optimal one to meet the desired metric. In game theory, we develop constrained symbolic games that include symbolic pay-offs, and for which we can find Nash Equilibria that vary as the symbolic terms change. This allows us to advise players on the best mix of strategies to consider as the uncertain pay-offs vary, to either optimise pay-offs, or the use of particular strategies. Eventually, we are able to combine our approaches into an all-encompassing, yet fine-grained, model. Such integration accomplishes modelling all aspects of an inspection process and the regime that may call such a process. Integration also accounts for the shortcomings individual mathematical techniques have that other techniques can overcome. Our tools encode models in a Satisfiability Modulo Theories (SMT) solver: SMT are powerful decision procedures for quantifier-free, first-order logic. Solving our problems using SMT enables us to assess the sensitivity and relative confidence we have in particular models, as well as optimise for variables of interest and test hypotheses even without full data. The practical difficulties lie in leveraging the SMT to work for our large mathematical models, when, normally, they can only be relied on for simple or small numbers of mathematical computations. Although the theory, formalisations and methodologies engineered here are not specific to this domain, we utilise a case study in nuclear arms control to evaluate our approach and to demonstrate the real world insights gained. We conclude that the increased analytical capabilities from combining mathematical modelling and SMT allows us to - in principle - support the design or assessment of future bilateral arms control instruments by applying them to models of interest.
|
|---|
