Docs

Development Guide

Guide for developing, debugging, and verifying ZeroProofML models.

Development Setup

Clone and Install

git clone https://github.com/domezsolt/zeroproofml.git
cd zeroproofml

python -m venv .venv
source .venv/bin/activate  # Windows: .venv\Scripts\activate

pip install -e ".[dev,torch]"

Run Tests

# All tests
pytest

# Specific module
pytest tests/scm/

# With coverage
pytest --cov=zeroproof --cov-report=html

# Fast (skip slow tests)
pytest -m "not slow"

Projective Training Internals

Tuple Lifecycle

Understanding how ⟨N,D⟩ tuples flow through training:

1. Encoding

from zeroproof.autodiff.projective import encode

# Finite: x → ⟨x, 1⟩
sample = encode(scm_real(3.14))
assert sample.numerator == 3.14
assert sample.denominator == 1.0

# Bottom: ⊥ → ⟨1, 0⟩
bottom_sample = encode(scm_bottom())
assert bottom_sample.denominator == 0.0

2. Detached Renormalization

from zeroproof.autodiff.projective import renormalize

# Prevent gradients leaking through norm
N, D = renormalize(N, D, gamma=1e-9)

# Equivalent to:
# S = stop_gradient(√(N² + D²) + γ)
# N', D' = N/S, D/S

3. Gradient Flow

Autograd runs on the renormalized tuples. Losses should use decoded values after renormalization:

# ✅ Correct
N, D = renormalize(N, D)
decoded = decode(N, D)
loss = mse(decoded, targets)

# ❌ Wrong (biases tuple scale)
decoded = decode(N, D)  # Before renorm
loss = mse(decoded, targets)
N, D = renormalize(N, D)

4. Decoding

from zeroproof.autodiff.projective import decode

# Inference: strict threshold
decoded = decode(sample, tau=1e-6)

Denominator Anchoring

For finite-target regression, anchor denominators near 1:

# Bias toward finite chart
Q = 1.0 + delta_Q  # delta_Q learned
P, Q = renormalize(P, Q)

# This prevents drift to tiny-but-nonzero D values
# that amplify decoded ratios

Minimal Training Skeleton

from zeroproof.autodiff.projective import encode, renormalize, decode

# Forward
N, D = model(x)  # Model outputs projective tuple
N, D = renormalize(N, D, gamma=1e-9)

# Decode for loss
decoded = decode(N, D, tau=1e-4)
loss = loss_fn(decoded, targets)

# Backward
loss.backward()
optimizer.step()

Debug Logging

Python Logging

import logging

logging.basicConfig(level=logging.INFO)
logging.getLogger("zeroproof").setLevel(logging.DEBUG)

Per-Step Metrics

Capture training metrics with log_hook:

import json
from pathlib import Path
from zeroproof.training import TrainingConfig

log_path = Path("runs/metrics.jsonl")
log_path.parent.mkdir(parents=True, exist_ok=True)

def log_hook(metrics):
    with log_path.open("a") as f:
        f.write(json.dumps(metrics) + "\n")

config = TrainingConfig(log_hook=log_hook)

Available metrics:

  • loss: Total training loss
  • coverage: Fraction of non-⊥ predictions
  • epoch: Current epoch
  • step: Global step count

Debugging ⊥ Propagation

Inspect bottom masks:

from zeroproof.layers import SCMRationalLayer

layer = SCMRationalLayer(3, 2)
output, bottom_mask = layer(x)

print(f"Bottom rate: {bottom_mask.float().mean():.3f}")
print(f"Bottom indices: {bottom_mask.nonzero().squeeze()}")

Log payload and mask:

# For vectorized ops
result, mask = scm_div_torch(N, D, N_mask, D_mask)

logger.debug(f"Payload: {result}")
logger.debug(f"Mask: {mask}")
logger.debug(f"Coverage: {(~mask).float().mean():.3f}")

Verification

SCM Semantics

Verify meadow axioms hold:

from zeroproof.scm.ops import scm_add, scm_mul, scm_div
from zeroproof.scm.value import scm_real, scm_bottom

# Absorption
x = scm_real(5.0)
b = scm_bottom()

assert scm_add(x, b).is_bottom
assert scm_mul(x, b).is_bottom

# Total inverse
assert scm_div(x, scm_real(0.0)).is_bottom

# Identity
assert scm_add(x, scm_real(0.0)).value == 5.0
assert scm_mul(x, scm_real(1.0)).value == 5.0

Gradient Policy Verification

from zeroproof.autodiff.policies import apply_policy, GradientPolicy

# CLAMP zeroes ⊥ gradients
grad = apply_policy(gradient=2.0, is_bottom=True, policy=GradientPolicy.CLAMP)
assert grad == 0.0

# PROJECT masks ⊥ paths
grad = apply_policy(gradient=2.0, is_bottom=True, policy=GradientPolicy.PROJECT)
assert grad == 0.0

# PASSTHROUGH preserves
grad = apply_policy(gradient=2.0, is_bottom=True, policy=GradientPolicy.PASSTHROUGH)
assert grad == 2.0

Coverage Verification

Test coverage on held-out data:

from zeroproof.losses.coverage import coverage_metric

model.eval()
with torch.no_grad():
    _, bottom_mask, _ = model(test_data)
    coverage = coverage_metric(bottom_mask)

    assert coverage >= 0.95, f"Coverage too low: {coverage:.3f}"

Common Issues

High ⊥ Rate During Training

Symptoms: Coverage drops below 50%

Debug steps:

  1. Check target lifting:

    Y_n, Y_d = lift_targets(targets)
print(f"Singular targets: {(Y_d.abs() < 1e-3).sum()}")

  2. Verify margin loss is active:

    loss_margin = margin_loss(D, tau_train=1e-4)
print(f"Margin loss: {loss_margin.item():.6f}")

  3. Increase rejection loss weight:

    loss_fn = SCMTrainingLoss(lambda_rejection=0.1)  # Was 0.01

NaN in Gradients

Symptoms: loss.backward() produces NaN

Debug steps:

  1. Check renormalization:

    # Ensure gamma > 0
N, D = renormalize(N, D, gamma=1e-9)

  2. Verify gradient policy:

    with gradient_policy(GradientPolicy.PROJECT):
    loss.backward()

  3. Enable gradient clipping:

    torch.nn.utils.clip_grad_norm_(model.parameters(), max_norm=1.0)

Inconsistent Signs

Symptoms: +∞ and -∞ predictions unstable

Debug steps:

  1. Enable sign consistency loss:

    loss_sign = sign_consistency_loss(N, D, Y_n, Y_d, tau_sing=1e-3)

  2. Check weak sign operator:

    from zeroproof.scm.sign import weak_sign

signs = weak_sign(values, mask, tau_sign=1e-6)

  3. Verify singular targets are correctly lifted

Testing Patterns

Unit Test Structure

import pytest
import torch
from zeroproof.layers import SCMRationalLayer

class TestSCMRational:
    def test_finite_inputs(self):
        layer = SCMRationalLayer(3, 2)
        x = torch.randn(32, 10)
        output, bottom_mask = layer(x)

        assert output.shape == (32, 1)
        assert bottom_mask.shape == (32, 1)
        assert not bottom_mask.all()  # Not all bottom

    def test_singular_inputs(self):
        layer = SCMRationalLayer(3, 2)
        x = torch.zeros(32, 10)  # Might trigger ⊥
        output, bottom_mask = layer(x)

        # Verify bottom propagation
        if bottom_mask.any():
            assert torch.isnan(output[bottom_mask]).all()

Integration Tests

def test_end_to_end_training():
    # Setup
    model = create_model()
    optimizer = torch.optim.Adam(model.parameters())
    loss_fn = SCMTrainingLoss()

    # Generate data
    x = torch.linspace(-1, 1, 100).unsqueeze(-1)
    y = 1.0 / (x + 0.1)  # Has singularity

    # Train
    for epoch in range(10):
        N, D = model(x)
        loss = loss_fn((N, D), lift_targets(y))
        loss.backward()
        optimizer.step()

    # Verify
    model.eval()
    with torch.no_grad():
        N, D = model(x)
        decoded, bottom, gap = strict_inference(N, D)
        coverage = (~bottom & ~gap).float().mean()

        assert coverage > 0.8

Contribution Guidelines

Code Style

# Format
black zeroproof/ tests/

# Lint
flake8 zeroproof/

# Type check
mypy zeroproof/

Pre-Commit Hooks

pip install pre-commit
pre-commit install

Pull Requests

  1. Branch from main
  2. Add tests for new features
  3. Update documentation
  4. Ensure CI passes
  5. Request review

Next Steps