164 lines
5.2 KiB
Python
164 lines
5.2 KiB
Python
"""Property-based tests for v3 correlation-aware clustering.
|
|
|
|
Feature: math-core-v3-engine
|
|
|
|
Uses Hypothesis to validate correctness properties of the v3 clustering
|
|
layer: effective evidence count n_eff is bounded by cluster size, and
|
|
cluster LLR is clamped to [-2.5, 2.5].
|
|
|
|
Validates: Requirements 4.2, 4.3, 4.4, 4.5, 21.4
|
|
"""
|
|
from __future__ import annotations
|
|
|
|
from hypothesis import given, settings
|
|
from hypothesis import strategies as st
|
|
|
|
from services.aggregation.worker import (
|
|
compute_cluster_llr,
|
|
compute_n_eff,
|
|
)
|
|
|
|
# ---------------------------------------------------------------------------
|
|
# Hypothesis strategies
|
|
# ---------------------------------------------------------------------------
|
|
|
|
# LLR values for testing
|
|
llr_values = st.floats(min_value=-5.0, max_value=5.0, allow_nan=False, allow_infinity=False)
|
|
llr_lists = st.lists(llr_values, min_size=1, max_size=20)
|
|
|
|
# Correlation values
|
|
rho_values = st.floats(min_value=0.0, max_value=1.0, allow_nan=False, allow_infinity=False)
|
|
|
|
|
|
def _symmetric_correlation_matrix(n: int) -> st.SearchStrategy[list[list[float]]]:
|
|
"""Generate an NxN symmetric correlation matrix with values in [0, 1].
|
|
|
|
Diagonal is 1.0, off-diagonal entries are symmetric rho in [0, 1].
|
|
"""
|
|
if n <= 1:
|
|
return st.just([[1.0]])
|
|
|
|
# Generate upper-triangle entries (n*(n-1)/2 values)
|
|
n_pairs = n * (n - 1) // 2
|
|
upper_triangle = st.lists(rho_values, min_size=n_pairs, max_size=n_pairs)
|
|
|
|
@st.composite
|
|
def build_matrix(draw: st.DrawFn) -> list[list[float]]:
|
|
entries = draw(upper_triangle)
|
|
matrix = [[0.0] * n for _ in range(n)]
|
|
idx = 0
|
|
for i in range(n):
|
|
matrix[i][i] = 1.0
|
|
for j in range(i + 1, n):
|
|
matrix[i][j] = entries[idx]
|
|
matrix[j][i] = entries[idx]
|
|
idx += 1
|
|
return matrix
|
|
|
|
return build_matrix()
|
|
|
|
|
|
# n_eff positive floats for property 6
|
|
n_eff_values = st.floats(min_value=0.1, max_value=20.0, allow_nan=False, allow_infinity=False)
|
|
|
|
|
|
# ---------------------------------------------------------------------------
|
|
# Property 5: Effective evidence count n_eff is bounded by cluster size
|
|
# Feature: math-core-v3-engine, Property 5: Effective evidence count n_eff is bounded by cluster size
|
|
# Validates: Requirements 4.2, 4.3, 21.4
|
|
# ---------------------------------------------------------------------------
|
|
|
|
|
|
@settings(max_examples=100)
|
|
@given(llrs=llr_lists)
|
|
def test_property_5_n_eff_bounded_by_cluster_size_default_correlations(
|
|
llrs: list[float],
|
|
) -> None:
|
|
"""Property 5: n_eff is bounded by cluster size (default correlations).
|
|
|
|
For any cluster of N signals using default pairwise correlations (rho=0.80),
|
|
the computed n_eff SHALL satisfy 0 < n_eff <= N.
|
|
|
|
**Validates: Requirements 4.2, 4.3**
|
|
"""
|
|
n = len(llrs)
|
|
n_eff = compute_n_eff(llrs)
|
|
|
|
assert n_eff > 0.0, f"n_eff={n_eff} must be positive"
|
|
assert n_eff <= n + 1e-9, f"n_eff={n_eff} exceeds cluster size N={n}"
|
|
|
|
|
|
@settings(max_examples=100)
|
|
@given(
|
|
data=st.data(),
|
|
llrs=st.lists(llr_values, min_size=2, max_size=10),
|
|
)
|
|
def test_property_5_n_eff_bounded_with_explicit_correlations(
|
|
data: st.DataObject,
|
|
llrs: list[float],
|
|
) -> None:
|
|
"""Property 5: n_eff is bounded by cluster size (explicit correlation matrix).
|
|
|
|
For any cluster of N signals with a symmetric NxN correlation matrix
|
|
with values in [0, 1], the computed n_eff SHALL satisfy 0 < n_eff <= N.
|
|
|
|
**Validates: Requirements 4.2, 4.3, 21.4**
|
|
"""
|
|
n = len(llrs)
|
|
corr_matrix = data.draw(_symmetric_correlation_matrix(n))
|
|
|
|
n_eff = compute_n_eff(llrs, correlations=corr_matrix)
|
|
|
|
assert n_eff > 0.0, f"n_eff={n_eff} must be positive"
|
|
assert n_eff <= n + 1e-9, f"n_eff={n_eff} exceeds cluster size N={n}"
|
|
|
|
|
|
# ---------------------------------------------------------------------------
|
|
# Property 6: Cluster LLR is clamped to [-2.5, 2.5]
|
|
# Feature: math-core-v3-engine, Property 6: Cluster LLR is clamped to [-2.5, 2.5]
|
|
# Validates: Requirements 4.4, 4.5
|
|
# ---------------------------------------------------------------------------
|
|
|
|
|
|
@settings(max_examples=100)
|
|
@given(
|
|
llrs=llr_lists,
|
|
n_eff=n_eff_values,
|
|
)
|
|
def test_property_6_cluster_llr_clamped(
|
|
llrs: list[float],
|
|
n_eff: float,
|
|
) -> None:
|
|
"""Property 6: Cluster LLR is clamped to [-2.5, 2.5].
|
|
|
|
For any cluster configuration with any number of signals and any LLR values,
|
|
the computed cluster LLR_c SHALL be in [-2.5, 2.5].
|
|
|
|
**Validates: Requirements 4.4, 4.5**
|
|
"""
|
|
cluster_llr = compute_cluster_llr(llrs, n_eff)
|
|
|
|
assert -2.5 <= cluster_llr <= 2.5, (
|
|
f"cluster_llr={cluster_llr} out of [-2.5, 2.5]"
|
|
)
|
|
|
|
|
|
@settings(max_examples=100)
|
|
@given(llrs=llr_lists)
|
|
def test_property_6_cluster_llr_clamped_with_computed_n_eff(
|
|
llrs: list[float],
|
|
) -> None:
|
|
"""Property 6: Cluster LLR is clamped when using computed n_eff.
|
|
|
|
End-to-end: compute n_eff from the LLRs, then compute cluster LLR.
|
|
The result SHALL still be in [-2.5, 2.5].
|
|
|
|
**Validates: Requirements 4.4, 4.5**
|
|
"""
|
|
n_eff = compute_n_eff(llrs)
|
|
cluster_llr = compute_cluster_llr(llrs, n_eff)
|
|
|
|
assert -2.5 <= cluster_llr <= 2.5, (
|
|
f"cluster_llr={cluster_llr} out of [-2.5, 2.5]"
|
|
)
|