Provenance
AuthorsEnglert, Siebert, Ziegler
VenuearXiv
FunderNot found
MethodFormal proof
Summary

Lethal Autonomous Weapons promise to revolutionize warfare and raise a multitude of ethical and legal questions. It has thus been suggested to program values and principles of conduct (such as the Geneva Conventions) into the machines' control, thereby rendering them both physically and morally superior to human combatants. The paper employs mathematical logic and theoretical computer science to explore fundamental limitations to the moral behaviour of intelligent machines in a series of "Gedankenexperiments": Refining and sharpening variants of the Trolley Problem leads to the construction of an (admittedly artificial but) fully deterministic situation where a robot is presented with two choices: one morally clearly preferable over the other - yet, based on the undecidability of the Halting problem, it provably cannot decide algorithmically which one. These considerations have surprising implications to the question of responsibility and liability for an autonomous system's actions and lead to specific technical recommendations. Lethal autonomous systems (LASs) without an operator fall into a new legal limbo — being simultaneously object of producer misrepresentation and subject as an autonomous entity — which makes an untraceable, non-attributable LAS “an ideal tool to the perfect crime,” and the undecidability of the Halting problem could in an ironic twist be misconstrued to exculpate war crimes and other misconduct performed by AIs. The results thus “make a strong case” for demands by responsible scientists and politicians to ban autonomous weapons, and the best choice “is to never develop them in the first place.” However, LASs are developed then so should the following regulations: government-only ownership and operation of LASs with a fixed distinctive sign and unique ID, a registered legal custodian and type approval for every autonomous robot, mandatory formal methods of software verification (computer-checkable proofs of specification compliance), and tamper-proof data/event logging secured by asymmetric encryption.

Next Step

Closely regulate both the design of lethal autonomous systems and the question of attributability and accountability in case of maloperation, whether deliberate or erroneous.

Read paper ↗