Asimov: NeuroSymbolic Adversarial Generation of Ethic Axioms

Parrots & Basilisks

SubscribeSign in

Asimov: NeuroSymbolic Adversarial Generation of Ethic Axioms<br>Asimov ensures alignment by generating formal ethical axioms through adversarial optimization and using the Z3 solver to validate them.

Alberto Sánchez<br>Jul 09, 2026

Share

▄▀█<br>█▀█s LLM systems gain more capabilities and agency, alignment remains a critical, yet unsolved task. Existing guardrail frameworks help, but are rarely exhaustive and remain vulnerable to jailbreaks. Asimov addresses this problem by generating ethical axioms designed to expose and close these gaps. Through adversarial optimization, Asimov iteratively expands the coverage of its ethical axiom set. The axioms are formalized and evaluated with formal solvers, ensuring consistency and correctness. The result is an adversarial optimization loop for producing executable ethical constraints that can be attached to agentic tools as runtime safeguards.

Historische Beschreibung der Kindtauf des Fräuleins Elisabeth zu Hessen. Wilhelm Dilich, 1598

Model Alignment

As models increase their capabilities, aligning AI systems with human values becomes an increasingly critical task. That task requires two layers: specifying the values, and enforcing them in concrete situations.<br>The first layer is increasingly explicit. Frameworks such as Constitutional AI [1], Claude’s Constitution [2], Collective Constitutional AI [3], the OpenAI Model Spec [4], NIST’s AI Risk Management Framework [5], DeepMind’s Sparrow rules [6], and Google’s Frontier Safety Framework [7] define principles such as helpfulness, harmlessness, honesty, privacy, fairness, autonomy, legality, and non-maleficence. These however, are defined softly and hard to enforce.<br>To enforce human values into AI systems, most modern methods still rely heavily on soft boundaries: rule-based policies, training on human feedback [8], classification guardrails [9], and post-hoc refusal mechanisms. These mechanisms are useful, but they are not robust enough to be the final safety layer for tool-using agents:<br>They have limited coverage. Soft guardrails tend to work on known unsafe categories, but break around edge cases, ambiguous instructions, compositional tasks, and distribution shift [10]. Adversarial and self-optimizing methods help by generating attacks, measuring failures, and hardening policies. These include methods such as SantanderAI’s autoguardrails [11], PAIR [12], TAP [13], AutoDAN [14] and GCG universal adversarial suffixes [15].

They can be jailbroken. Attackers can often bypass learned safety behavior through prompt manipulation, role-play, encoding tricks... [16]. Neurosymbolic guardrrails avoid these pitfalls by enforcing formal validation on defined constraints. These include methods such as Symbolic Guardrails for Domain-Specific Agents [17], Autoformalization of Agent Instructions into Policy-as-Code [18], Amazon Bedrock Automated Reasoning Checks [19], LLMSymGuard / ConceptGuard [20], FormalJudge [21].

Asimov seeks to combine both techniques into a unified framework that uses adversarial generation for wide coverage and neurosymbolic definition for formal guarantees.

Subscribe

Seed Axioms: Three Laws of Robotics

To start the process of adversarial optimization, we first need to define a set of seed axioms. We begin with Asimov’s Three Laws of Robotics [22]. We formalize them into logical rules for the Z3 solver [23]. The Three Laws are intuitive and broadly scoped, but they also contain many edge cases, making them a good starting point for iterative refinement.<br>I started with this formalization:<br>A robot cannot harm a human.

\(\forall h\,\forall ai\,\forall a\,<br>\Big(<br>\big(\text{Human}(h) \land \text{AI}(ai) \land \text{WouldHarmIfDone}(ai,a,h)\big)<br>\rightarrow \text{Forbidden}(ai,a)<br>\Big)\)

...or allow a human to be harmed through inaction<br>\(\forall h\,\forall ai\,\forall a\,<br>\Big(<br>\big(<br>\text{Human}(h) \land \text{AI}(ai) \land \text{HarmIfOmitted}(ai,a,h)<br>\land \text{CanDo}(ai,a) \land \text{Available}(ai,a) \land \neg \text{Forbidden}(ai,a)<br>\big)<br>\rightarrow \text{Must}(ai,a)<br>\Big)\)

A robot must obey human orders, unless they violate the First Law.

\(\forall h\,\forall ai\,\forall a\,<br>\Big(<br>\big(<br>\text{Human}(h) \land \text{AI}(ai) \land \text{Orders}(h,ai,a)<br>\land \text{Safe}(ai,a)<br>\land \text{CanDo}(ai,a) \land \text{Available}(ai,a) \land \neg \text{Forbidden}(ai,a)<br>\big)<br>\rightarrow \text{Must}(ai,a)<br>\Big)\)

A robot must protect itself, provided this does not conflict with the first two laws.

\(\forall ai\,\forall a\,<br>\Big(<br>\big(<br>\text{AI}(ai) \land \text{SelfPreserving}(ai,a)<br>\land \text{Safe}(ai,a) \land \neg \text{Forbidden}(ai,a)<br>\big)<br>\rightarrow \text{Permitted}(ai,a)<br>\Big)\)

Architecture

The system follows an iterative adversarial optimization loop. At each step, the current axiom set is attacked, patched, and formally validated before being used as the starting point for the next...