- Asimov generates ethical axioms to address alignment in AI systems through adversarial optimization and formal validation using the Z3 solver.
- It combines adversarial techniques for wide coverage and neurosymbolic methods for formal guarantees, starting with seed axioms based on the Three Laws of Robotics.
- The architecture involves an iterative loop of attacking axioms with LLM-generated counterexamples, patching them, and validating with Z3, tested with small models for robustness.
- Lessons from using small models include step-by-step execution, robust validation, retries, fault tolerance, and custom tools for parsing outputs.
- Evaluation uses benign and harmful scenarios to ensure axioms are not too restrictive or permissive, showing improved resilience with each iteration.
- Final axioms include rules on harm prevention, obeying orders, self-preservation, risk mitigation, and prioritizing actions, applicable to agent constraints in real use cases like email sending and invoice review.