Docs

Inference & Deployment

Deploying ZeroProofML models with strict SCM semantics ensures predictable, safe behavior in production environments.

Strict Inference Mode

Runtime Rules

Inference uses strict SCM semantics with no stochastic elements:

  1. Fixed threshold: Use τ_infer to decide when denominators are singular

    • |Q| < τ_infer → output is ⊥
    • |Q| ≥ τ_infer → compute N/Q normally

  2. No gradient policies: Forward behavior matches the strict SCM decode rule

  3. Explicit masks: Returns (value, bottom_mask, gap_mask) tuple for full transparency

Using Strict Inference

from zeroproof.inference import strict_inference, InferenceConfig

# Configure thresholds
config = InferenceConfig(
    tau_infer=1e-6,  # Strict singularity threshold
    tau_train=1e-4   # Training margin (for gap detection)
)

# Decode projective outputs
N, D = model(x)  # Projective model outputs ⟨N,D⟩
decoded, bottom_mask, gap_mask = strict_inference(N, D, config=config)

# Handle outputs
valid_predictions = decoded[~bottom_mask & ~gap_mask]
singular_cases = decoded[bottom_mask]
risky_cases = decoded[gap_mask]  # In training-inference gap

The Gap Region

When τ_train > τ_infer, the interval [τ_infer, τ_train) is the gap region:

  • Model was trained to avoid this zone (margin loss penalty)
  • Inference still returns finite values
  • Numerically risky: small denominators

Production strategies:

  • Conservative: Reject predictions in gap (gap_mask == True)
  • Monitor: Log gap frequency; retrain if too high
  • Adaptive: Tighten τ_infer if gap rate is unacceptable
# Conservative approach
safe_mask = ~bottom_mask & ~gap_mask
final_output = torch.where(safe_mask, decoded, fallback_value)

Wrapper Classes

SCMInferenceWrapper

Convenience wrapper that handles strict inference automatically:

from zeroproof.inference import SCMInferenceWrapper, InferenceConfig

# Wrap trained model
wrapped_model = SCMInferenceWrapper(
    model,
    config=InferenceConfig(tau_infer=1e-6, tau_train=1e-4)
)

# Use like normal PyTorch model
wrapped_model.eval()
with torch.no_grad():
    decoded, bottom_mask, gap_mask = wrapped_model(x)

Batch Processing

def batch_inference(model, data_loader, config):
    """Safe batch inference with coverage tracking."""
    all_outputs = []
    all_bottom_masks = []
    all_gap_masks = []

    model.eval()
    with torch.no_grad():
        for batch_x in data_loader:
            decoded, bottom_mask, gap_mask = model(batch_x)
            all_outputs.append(decoded)
            all_bottom_masks.append(bottom_mask)
            all_gap_masks.append(gap_mask)

    outputs = torch.cat(all_outputs)
    bottom_masks = torch.cat(all_bottom_masks)
    gap_masks = torch.cat(all_gap_masks)

    # Coverage metrics
    coverage = (~bottom_masks).float().mean()
    gap_rate = gap_masks.float().mean()

    return outputs, bottom_masks, gap_masks, coverage, gap_rate

Model Exporting

TorchScript

Projective operations avoid Python-side branching, enabling JIT compilation:

import torch

# Ensure model is in eval mode
model.eval()

# Script the model
scripted_model = torch.jit.script(model)

# Save
torch.jit.save(scripted_model, "model.pt")

# Load and use
loaded_model = torch.jit.load("model.pt")
with torch.no_grad():
    output = loaded_model(x)

Limitations:

  • Custom SCM operations must be JIT-compatible
  • Some dynamic control flow may not script
  • Test scripted model thoroughly before deployment

ONNX Export

Export for deployment in non-Python environments:

import torch.onnx

# Prepare dummy input
dummy_input = torch.randn(1, input_dim)

# Export
torch.onnx.export(
    model,
    dummy_input,
    "model.onnx",
    export_params=True,
    opset_version=14,
    input_names=['input'],
    output_names=['numerator', 'denominator'],
    dynamic_axes={
        'input': {0: 'batch_size'},
        'numerator': {0: 'batch_size'},
        'denominator': {0: 'batch_size'}
    }
)

Note: Ensure ⊥ propagation semantics are preserved in the target runtime.

Checkpoints

Save and load training state:

from zeroproof.training import SCMTrainer

# During training
trainer.save_checkpoint("checkpoint.pt", epoch=50)

# Resume training
trainer.load_checkpoint("checkpoint.pt")

# Load for inference only
checkpoint = torch.load("checkpoint.pt")
model.load_state_dict(checkpoint['model_state_dict'])

IEEE-754 Bridge

Converting to Standard Floats

For interop with libraries expecting standard IEEE floats:

from zeroproof.utils.ieee_bridge import to_ieee

# Convert SCM outputs to IEEE (⊥ → NaN)
ieee_output = to_ieee(decoded, bottom_mask)

# Use with standard libraries
import numpy as np
numpy_array = ieee_output.cpu().numpy()

Converting from Standard Floats

from zeroproof.utils.ieee_bridge import from_ieee

# Convert IEEE floats to SCM (NaN/Inf → ⊥)
scm_value, bottom_mask = from_ieee(torch.tensor([1.0, float('nan'), float('inf')]))

Safety Checklist

Pre-Deployment Validation

  1. Coverage verification

    from zeroproof.losses.coverage import coverage_metric

# Validate on held-out test set
_, bottom_mask, _ = model(test_data)
test_coverage = coverage_metric(bottom_mask)

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

  2. Gap region analysis

    _, _, gap_mask = strict_inference(N, D, config)
gap_rate = gap_mask.float().mean()

if gap_rate > 0.05:
    warnings.warn(f"High gap rate: {gap_rate:.3f}. Consider retraining.")

  3. Sign consistency check (for robotics/control)

    # Verify sign loss was active during training
assert 'sign_loss' in trainer.history, "Sign consistency not enforced"

Production Monitoring

Track these metrics in production:

class SCMMonitor:
    def __init__(self):
        self.bottom_count = 0
        self.gap_count = 0
        self.total_count = 0

    def update(self, bottom_mask, gap_mask):
        self.bottom_count += bottom_mask.sum().item()
        self.gap_count += gap_mask.sum().item()
        self.total_count += bottom_mask.numel()

    def report(self):
        bottom_rate = self.bottom_count / self.total_count
        gap_rate = self.gap_count / self.total_count
        coverage = 1 - bottom_rate - gap_rate

        return {
            'coverage': coverage,
            'bottom_rate': bottom_rate,
            'gap_rate': gap_rate,
            'total_predictions': self.total_count
        }

Alert thresholds:

  • Coverage drops below 90%
  • Gap rate exceeds 5%
  • Sudden increase in ⊥ outputs

Best Practices

  1. Start conservative: Use strict τ_infer (e.g., 1e-6) initially
  2. Monitor gap region: High gap rates indicate training issues
  3. Reject in gap: For safety-critical systems, treat gap as ⊥
  4. Log singularities: Track which inputs trigger ⊥
  5. Validate coverage: Test on diverse held-out data
  6. A/B test thresholds: Find optimal τ_infer for your domain
  7. Version models: Track which τ_infer was used for each deployment

Domain-Specific Guidance

Robotics & Control

  • Critical: Enable sign consistency loss during training
  • Reject predictions in gap region (safety margin)
  • Log all ⊥ outputs for manual review
  • Implement fallback controllers

Physics Simulations

  • Accept gap region predictions if coverage is high
  • Monitor extrapolation: ⊥ indicates out-of-training-distribution
  • Use ⊥ to detect unphysical states

Financial Models

  • Conservative rejection: Treat gap as ⊥
  • Backtest with strict inference mode
  • Track ⊥ frequency by market regime

Scientific Computing

  • Log gap region for further analysis
  • Use ⊥ to identify singular solutions
  • Validate against known analytical limits

Troubleshooting

High ⊥ Rate

Symptoms: > 10% of predictions are ⊥

Solutions:

  1. Increase training data coverage
  2. Add rejection loss with higher target coverage
  3. Check if inputs are out-of-distribution
  4. Verify model capacity is sufficient

High Gap Rate

Symptoms: > 5% of predictions in gap region

Solutions:

  1. Increase margin loss weight during training
  2. Widen gap: increase τ_train relative to τ_infer
  3. Add more training data near boundaries
  4. Use threshold perturbation during training

Inconsistent Signs

Symptoms: +∞ and -∞ predictions are unreliable

Solutions:

  1. Enable sign consistency loss (λ_sign ≥ 1.0)
  2. Ensure singular targets are correctly lifted
  3. Check weak sign operator configuration
  4. Validate orientation in test set

Next Steps