<jupyter_start><jupyter_text>Training a selector with scikit-learn<jupyter_code># Hyperparameter

EMBEDDING_PATH = "sv-comp-embed.jsonl" # Set this path to the embedding file generated by run_batch_embed.py
LABEL_PATH     = "labels.jsonl" # Set this path to the label file generated by script/parse_svcomp_results.py
C = 10 # The default regularization parameter used by Logistic Regression<jupyter_output><empty_output><jupyter_text>Load the dataset for Embedding training<jupyter_code>from cst_transform.utils import EmbeddingLoader

data_loader = EmbeddingLoader(EMBEDDING_PATH, LABEL_PATH)

print("Datasets are available for the following tools: %s" % list(data_loader.tools))<jupyter_output>Datasets are available for the following tools: ['Pinaka', 'VeriAbs', 'Dartagnan', 'Korn', 'PeSCo', 'BRICK', 'symbiotic', 'ULTIMATE Automizer', 'CPAchecker', 'ESBMC', 'SMACK', 'DIVINE', 'CBMC', 'Lazy-CSeq', 'ULTIMATE Kojak', 'ULTIMATE Taipan', 'gazer-theta', '2LS', 'PredatorHP', 'Goblint']<jupyter_text>Train a single hardness model for CPAchecker<jupyter_code>from sklearn.model_selection import train_test_split
from sklearn.linear_model import LogisticRegression

X, y = data_loader("CPAchecker")

X_train, X_test, y_train, y_test = train_test_split(X, y, test_size = 0.1, random_state = 42)

# Train logistic regression classifier
model = LogisticRegression(C = C, max_iter = 10_000)
model.fit(X_train, y_train)

print("The hardness model achieved an accuracy of %f%%" % (100 * model.score(X_test, y_test)))
# Is CPAchecker likely to solve verification task "sv-benchmarks/c/floats-cdfpl/newton_1_4.i"?
# SVCOMP result: verdict: false, tool-output: false (unreach-call), time: 40s

import numpy as np

TASK_PATH = "sv-benchmarks/c/floats-cdfpl/newton_1_4.i"

task_embedding = data_loader.embedding(TASK_PATH)
prediction     = model.predict_proba(task_embedding[np.newaxis, :])[0, 1]

accept_str = "likely" if prediction > 0.5 else "unlikely"

print("CPAchecker is %s to solve the task %s (Conf: %.2f%%)" % (accept_str, TASK_PATH, 100 * prediction))<jupyter_output>CPAchecker is likely to solve the task sv-benchmarks/c/floats-cdfpl/newton_1_4.i (Conf: 70.19%)<jupyter_text>Training a complete selector with scikit learn<jupyter_code># Selector for CBMC, CPAchecker, ESBMC, Symbiotic, Ultimate Automizer

from tqdm import trange
from cst_transform.utils import group_stratified_split
from sklearn.linear_model import LogisticRegression

# Dataset
tools = ["CBMC", "CPAchecker", "ESBMC", "symbiotic", "ULTIMATE Automizer"]
X, Y, groups = data_loader(*tools, return_groups = True) # groups assigns every example to a specific group (e.g. array-examples)

# Split in train test (Stratified according verification task groups)
Xtrain, Xtest, Ytrain, Ytest = group_stratified_split(groups, X, Y, ratio = 0.1)

# Train logistic regression models
models = []
prediction = []

for train_index in trange(Ytrain.shape[1]):
    model = LogisticRegression(C = C, max_iter = 10_000)
    model.fit(Xtrain, Ytrain[:, train_index])
    models.append(model)
    prediction.append(model.predict_proba(Xtest)[:, 1])

prediction = np.vstack(prediction).transpose()

# Calculating the oracle score
selection      = prediction.argmax(axis = 1)
ohe_selection  = np.zeros((selection.shape[0], prediction.shape[1]))
ohe_selection[np.arange(selection.size), selection] = 1

selection_score = (ohe_selection * Ytest).max(axis = 1).sum()
oracle_score    = Ytest.max(axis = 1).sum()
selection_dist  = ohe_selection.mean(axis = 0)

print("The selector achieves the best possible prediction in %.2f%% of all cases" % (100*(selection_score / oracle_score)))

print("The selector chooses tools with the following distribution:")
for i, tool in enumerate(tools):
    print("%s: %.2f%%" % (tool, 100 * selection_dist[i]))<jupyter_output>100%|█████████████████████████████████████████████████████████████████████████████████████| 5/5 [00:00<00:00,  5.68it/s]<jupyter_text>Save the new selector to a directory<jupyter_code>import os
import json
import joblib

SELECTOR_DIRECTORY = "../data/new_selector/" # The directory referenced by run_selector.py
SELECTOR_NAME      = "base_selector"


if not os.path.exists(SELECTOR_DIRECTORY):
    os.makedirs(SELECTOR_DIRECTORY)

selector_config = {}

for i, tool in enumerate(tools):
    model = models[i]
    save_path = "%s_%s.jbl" % (SELECTOR_NAME, tool)
    joblib.dump(model, os.path.join(SELECTOR_DIRECTORY, save_path))
    selector_config[tool] = save_path

# Setup selector config
selector_config = {
    "name": SELECTOR_NAME,
    "description": "",
    "embedding"  : "tools", # Name of used pretrained model for embedding (Default: tools)
    "checkpoints": selector_config
}

with open(os.path.join(SELECTOR_DIRECTORY, "config.json"), "w") as o:
    json.dump(selector_config, o, indent = 4)<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.1347942939838743, 'fraction_numerical': 0.01571221831713872, 'mean_word_length': 5.9411764705882355, 'pattern_counts': {'":': 3, '<': 19, '<?xml version=': 0, '>': 19, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '5', 'dir': 'jupyter-structured-clean-dedup', 'id': '403873', 'license': 'Apache-2.0', 'n_tokens_mistral': 1794, 'n_tokens_neox': 1676, 'n_words': 416, 'path': 'train_selector.ipynb', 'repo_name': 'skanav/cst_transform', 'size': '4837'}