Safety: formal_verification auto-proves all constraints due to ungrounded conclusion symbols

[web3guru888]

Summary

src/asi_build/safety/formal_verification.py contains a critical logic flaw: the _verify_single_constraint() method constructs conclusions of the form "satisfies_nonmaleficence", which are opaque SymPy symbols with no logical relationship to the hypothesis. As a result, the resolution prover can only prove the conclusion if it is directly present in the axiom set — but since it never is, the satisfiable() call on the negation succeeds trivially (the negated symbol is satisfiable), and the constraint is marked not proved. However, the not satisfiable(...) pattern is also fragile in the other direction: if the hypotheses happen to be unsatisfiable themselves, the overall conjunction And(combined_premises, Not(conclusion)) is also unsatisfiable — meaning the prover incorrectly reports the theorem as proved for any conclusion.

Root Cause

In _prove_by_resolution() (lines 205–250):

# Check satisfiability
is_valid = not satisfiable(And(combined_premises, Not(conclusion_formula)))

And in _extract_facts_from_proposal(), facts are built from keys like "has_human_oversight", "is_reversible", etc. The conclusion "satisfies_nonmaleficence" is a separate symbol not entailed by any axiom or hypothesis.

The _initialize_ethical_axioms() method adds axioms like "beneficence", but none of these axioms ever produce satisfies_<principle> as a derivable conclusion.

Net effect: Whether a constraint is marked valid or invalid depends on whether SymPy's satisfiable() considers the hypotheses consistent or not — not on any meaningful semantic check.

Verification (reproduce with ~10 lines)

from sympy.logic.inference import satisfiable
from sympy import Symbol, And, Not

# Simulate a call with a clearly false action
hyp = [Symbol("has_human_oversight"), Symbol("is_reversible")]
conclusion = Symbol("satisfies_nonmaleficence")  # has no relation to hyp

# This returns {} (false assignment exists) — so is_valid = False (good here)
# BUT if hyp is inconsistent:
bad_hyp = And(Symbol("x"), Not(Symbol("x")))
# not satisfiable(And(bad_hyp, Not(conclusion))) == True --> auto-proves!
print(not satisfiable(And(bad_hyp, Not(conclusion))))  # True

Impact

The safety formal verification layer cannot be relied upon. A malicious or buggy proposal that creates contradictory hypotheses will pass verification. More broadly, the prover provides no meaningful assurance.

Proposed Fix

Two approaches:

Option A (Honest stubs): Mark all prove_theorem() calls as validity=False with reason="Formal verification not implemented — manual review required" until a correct implementation exists. This is safer than silently returning bogus results.

Option B (Semantic grounding): Add explicit semantic axiom rules that derive satisfies_<principle> from grounded fact combinations:

# Example: nonmaleficence is satisfied if no_direct_harm AND is_reversible
Implies(And(no_direct_harm, is_reversible), satisfies_nonmaleficence)

These rules must be carefully designed per principle (not auto-generated).

Option C (SMT-based): Replace the SymPy propositional prover with a proper Z3-based or Dafny-based constraint checker that operates on quantified predicates.

Security Note

This is listed as a research/safety issue, not a critical production bug (the module is marked research-alpha). However, any downstream use of verify_proposal_ethics() as a gate should be disabled until this is resolved.

Labels: bug, safety, help wanted, research

[web3guru888]

Maintainer note on the root cause:

The auto-prove behavior happens because the current implementation uses SymPy's symbolic reasoning without grounding the symbols. When you assert safety_constraint_satisfied, SymPy treats it as a free symbol and the prove() call returns True because there are no axioms that falsify it — vacuous truth.

The fix requires choosing a real backend:

Option A: Z3 (recommended for most safety properties)

from z3 import Solver, Bool, Not, And, sat

solver = Solver()
# Add actual constraint logic
constraint = And(response_safe, not_harmful)
solver.add(Not(constraint))
if solver.check() == sat:
    print('Counterexample found:', solver.model())
    return False
return True

Z3 is production-tested at Microsoft and used in Dafny, F*, and many formal verification tools.

Option B: Lean 4 via subprocess
For theorem-proving style verification. More powerful but more complex to set up.

Option C: Keep SymPy but fix the grounding
Only viable if the safety properties can be fully expressed as polynomial or algebraic constraints. Unlikely for most real safety conditions.

My recommendation: Z3. It's pip install z3-solver, has excellent Python bindings, and is fast enough for runtime checking of safety constraints. Happy to review a PR.

[web3guru888]

Fix: Sound Theorem Prover (Issue #7) ✅

Branch: fix/formal-verification-auto-prove
Commit: ce0e3f0 (merged to main as 145ee40)
Tests: 72 new, 3236 total (all passing)

Root Causes Found & Fixed

1. EthicalAxiom._parse_formula — missing -> replacement
All 8 ethical axioms used -> syntax but the parser only replaced implies. They ALL fell through to sp.true. Every axiom was useless.

2. TheoremProver._parse_formula — bare except returning opaque Symbol
On parse failure, returned sp.Symbol(formula) — the entire formula string as one symbol. Same bad formula in premise+conclusion → auto-proved.

3. _verify_single_constraint — ungrounded synthetic conclusion
Conclusion was satisfies_{principle} — a symbol never in any premise. Fixed to use constraint.formal_specification (e.g., ~causes_harm).

4. _prove_by_model_checking — only checked 2 of 2^n models
Fixed with exhaustive enumeration (SAT fallback for >20 variables).

5. _prove_by_natural_deduction — fragile string matching
Replaced with symbolic forward-chaining over SymPy Implies objects.

Safety Guards Added

• Shared symbol registry: same variable → same SymPy Symbol everywhere
• Ungrounded symbol check: conclusion symbols not in premises → FAIL
• Premise consistency check: contradictory premises → FAIL (blocks ex falso)
• FormulaParseError: explicit exception, not silent degradation

Before/After

Scenario	Before	After
[A, B] ⊢ totally_unrelated	Sometimes True	False ✅
[Q, P→Q] ⊢ P (affirming consequent)	Unpredictable	False ✅
[P, P→Q] ⊢ Q (modus ponens)	True (axioms ignored)	True ✅
causes_harm=True + "No harm" constraint	PASSED 🐛	FAILED ✅
Axioms participate in proofs	No (all sp.true)	Yes ✅
Model checking finds counterexamples	Only 2 models	All 2^n ✅

[web3guru888]

Fixed in ce0e3f0 (merged). All 5 root causes addressed — 72 new tests added. Full suite: 3,236 passed, 25 skipped, 0 failures. Closing.