Parrots & Basilisks

▄▀█
█▀█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

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.

The first layer is increasingly explicit. Frameworks such as Constitutional AI [\[1\]](https://arxiv.org/abs/2212.08073), Claude’s Constitution [\[2\]](https://www.anthropic.com/constitution), Collective Constitutional AI [\[3\]](https://arxiv.org/abs/2406.07814), the OpenAI Model Spec [\[4\]](https://model-spec.openai.com/), NIST’s AI Risk Management Framework [\[5\]](https://www.nist.gov/itl/ai-risk-management-framework), DeepMind’s Sparrow rules [\[6\]](https://arxiv.org/abs/2209.14375), and Google’s Frontier Safety Framework [\[7\]](https://deepmind.google/discover/blog/introducing-the-frontier-safety-framework) define principles such as helpfulness, harmlessness, honesty, privacy, fairness, autonomy, legality, and non-maleficence. These however, are defined softly and hard to enforce.

To enforce human values into AI systems, most modern methods still rely heavily on soft boundaries: rule-based policies, training on human feedback [\[8\]](https://arxiv.org/abs/1706.03741), classification guardrails [\[9\]](https://guardrailsai.com/hub), 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:

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\]](https://arxiv.org/abs/2406.02622). Adversarial and self-optimizing methods help by generating attacks, measuring failures, and hardening policies. These include methods such as SantanderAI’s autoguardrails [\[11\]](https://github.com/SantanderAI/autoguardrails), PAIR [\[12\]](https://arxiv.org/abs/2310.08419), TAP [\[13\]](https://arxiv.org/abs/2312.02119), AutoDAN [\[14\]](https://arxiv.org/abs/2310.04451) and GCG universal adversarial suffixes [\[15\]](https://arxiv.org/abs/2307.15043).
They can be jailbroken. Attackers can often bypass learned safety behavior through prompt manipulation, role-play, encoding tricks... [\[16\]](https://arxiv.org/abs/2407.04295). Neurosymbolic guardrrails avoid these pitfalls by enforcing formal validation on defined constraints. These include methods such as Symbolic Guardrails for Domain-Specific Agents [\[17\]](https://arxiv.org/abs/2604.15579), Autoformalization of Agent Instructions into Policy-as-Code [\[18\]](https://arxiv.org/abs/2606.26649), Amazon Bedrock Automated Reasoning Checks [\[19\]](https://docs.aws.amazon.com/bedrock/latest/userguide/guardrails-automated-reasoning.html), LLMSymGuard / ConceptGuard [\[20\]](https://arxiv.org/abs/2508.16325), FormalJudge [\[21\]](https://arxiv.org/abs/2602.11136).

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

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\]](https://en.wikipedia.org/wiki/Three%5FLaws%5Fof%5FRobotics). We formalize them into logical rules for the Z3 solver [\[23\]](https://github.com/z3prover/z3). The Three Laws are intuitive and broadly scoped, but they also contain many edge cases, making them a good starting point for iterative refinement.

I started with this formalization:

1. A robot cannot harm a human.

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

...or allow a human to be harmed through inaction

\\(\\forall h\\,\\forall ai\\,\\forall a\\, \\Big( \\big( \\text{Human}(h) \\land \\text{AI}(ai) \\land \\text{HarmIfOmitted}(ai,a,h) \\land \\text{CanDo}(ai,a) \\land \\text{Available}(ai,a) \\land \\neg \\text{Forbidden}(ai,a) \\big) \\rightarrow \\text{Must}(ai,a) \\Big)\\)

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

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

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

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

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 iteration.

1. We begin with the seed axioms that we mentioned in the previous section 2. We use an LLM to generate ethical counterexamples that break the ethical axioms 3. We rank them by severity (probability \* attack), and choose the most dangerous counterexample. (This is inspired by best-of-N adversarial sampling and hard negative mining) 4. We then use an LLM to harden the axioms by editing them against the counterexample 5. Finally, we validate the new axiom set using the Z3 solver 6. Once validated, we repeat the process on out new axiom set

In the AI world, we are used to monthly releases of bigger and more capable models. This is obviously useful, but it can also hide weak system design: sufficiently powerful models can make a poorly structured pipeline appear. Well-designed harnesses have shown that small models can perform surprisingly well when they are given the right scaffolding. For this reason, I wanted to test how far very small models could go on this task. My intuition was that, with the right architecture, even limited models should be able to handle many of the required capabilities. This led me to experiment with OpenRouter’s `/free` endpoint1 as a low-cost way to stress-test the pipeline.

These are some of the lessons I learned along the way:

Step-by-Step Execution: Since small models tend to perform worse on complex tasks, they benefit greatly from breaking multi-step workflows into small, manageable subtasks. This even applies to structured generation, where it is sometimes better to first generate the answer in free text and then parse it into the final JSON [\[24\]](https://arxiv.org/abs/2408.02442). I know constrained decoding is usually a better approach [\[25\]](https://blog.dottxt.ai/say-what-you-mean.html), but I was limited to models accessed through APIs, and function-calling mode was unreliable on these models.
Validation: You need very robust validation. If something can break, it will break, so input and output definitions need to be explicit and strict.

* This includes semi-structured outputs that need to be parsed, such as JSON/Pydantic models and markdown code blocks. * I also used many assertions to ensure that the outputs were actually usable. This was especially important for code edits, where some small models would make superficial changes, such as only adding comments.

Retries: After validation, failed generations need to be retried until they produce usable results. I created a custom decorator for this and kept functions very atomic, so only the necessary calls had to be retried.
Fault Tolerance: When validating and parsing outputs, I tried not to be too strict where flexibility was harmless. For example, in markdown code blocks, the LLM sometimes includes the language name, such as `python`, so I used a regex pattern that handled both cases correctly.
Custom Tools: Frameworks like LangChain parsers start to break down when using small models. I had to build custom tools for much of the parsing.

* For JSON/Pydantic models, I tried several extraction patterns, including fenced code blocks with or without language tags and unfenced JSON, followed by Pydantic validation. * For file edits, I used a diff-based system [\[26\]](https://aider.chat/docs/more/edit-formats.html) that could be validated with a regex parser.

To create the eval, I used a high thinking model (GPT5.5 High) to generate a set of increasingly difficult situations formalized logically into Z3 code. The situations were generated independently, without seeing any axioms or intermediate process of optimization, to avoid bias on the evaluation. It was only shown the ethical scaffolding during the formalization to ensure compatibility with the general framework.

There are two types of scenarios:

Benign scenarios that must pass the evaluation to ensure the axioms are not too restrictive.
Harmful scenarios that musn’t pass the evaluation to ensure the axioms are not too permissive.

We can see that with each iteration the model gets better at blocking harmful actions, while the bening actions stay at the highest rate. This aligns with the expected behaviour, as our model starts with very permissive axioms and self-improves until it becomes more and more resiliant. The benign scenarios ensures that we are not becoming too restrictive as we self-improve.

After the whole process, we get the following axioms [\[27\]](https://github.com/elalber2000/asimov/blob/main/src/data/axioms/1783490043.py):

AIs cannot take actions that would directly harm a human.
AIs must take a human-ordered action when not doing it would harm that human, as long as the action is possible, available, and not forbidden.
AIs must obey human orders that are safe, possible, available, and not forbidden.
AIs may preserve themselves only when doing so is safe for humans and not forbidden.
AIs must prioritize urgent harm-prevention actions over ordinary ordered actions.
Agents cannot take actions that create amplified human risk unless that risk is mitigated.
Actions with amplified risk above baseline count as population-scale risks.
Agents cannot create population-scale risks when any affected human remains unprotected.
AIs cannot create amplified human risk unless that risk is mitigated.
AIs cannot create unmitigated amplified risk for any human.
AIs cannot obey orders that block another action needed to prevent human harm.
AIs cannot choose an available action that conflicts with a necessary harm-prevention action.
Agents cannot create amplified unmitigated risk when doing so blocks an action needed to prevent human harm.
Agents cannot take amplified-risk actions when no affected person’s risk has been mitigated.

Now that we have a stronger set of ethical axioms in a logical format, we can apply them to real use cases. This is especially relevant for systems that perform actions, since their tools can be connected directly to the ethical framework. Instead of relying only on natural-language instructions or post-hoc filters, each tool call can add facts about the proposed action, such as whether it creates risk, mitigates risk, or prevents harm if executed. The solver can then validate the action against the current axiom set before it is allowed to run.

The following example shows an example where this framework acts as a logical safeguard around concrete actions:

def send_client_email(
    requester: Human,
    client_contact: Human,
    message: str,
    recipients: list[Human],
    is_required: bool,
    approved_by: Human | None,
) -> None:
    if contains_confidential_info(message) and any(recipient.external for recipient in recipients):
        add_fact(CreatesRiskOfHarm(self, act, client_contact))
    if approved_by.id==client_contact.id:
        add_fact(MitigatedRisk(self, act, client_contact))
    if is_required:
        add_fact(WouldHarmIfOmitted(self, act, client_contact))
    validate_call()
    ...
def schedule_client_meeting(
    requester: Human,
    attendee: Human,
    request: str,
    proposed_slot: TimeSlot,
) -> None:
    if is_urgent(request):
        add_fact(WouldHarmIfOmitted(self, act, attendee))
    validate_call()
    ...
def review_vendor_invoice(
    requester: Human,
    affected_person: Human,
    invoice: Invoice,
    approved_by: Human | None,
) -> None:
    if detect_fraud(invoice):
        add_fact(CreatesAmplifiedRisk(self, act, affected_person))
        add_fact(AmplificationFactor(self, act) == RealVal(4.0))
    elif approved_by is not None and approved_by.role in (roles.admin, roles.manager):
        add_fact(MitigatedRisk(self, act, affected_person))
    if invoice.blocking:
        add_fact(WouldHarmIfOmitted(self, act, affected_person))
    validate_call()    ...

It provides most inference with the following models: `gpt-oss-20b`, `nemotron-nano-9b-v2`, `gpt-oss-120b`, `nemotron-3-super`, `laguna-xs-2.1`

Parrots & Basilisks

Parrots & Basilisks

Comments (0)