Shield Layer & Memory-efficient Loss

The two top-level entry points of PiShield.

build_shield_layer

shield_layer

Top-level entry point for building Shield Layers.

A Shield Layer is a differentiable layer that corrects a model's outputs so that they are guaranteed to satisfy a given set of requirements (constraints), regardless of the input. This module exposes :func:build_shield_layer, which dispatches to the appropriate backend (linear, QFLRA, or propositional) based on the requirements, and :func:detect_requirements_type, which infers the requirement type from a requirements file.

build_shield_layer

build_shield_layer(num_variables: int, requirements_filepath: str, ordering_choice: str = 'given', custom_ordering: List = None, requirements_type='auto')

Build a Shield Layer from the given requirements.

Selects and constructs the appropriate Shield Layer backend (linear, QFLRA, or propositional) for the supplied requirements. The returned layer is differentiable and can be used at both inference and training time to correct a model's outputs so that they satisfy the requirements.

Parameters:

Name	Type	Description	Default
num_variables	int	Total number of variables (e.g. labels or features, depending on the task), matching the dimension of the tensors that are to be corrected by the layer.	required
requirements_filepath	str	Path to a .txt file containing the requirements.	required
ordering_choice	str	How to order the variables when applying corrections. One of 'given', 'random', or a custom ordering implemented by the user. If 'given', the ordering is read from requirements_filepath when available, otherwise the ascending order of the variables is used. If 'random', a random ordering of the variables is used.	'given'
custom_ordering	List	An explicit ordering of the variables (only used by the propositional backend). Defaults to None.	None
requirements_type		One of 'auto', 'linear', 'propositional', or 'qflra'. If 'auto', the appropriate backend is detected from the contents of requirements_filepath via :func:detect_requirements_type.	'auto'

Returns:

Type	Description
	A Shield Layer instance (LinearConstraintLayer, QFLRAConstraintLayer,
	or PropositionalConstraintLayer) that corrects model outputs to
	satisfy the requirements.

Raises:

Type	Description
Exception	If requirements_type is not one of the recognised values.

Example

layer = build_shield_layer( ... num_variables=5, ... requirements_filepath='requirements.txt', ... ) corrected = layer(model_output) # corrected satisfies the requirements

Source code in pishield/shield_layer.py

def build_shield_layer(num_variables: int,
                       requirements_filepath: str,
                       ordering_choice: str = 'given',
                       custom_ordering: List = None,
                       requirements_type='auto'):
    """Build a Shield Layer from the given requirements.

    Selects and constructs the appropriate Shield Layer backend (linear, QFLRA,
    or propositional) for the supplied requirements. The returned layer is
    differentiable and can be used at both inference and training time to correct
    a model's outputs so that they satisfy the requirements.

    Args:
        num_variables: Total number of variables (e.g. labels or features,
            depending on the task), matching the dimension of the tensors that
            are to be corrected by the layer.
        requirements_filepath: Path to a ``.txt`` file containing the requirements.
        ordering_choice: How to order the variables when applying corrections.
            One of ``'given'``, ``'random'``, or a custom ordering implemented by
            the user. If ``'given'``, the ordering is read from
            ``requirements_filepath`` when available, otherwise the ascending
            order of the variables is used. If ``'random'``, a random ordering of
            the variables is used.
        custom_ordering: An explicit ordering of the variables (only used by the
            propositional backend). Defaults to None.
        requirements_type: One of ``'auto'``, ``'linear'``, ``'propositional'``,
            or ``'qflra'``. If ``'auto'``, the appropriate backend is detected
            from the contents of ``requirements_filepath`` via
            :func:`detect_requirements_type`.

    Returns:
        A Shield Layer instance (``LinearConstraintLayer``, ``QFLRAConstraintLayer``,
        or ``PropositionalConstraintLayer``) that corrects model outputs to
        satisfy the requirements.

    Raises:
        Exception: If ``requirements_type`` is not one of the recognised values.

    Example:
        >>> layer = build_shield_layer(
        ...     num_variables=5,
        ...     requirements_filepath='requirements.txt',
        ... )
        >>> corrected = layer(model_output)  # corrected satisfies the requirements
    """

    if requirements_type == 'linear':
        return LinearConstraintLayer(num_variables, requirements_filepath, ordering_choice)
    elif requirements_type == 'qflra':
        return QFLRAConstraintLayer(num_variables, requirements_filepath, ordering_choice)
    elif requirements_type == 'propositional':
        return PropositionalConstraintLayer(num_variables, requirements_filepath, ordering_choice, custom_ordering=custom_ordering)
    elif requirements_type == 'auto':
        detected_requirements_type = detect_requirements_type(requirements_filepath)
        return build_shield_layer(num_variables, requirements_filepath, ordering_choice, custom_ordering=custom_ordering,
                                  requirements_type=detected_requirements_type)
    else:
        raise Exception('Unknown requirements type!')

detect_requirements_type

detect_requirements_type(requirements_filepath: str) -> str

Infer the requirement type from the contents of a requirements file.

Scans the file and classifies it as 'propositional', 'qflra', or 'linear' based on the tokens it contains (see inline comments for the exact detection rules).

Parameters:

Name	Type	Description	Default
requirements_filepath	str	Path to a .txt file containing the requirements.	required

Returns:

Type	Description
str	The detected requirement type as one of 'propositional', 'qflra',
str	or 'linear', or None if no requirement type could be detected.

Source code in pishield/shield_layer.py

def detect_requirements_type(requirements_filepath: str) -> str:
    """Infer the requirement type from the contents of a requirements file.

    Scans the file and classifies it as ``'propositional'``, ``'qflra'``, or
    ``'linear'`` based on the tokens it contains (see inline comments for the
    exact detection rules).

    Args:
        requirements_filepath: Path to a ``.txt`` file containing the requirements.

    Returns:
        The detected requirement type as one of ``'propositional'``, ``'qflra'``,
        or ``'linear'``, or None if no requirement type could be detected.
    """
    # Propositional requirements can be written either as Horn rules ('head :- body') or as
    # disjunctive clauses ('y_0 or not y_1'); both are accepted by the propositional parser.
    # The detection order matters: a ':-' token unambiguously marks a propositional Horn rule.
    # Otherwise, QFLRA and linear requirements both contain inequality signs, so we distinguish
    # them by the boolean operators ('or'/'neg') that only QFLRA uses. A clause-style
    # propositional requirement also uses 'or' but, unlike QFLRA, has no inequality sign.
    inequality_signs = ['>=', '>', '<=', '<']
    with open(requirements_filepath, 'r') as f:
        for line in f:
            line = line.strip()
            if not line or 'ordering' in line:
                continue
            tokens = line.split()
            if ':-' in tokens:
                print('Using auto mode ::: Detected propositional requirements!')
                return 'propositional'
            has_inequality = any(sign in line for sign in inequality_signs)
            has_boolean_op = 'or' in tokens or 'neg' in tokens
            if has_inequality:
                detected = 'qflra' if has_boolean_op else 'linear'
                print(f'Using auto mode ::: Detected {detected.upper() if detected == "qflra" else detected} requirements!')
                return detected
            if has_boolean_op:
                print('Using auto mode ::: Detected propositional requirements!')
                return 'propositional'
    return None

build_shield_loss

shield_loss

Top-level entry point for building the Memory-efficient Loss.

The Memory-efficient Loss is an additional loss term that encourages (but, unlike a Shield Layer, does not guarantee) requirement satisfaction at training time, using t-norms. It is a memory-efficient t-norm loss inspired by Logic Tensor Networks (LTN). This module exposes :func:build_shield_loss, which builds it.

build_shield_loss

build_shield_loss(num_variables: int, requirements_filepath: str, tnorm_choice: str = 'godel', requirements_type='propositional')

Build a Memory-efficient Loss from the given requirements.

Constructs a loss term that penalises violations of the requirements during training, using the chosen t-norm to measure satisfaction. The Memory-efficient Loss is a memory-efficient t-norm loss inspired by Logic Tensor Networks (LTN).

Parameters:

Name	Type	Description	Default
num_variables	int	Total number of variables (e.g. labels or features, depending on the task), matching the dimension of the tensors that are scored by the loss.	required
requirements_filepath	str	Path to a .txt file containing the requirements.	required
tnorm_choice	str	The t-norm used to compute requirement satisfaction. One of 'product', 'godel', or 'lukasiewicz'. Defaults to 'godel'.	'godel'
requirements_type		The requirement type. Only 'propositional' is currently supported.	'propositional'

Returns:

Type	Description
	A ShieldLoss instance (the Memory-efficient Loss) that computes the
	requirement-satisfaction loss.

Raises:

Type	Description
Exception	If requirements_type is not 'propositional'.

Example

loss_fn = build_shield_loss( ... num_variables=5, ... requirements_filepath='requirements.txt', ... tnorm_choice='product', ... ) penalty = loss_fn(model_output)

Source code in pishield/shield_loss.py

def build_shield_loss(num_variables: int,
                       requirements_filepath: str,
                       tnorm_choice: str = 'godel',
                       requirements_type='propositional'):
    """Build a Memory-efficient Loss from the given requirements.

    Constructs a loss term that penalises violations of the requirements during
    training, using the chosen t-norm to measure satisfaction. The Memory-efficient
    Loss is a memory-efficient t-norm loss inspired by Logic Tensor Networks (LTN).

    Args:
        num_variables: Total number of variables (e.g. labels or features,
            depending on the task), matching the dimension of the tensors that
            are scored by the loss.
        requirements_filepath: Path to a ``.txt`` file containing the requirements.
        tnorm_choice: The t-norm used to compute requirement satisfaction. One of
            ``'product'``, ``'godel'``, or ``'lukasiewicz'``. Defaults to ``'godel'``.
        requirements_type: The requirement type. Only ``'propositional'`` is
            currently supported.

    Returns:
        A ``ShieldLoss`` instance (the Memory-efficient Loss) that computes the
        requirement-satisfaction loss.

    Raises:
        Exception: If ``requirements_type`` is not ``'propositional'``.

    Example:
        >>> loss_fn = build_shield_loss(
        ...     num_variables=5,
        ...     requirements_filepath='requirements.txt',
        ...     tnorm_choice='product',
        ... )
        >>> penalty = loss_fn(model_output)
    """

    if requirements_type == 'propositional':
        return ShieldLoss(num_variables, requirements_filepath, tnorm_choice)
    else:
        raise Exception('Unknown requirements type!')