Training for General Output Properties¶

In this example, we train a small controller to follow a proportional control law while keeping both actions within [-0.1, 0.1] throughout a declared input box. We use PropertyModelWrapper to combine the task loss with a bound-based property loss.

First, we import the required functions.

In [ ]:

import torch
from torch.utils.data import DataLoader, TensorDataset

from CTRAIN.model_definitions import ControllerMLP
from CTRAIN.model_wrappers import PropertyModelWrapper
from CTRAIN.properties import Outputs, And, Box, PropertySpec

import torch from torch.utils.data import DataLoader, TensorDataset from CTRAIN.model_definitions import ControllerMLP from CTRAIN.model_wrappers import PropertyModelWrapper from CTRAIN.properties import Outputs, And, Box, PropertySpec

Now, we define the controller and sample training states. The targets are the actions of a proportional controller.

In [ ]:

model = ControllerMLP()
states = 2 * torch.rand(256, 2) - 1
targets = -0.05 * states
train_loader = DataLoader(TensorDataset(states, targets), batch_size=32, shuffle=True)

model = ControllerMLP() states = 2 * torch.rand(256, 2) - 1 targets = -0.05 * states train_loader = DataLoader(TensorDataset(states, targets), batch_size=32, shuffle=True)

We declare the output constraints and the input region on which they should hold. Outputs() refers symbolically to the model outputs; And requires every comparison to hold.

In [ ]:

y = Outputs()
property_spec = PropertySpec(
    "bounded_actions",
    And(y[0] >= -0.1, y[0] <= 0.1, y[1] >= -0.1, y[1] <= 0.1),
    [Box([-1.0, -1.0], [1.0, 1.0])],
)

y = Outputs() property_spec = PropertySpec( "bounded_actions", And(y[0] >= -0.1, y[0] <= 0.1, y[1] >= -0.1, y[1] <= 0.1), [Box([-1.0, -1.0], [1.0, 1.0])], )

Now, we wrap the model and start training. Mean squared error measures the control task, while CROWN-IBP bounds supply the property penalty. The first five epochs optimise only the task loss; the property weight then increases over 20 epochs.

In [ ]:

wrapped_model = PropertyModelWrapper(
    model=model,
    input_shape=(2,),
    properties=[property_spec],
    task_loss=torch.nn.MSELoss(),
    num_epochs=50,
    training_method="CROWN-IBP",
    property_weight=20.0,
    warm_up_epochs=5,
    weight_ramp_epochs=20,
    device="cpu",
)
wrapped_model.train_model(train_loader)

wrapped_model = PropertyModelWrapper( model=model, input_shape=(2,), properties=[property_spec], task_loss=torch.nn.MSELoss(), num_epochs=50, training_method="CROWN-IBP", property_weight=20.0, warm_up_epochs=5, weight_ramp_epochs=20, device="cpu", ) wrapped_model.train_model(train_loader)

Finally, we compute fresh bounds over the complete declared box. Certification concerns every input in that region, rather than only the sampled training states.

In [ ]:

report = wrapped_model.certify_properties(method="CROWN")
print("Whole domain certified:", report["certified"])

report = wrapped_model.certify_properties(method="CROWN") print("Whole domain certified:", report["certified"])

A low training loss does not by itself establish certification. The general-properties guide explains disjunctions, input refinement, fixed dynamics and complete verification.