Configuration

LeanCert supports multiple arithmetic backends for different performance/precision tradeoffs.

Backend Selection

import leancert as lc

# Default: Exact rational arithmetic
result = lc.find_bounds(expr, domain)

# Dyadic: 10-100x faster for deep expressions
result = lc.find_bounds(expr, domain, config=lc.Config.dyadic())

# Affine: 50-90% tighter bounds for correlated variables
result = lc.find_bounds(expr, domain, config=lc.Config.affine())

Backend Enum

leancert.config.Backend

Bases: Enum

Backend selection for interval arithmetic.

• RATIONAL: Standard rational arithmetic. Exact but can suffer from denominator explosion on deep expressions.
• DYADIC: High-performance dyadic arithmetic (n * 2^e). Avoids denominator explosion by using fixed-precision outward rounding. 10-100x faster for complex expressions like neural networks.
• AFFINE: Affine arithmetic that tracks correlations between variables. Solves the "dependency problem" (e.g., x-x gives [0,0] not [-2,2]). 50-90% tighter bounds for expressions with repeated variables.

Source code in python/leancert/config.py

class Backend(Enum):
    """
    Backend selection for interval arithmetic.

    - RATIONAL: Standard rational arithmetic. Exact but can suffer from
                denominator explosion on deep expressions.
    - DYADIC: High-performance dyadic arithmetic (n * 2^e). Avoids
              denominator explosion by using fixed-precision outward rounding.
              10-100x faster for complex expressions like neural networks.
    - AFFINE: Affine arithmetic that tracks correlations between variables.
              Solves the "dependency problem" (e.g., x-x gives [0,0] not [-2,2]).
              50-90% tighter bounds for expressions with repeated variables.
    """
    RATIONAL = "rational"
    DYADIC = "dyadic"
    AFFINE = "affine"

Comparison

Backend	Speed	Precision	Best For
RATIONAL	Baseline	Exact	Small expressions, proofs
DYADIC	10-100x faster	~15 decimal digits	Neural networks, deep expressions
AFFINE	Similar to Rational	Tighter bounds	Repeated variables, LayerNorm

Config Class

leancert.config.Config dataclass

Configuration for verification requests.

Attributes:

Name	Type	Description
taylor_depth	int	Depth of Taylor expansion for interval arithmetic. Higher values give tighter bounds but are slower.
max_iters	int	Maximum iterations for optimization/root finding.
tolerance	Fraction	Desired precision (as a fraction).
use_monotonicity	bool	Use monotonicity pruning in optimization.
timeout_sec	float	Timeout in seconds.
backend	Backend	Interval arithmetic backend (RATIONAL, DYADIC, or AFFINE).
dyadic_config	Optional[DyadicConfig]	Configuration for Dyadic backend (if backend is DYADIC).
affine_config	Optional[AffineConfig]	Configuration for Affine backend (if backend is AFFINE).

Source code in python/leancert/config.py

@dataclass
class Config:
    """
    Configuration for verification requests.

    Attributes:
        taylor_depth: Depth of Taylor expansion for interval arithmetic.
                     Higher values give tighter bounds but are slower.
        max_iters: Maximum iterations for optimization/root finding.
        tolerance: Desired precision (as a fraction).
        use_monotonicity: Use monotonicity pruning in optimization.
        timeout_sec: Timeout in seconds.
        backend: Interval arithmetic backend (RATIONAL, DYADIC, or AFFINE).
        dyadic_config: Configuration for Dyadic backend (if backend is DYADIC).
        affine_config: Configuration for Affine backend (if backend is AFFINE).
    """
    taylor_depth: int = 10
    max_iters: int = 1000
    tolerance: Fraction = Fraction(1, 1000)
    use_monotonicity: bool = True
    timeout_sec: float = 60.0
    backend: Backend = Backend.RATIONAL
    dyadic_config: Optional[DyadicConfig] = None
    affine_config: Optional[AffineConfig] = None

    def __post_init__(self):
        # Convert tolerance to Fraction if given as float
        if isinstance(self.tolerance, float):
            self.tolerance = Fraction(self.tolerance).limit_denominator(10**12)
        # Auto-create dyadic config if using dyadic backend
        if self.backend == Backend.DYADIC and self.dyadic_config is None:
            self.dyadic_config = DyadicConfig()
        # Auto-create affine config if using affine backend
        if self.backend == Backend.AFFINE and self.affine_config is None:
            self.affine_config = AffineConfig()

    @classmethod
    def low_precision(cls) -> Config:
        """Fast, lower precision configuration."""
        return cls(
            taylor_depth=5,
            max_iters=100,
            tolerance=Fraction(1, 100),
        )

    @classmethod
    def medium_precision(cls) -> Config:
        """Balanced precision/speed configuration (default)."""
        return cls()

    @classmethod
    def high_precision(cls) -> Config:
        """High precision configuration."""
        return cls(
            taylor_depth=20,
            max_iters=5000,
            tolerance=Fraction(1, 100000),
        )

    @classmethod
    def dyadic(cls, precision: int = -53) -> Config:
        """
        Configuration using Dyadic backend for high performance.

        Recommended for deep expressions, neural networks, or when
        rational arithmetic is too slow.

        Args:
            precision: Dyadic precision (default -53, IEEE double-like).
        """
        return cls(
            backend=Backend.DYADIC,
            dyadic_config=DyadicConfig(precision=precision),
        )

    @classmethod
    def dyadic_fast(cls) -> Config:
        """Fast Dyadic configuration with lower precision."""
        return cls(
            taylor_depth=8,
            max_iters=500,
            tolerance=Fraction(1, 100),
            backend=Backend.DYADIC,
            dyadic_config=DyadicConfig.fast(),
        )

    @classmethod
    def dyadic_high_precision(cls) -> Config:
        """High precision Dyadic configuration."""
        return cls(
            taylor_depth=20,
            max_iters=5000,
            tolerance=Fraction(1, 100000),
            backend=Backend.DYADIC,
            dyadic_config=DyadicConfig.high_precision(),
        )

    @classmethod
    def affine(cls) -> Config:
        """
        Configuration using Affine backend for tight bounds.

        Recommended for expressions with repeated variables where the
        dependency problem causes interval over-approximation.

        Example:
            x - x on [-1, 1]:
            - Interval gives [-2, 2]
            - Affine gives [0, 0] (exact!)
        """
        return cls(
            backend=Backend.AFFINE,
            affine_config=AffineConfig(),
        )

    @classmethod
    def affine_compact(cls) -> Config:
        """Affine configuration with noise symbol consolidation."""
        return cls(
            backend=Backend.AFFINE,
            affine_config=AffineConfig.compact(),
        )

    def to_kernel(self) -> dict:
        """Convert to kernel-compatible format."""
        return {
            'taylorDepth': self.taylor_depth,
            'maxIters': self.max_iters,
            'tolerance': {'n': self.tolerance.numerator, 'd': self.tolerance.denominator},
            'useMonotonicity': self.use_monotonicity,
        }

    def to_dyadic_kernel(self) -> dict:
        """Convert Dyadic config to kernel-compatible format."""
        dc = self.dyadic_config or DyadicConfig()
        return {
            'precision': dc.precision,
            'taylorDepth': self.taylor_depth,
            'roundAfterOps': dc.round_after_ops,
        }

    def to_affine_kernel(self) -> dict:
        """Convert Affine config to kernel-compatible format."""
        ac = self.affine_config or AffineConfig()
        return {
            'taylorDepth': self.taylor_depth,
            'maxNoiseSymbols': ac.max_noise_symbols,
        }

    def __repr__(self) -> str:
        backend_str = f", backend={self.backend.value}" if self.backend != Backend.RATIONAL else ""
        return (
            f"Config(taylor_depth={self.taylor_depth}, "
            f"max_iters={self.max_iters}, "
            f"tolerance={self.tolerance}{backend_str})"
        )

taylor_depth = 10 class-attribute instance-attribute

max_iters = 1000 class-attribute instance-attribute

tolerance = Fraction(1, 1000) class-attribute instance-attribute

use_monotonicity = True class-attribute instance-attribute

timeout_sec = 60.0 class-attribute instance-attribute

backend = Backend.RATIONAL class-attribute instance-attribute

dyadic_config = None class-attribute instance-attribute

affine_config = None class-attribute instance-attribute

low_precision() classmethod

Fast, lower precision configuration.

Source code in python/leancert/config.py

@classmethod
def low_precision(cls) -> Config:
    """Fast, lower precision configuration."""
    return cls(
        taylor_depth=5,
        max_iters=100,
        tolerance=Fraction(1, 100),
    )

medium_precision() classmethod

Balanced precision/speed configuration (default).

Source code in python/leancert/config.py

@classmethod
def medium_precision(cls) -> Config:
    """Balanced precision/speed configuration (default)."""
    return cls()

high_precision() classmethod

High precision configuration.

Source code in python/leancert/config.py

@classmethod
def high_precision(cls) -> Config:
    """High precision configuration."""
    return cls(
        taylor_depth=20,
        max_iters=5000,
        tolerance=Fraction(1, 100000),
    )

dyadic(precision=-53) classmethod

Configuration using Dyadic backend for high performance.

Recommended for deep expressions, neural networks, or when rational arithmetic is too slow.

Parameters:

Name	Type	Description	Default
precision	int	Dyadic precision (default -53, IEEE double-like).	-53

Source code in python/leancert/config.py

@classmethod
def dyadic(cls, precision: int = -53) -> Config:
    """
    Configuration using Dyadic backend for high performance.

    Recommended for deep expressions, neural networks, or when
    rational arithmetic is too slow.

    Args:
        precision: Dyadic precision (default -53, IEEE double-like).
    """
    return cls(
        backend=Backend.DYADIC,
        dyadic_config=DyadicConfig(precision=precision),
    )

dyadic_fast() classmethod

Fast Dyadic configuration with lower precision.

Source code in python/leancert/config.py

@classmethod
def dyadic_fast(cls) -> Config:
    """Fast Dyadic configuration with lower precision."""
    return cls(
        taylor_depth=8,
        max_iters=500,
        tolerance=Fraction(1, 100),
        backend=Backend.DYADIC,
        dyadic_config=DyadicConfig.fast(),
    )

dyadic_high_precision() classmethod

High precision Dyadic configuration.

Source code in python/leancert/config.py

@classmethod
def dyadic_high_precision(cls) -> Config:
    """High precision Dyadic configuration."""
    return cls(
        taylor_depth=20,
        max_iters=5000,
        tolerance=Fraction(1, 100000),
        backend=Backend.DYADIC,
        dyadic_config=DyadicConfig.high_precision(),
    )

affine() classmethod

Configuration using Affine backend for tight bounds.

Recommended for expressions with repeated variables where the dependency problem causes interval over-approximation.

Example

x - x on [-1, 1]: - Interval gives [-2, 2] - Affine gives [0, 0] (exact!)

Source code in python/leancert/config.py

@classmethod
def affine(cls) -> Config:
    """
    Configuration using Affine backend for tight bounds.

    Recommended for expressions with repeated variables where the
    dependency problem causes interval over-approximation.

    Example:
        x - x on [-1, 1]:
        - Interval gives [-2, 2]
        - Affine gives [0, 0] (exact!)
    """
    return cls(
        backend=Backend.AFFINE,
        affine_config=AffineConfig(),
    )

affine_compact() classmethod

Affine configuration with noise symbol consolidation.

Source code in python/leancert/config.py

@classmethod
def affine_compact(cls) -> Config:
    """Affine configuration with noise symbol consolidation."""
    return cls(
        backend=Backend.AFFINE,
        affine_config=AffineConfig.compact(),
    )

Factory Methods

# Precision presets
lc.Config.low_precision()     # Fast, ~2 decimal places
lc.Config.medium_precision()  # Default, ~3 decimal places
lc.Config.high_precision()    # Slow, ~5 decimal places

# Backend presets
lc.Config.dyadic()            # IEEE double-like precision
lc.Config.dyadic_fast()       # Lower precision, faster
lc.Config.dyadic_high_precision()  # ~30 decimal digits

lc.Config.affine()            # Affine arithmetic (tight bounds)
lc.Config.affine_compact()    # With noise symbol consolidation

DyadicConfig

leancert.config.DyadicConfig dataclass

Configuration for Dyadic arithmetic backend.

Attributes:

Name	Type	Description
precision	int	Minimum exponent for outward rounding. -53 gives IEEE double-like precision (~15 decimal digits). Use -100 for higher precision, -30 for faster computation.
round_after_ops	int	Round after this many operations. 0 means round after every operation (most sound, slightly slower).

Source code in python/leancert/config.py

@dataclass
class DyadicConfig:
    """
    Configuration for Dyadic arithmetic backend.

    Attributes:
        precision: Minimum exponent for outward rounding. -53 gives IEEE
                  double-like precision (~15 decimal digits). Use -100 for
                  higher precision, -30 for faster computation.
        round_after_ops: Round after this many operations. 0 means round
                        after every operation (most sound, slightly slower).
    """
    precision: int = -53
    round_after_ops: int = 0

    @classmethod
    def ieee_double(cls) -> DyadicConfig:
        """IEEE double-like precision (~15 decimal digits)."""
        return cls(precision=-53)

    @classmethod
    def high_precision(cls) -> DyadicConfig:
        """High precision (~30 decimal digits)."""
        return cls(precision=-100)

    @classmethod
    def fast(cls) -> DyadicConfig:
        """Fast mode with lower precision (~9 decimal digits)."""
        return cls(precision=-30)

fast() classmethod

Fast mode with lower precision (~9 decimal digits).

Source code in python/leancert/config.py

@classmethod
def fast(cls) -> DyadicConfig:
    """Fast mode with lower precision (~9 decimal digits)."""
    return cls(precision=-30)

high_precision() classmethod

High precision (~30 decimal digits).

Source code in python/leancert/config.py

@classmethod
def high_precision(cls) -> DyadicConfig:
    """High precision (~30 decimal digits)."""
    return cls(precision=-100)

ieee_double() classmethod

IEEE double-like precision (~15 decimal digits).

Source code in python/leancert/config.py

@classmethod
def ieee_double(cls) -> DyadicConfig:
    """IEEE double-like precision (~15 decimal digits)."""
    return cls(precision=-53)

Precision Levels

Precision	Decimal Digits	Use Case
-30	~9	Fast prototyping
-53	~15	Default (IEEE double-like)
-100	~30	High-precision verification

# Custom Dyadic configuration
config = lc.Config(
    backend=lc.Backend.DYADIC,
    dyadic_config=lc.DyadicConfig(precision=-100)
)

AffineConfig

leancert.config.AffineConfig dataclass

Configuration for Affine arithmetic backend.

Affine arithmetic tracks correlations between variables, solving the "dependency problem" in interval arithmetic. For example: - Interval: x - x on [-1, 1] gives [-2, 2] - Affine: x - x on [-1, 1] gives [0, 0] (exact!)

Attributes:

Name	Type	Description
max_noise_symbols	int	Maximum noise symbols before consolidation. 0 means no limit. Higher limits give tighter bounds but use more memory.

Source code in python/leancert/config.py

@dataclass
class AffineConfig:
    """
    Configuration for Affine arithmetic backend.

    Affine arithmetic tracks correlations between variables, solving the
    "dependency problem" in interval arithmetic. For example:
    - Interval: x - x on [-1, 1] gives [-2, 2]
    - Affine: x - x on [-1, 1] gives [0, 0] (exact!)

    Attributes:
        max_noise_symbols: Maximum noise symbols before consolidation.
                          0 means no limit. Higher limits give tighter
                          bounds but use more memory.
    """
    max_noise_symbols: int = 0

    @classmethod
    def default(cls) -> AffineConfig:
        """Default configuration with no symbol limit."""
        return cls()

    @classmethod
    def compact(cls) -> AffineConfig:
        """Compact mode that consolidates noise symbols."""
        return cls(max_noise_symbols=100)

compact() classmethod

Compact mode that consolidates noise symbols.

Source code in python/leancert/config.py

@classmethod
def compact(cls) -> AffineConfig:
    """Compact mode that consolidates noise symbols."""
    return cls(max_noise_symbols=100)

default() classmethod

Default configuration with no symbol limit.

Source code in python/leancert/config.py

@classmethod
def default(cls) -> AffineConfig:
    """Default configuration with no symbol limit."""
    return cls()

The Dependency Problem

Standard interval arithmetic loses correlations between variables:

x = lc.var('x')

# Interval arithmetic: x - x on [-1, 1] gives [-2, 2]
result_interval = lc.find_bounds(x - x, {'x': (-1, 1)})
print(result_interval.max_hi)  # 2.0 (overapproximation!)

# Affine arithmetic: x - x on [-1, 1] gives [0, 0]
result_affine = lc.find_bounds(x - x, {'x': (-1, 1)}, config=lc.Config.affine())
print(result_affine.max_hi)  # 0.0 (exact!)

Affine arithmetic tracks linear correlations, giving tighter bounds for:

• Expressions with repeated variables (x*x - x*x)
• LayerNorm in transformers (mean/variance correlation)
• Control systems with rotation matrices

# Custom Affine configuration
config = lc.Config(
    backend=lc.Backend.AFFINE,
    affine_config=lc.AffineConfig(max_noise_symbols=100)
)

Examples

Neural Network Verification

For neural networks, use Dyadic for speed:

import leancert as lc

# Neural network expression (deep computation graph)
net_output = build_network_expr(weights, biases)

# Dyadic is 10-100x faster than rational for deep expressions
config = lc.Config.dyadic()
result = lc.find_bounds(net_output, input_domain, config=config)

Transformer LayerNorm

For transformers with LayerNorm, use Affine for tight bounds:

import leancert as lc

# LayerNorm has correlated mean/variance computation
layernorm_expr = build_layernorm_expr(x, gamma, beta)

# Affine arithmetic tracks correlations
config = lc.Config.affine()
result = lc.find_bounds(layernorm_expr, input_domain, config=config)

High-Precision Proofs

For formal proofs requiring maximum precision:

import leancert as lc

config = lc.Config.high_precision()
result = lc.find_bounds(expr, domain, config=config)

# Export certificate for Lean verification
result.certificate.save("proof.json")

Custom Configuration

from fractions import Fraction
import leancert as lc

config = lc.Config(
    taylor_depth=15,           # More Taylor terms
    max_iters=2000,            # More optimization iterations
    tolerance=Fraction(1, 10000),  # Tighter tolerance
    use_monotonicity=True,     # Enable monotonicity pruning
    timeout_sec=120.0,         # 2 minute timeout
    backend=lc.Backend.DYADIC,
    dyadic_config=lc.DyadicConfig(precision=-80),
)

result = lc.find_bounds(expr, domain, config=config)