LearningCore
Imports
open List;
open Tuple;
open Pair;
import Tensor (Vector);
Types
Functions
def read_csv (path : String) : {df : DataFrame | df_cols df ≥ 1 && df_rows df ≥ 0}
def target (1 df : DataFrame) (column : String) (temporal : Bool) (missing : Bool) : {
ds : Dataset | ds_rows ds = df_rows df
&&
(
ds_features ds = df_cols df - 1
&&
(
ds_target ds column = True
&&
(is_timeseries ds = temporal && (has_missing ds = missing && (coupled ds = False && independent_target ds = True)))
)
)
}
def target_at (1 df : DataFrame) (index : Int | index ≥ 0 && index < df_cols df) (temporal : Bool) (missing : Bool) : {
ds : Dataset | ds_rows ds = df_rows df
&&
(
ds_features ds = df_cols df - 1
&&
(is_timeseries ds = temporal && (has_missing ds = missing && (coupled ds = False && independent_target ds = True)))
)
}
def load (path : String) (temporal : Bool) (missing : Bool) : {
ds : Dataset | ds_features ds ≥ 0
&&
(
ds_rows ds ≥ 0
&&
(is_timeseries ds = temporal && (has_missing ds = missing && (coupled ds = False && independent_target ds = True)))
)
}
def create_dataset (rows : Int | rows ≥ 0) (features : Int | features ≥ 0) (bal : Bool) (temporal : Bool) (missing : Bool) : {
ds : Dataset | ds_rows ds = rows
&&
(
ds_features ds = features
&&
(
is_balanced ds = bal
&&
(is_timeseries ds = temporal && (has_missing ds = missing && (coupled ds = False && independent_target ds = True)))
)
)
}
def require_enough_data (1 ds : Dataset) : {d : Dataset | d = ds && ds_rows d > ds_features d * 10}
def columns (1 df : DataFrame) : List
def has_column (1 df : DataFrame) (column : String) : Bool
def n_columns (1 df : DataFrame) : {n : Int | n = df_cols df && n ≥ 0}
def n_rows (1 ds : Dataset) : {n : Int | n = ds_rows ds && n ≥ 0}
def n_features (1 ds : Dataset) : {n : Int | n = ds_features ds && n ≥ 0}
def balanced (1 ds : Dataset) : {b : Bool | b = is_balanced ds}
def is_nonempty (1 ds : Dataset) : {b : Bool | b = ds_rows ds > 0}
def is_splittable (1 ds : Dataset) : {b : Bool | b = ds_rows ds ≥ 2}
def is_multiclass (1 ds : Dataset) : {b : Bool | b = ds_classes ds ≥ 2}
def class_counts (1 ds : Dataset) : List
def split (1 ds : Dataset | ds_rows ds > ds_features ds * 10) (fraction : Float | 0.0 < fraction && fraction < 1.0) (shuffle : Bool) : {
p : Pair Dataset Dataset | ds_features (Pair_mk_fst p) = ds_features ds
&&
(
ds_features (Pair_mk_snd p) = ds_features ds
&&
(
ds_classes (Pair_mk_fst p) = ds_classes ds
&&
(
ds_classes (Pair_mk_snd p) = ds_classes ds
&&
(
is_timeseries (Pair_mk_fst p) = is_timeseries ds
&&
(
is_timeseries (Pair_mk_snd p) = is_timeseries ds
&&
(
has_missing (Pair_mk_fst p) = has_missing ds
&&
(
has_missing (Pair_mk_snd p) = has_missing ds
&&
(
coupled (Pair_mk_fst p) = coupled ds
&&
(
coupled (Pair_mk_snd p) = coupled ds
&&
(
independent_target (Pair_mk_fst p) = independent_target ds
&&
(
independent_target (Pair_mk_snd p) = independent_target ds
&&
(
--> shuffle (is_balanced (Pair_mk_fst p) = is_balanced ds)
&&
(
--> shuffle (is_balanced (Pair_mk_snd p) = is_balanced ds)
&&
clean_test (Pair_mk_snd p) = (coupled ds = False && --> (is_timeseries ds) (shuffle = False))
)
)
)
)
)
)
)
)
)
)
)
)
)
}
def train_of (p : Pair Dataset Dataset) : {d : Dataset | d = Pair_mk_fst p}
def test_of (p : Pair Dataset Dataset) : {d : Dataset | d = Pair_mk_snd p}
def copy_dataset (1 ds : Dataset) : {
p : Pair Dataset Dataset | ds_rows (Pair_mk_fst p) = ds_rows ds
&&
(
ds_rows (Pair_mk_snd p) = ds_rows ds
&&
(
ds_features (Pair_mk_fst p) = ds_features ds
&&
(
ds_features (Pair_mk_snd p) = ds_features ds
&&
(
ds_classes (Pair_mk_fst p) = ds_classes ds
&&
(
ds_classes (Pair_mk_snd p) = ds_classes ds
&&
(
is_balanced (Pair_mk_fst p) = is_balanced ds
&&
(
is_balanced (Pair_mk_snd p) = is_balanced ds
&&
(
is_timeseries (Pair_mk_fst p) = is_timeseries ds
&&
(
is_timeseries (Pair_mk_snd p) = is_timeseries ds
&&
(
has_missing (Pair_mk_fst p) = has_missing ds
&&
(
has_missing (Pair_mk_snd p) = has_missing ds
&&
(
coupled (Pair_mk_fst p) = coupled ds
&&
(
coupled (Pair_mk_snd p) = coupled ds
&&
(
independent_target (Pair_mk_fst p) = independent_target ds
&&
(
independent_target (Pair_mk_snd p) = independent_target ds
&&
(clean_test (Pair_mk_fst p) = clean_test ds && clean_test (Pair_mk_snd p) = clean_test ds)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
)
}
def fst_dataset (p : Pair Dataset Dataset) : {d : Dataset | d = Pair_mk_fst p}
def snd_dataset (p : Pair Dataset Dataset) : {d : Dataset | d = Pair_mk_snd p}
def smote (1 ds : Dataset | ds_classes ds ≥ 2) : {
out : Dataset | is_balanced out = True
&&
(
ds_features out = ds_features ds
&&
(
ds_classes out = ds_classes ds
&&
(
ds_rows out ≥ ds_rows ds
&&
(
coupled out = True
&&
(
has_missing out = has_missing ds
&&
(is_timeseries out = is_timeseries ds && independent_target out = independent_target ds)
)
)
)
)
)
}
def random_oversample (1 ds : Dataset | ds_classes ds ≥ 2) : {
out : Dataset | is_balanced out = True
&&
(
ds_features out = ds_features ds
&&
(
ds_classes out = ds_classes ds
&&
(
ds_rows out ≥ ds_rows ds
&&
(
coupled out = True
&&
(
has_missing out = has_missing ds
&&
(is_timeseries out = is_timeseries ds && independent_target out = independent_target ds)
)
)
)
)
)
}
def random_undersample (1 ds : Dataset | ds_classes ds ≥ 2) : {
out : Dataset | is_balanced out = True
&&
(
ds_features out = ds_features ds
&&
(
ds_classes out = ds_classes ds
&&
(
ds_rows out ≤ ds_rows ds
&&
(
coupled out = True
&&
(
has_missing out = has_missing ds
&&
(is_timeseries out = is_timeseries ds && independent_target out = independent_target ds)
)
)
)
)
)
}
def standard_scale (1 ds : Dataset) : {
out : Dataset | ds_rows out = ds_rows ds
&&
(
ds_features out = ds_features ds
&&
(
ds_classes out = ds_classes ds
&&
(
is_balanced out = is_balanced ds
&&
(
coupled out = True
&&
(
has_missing out = has_missing ds
&&
(
is_timeseries out = is_timeseries ds
&&
(independent_target out = independent_target ds && clean_test out = clean_test ds)
)
)
)
)
)
)
}
def minmax_scale (1 ds : Dataset) : {
out : Dataset | ds_rows out = ds_rows ds
&&
(
ds_features out = ds_features ds
&&
(
ds_classes out = ds_classes ds
&&
(
is_balanced out = is_balanced ds
&&
(
coupled out = True
&&
(
has_missing out = has_missing ds
&&
(
is_timeseries out = is_timeseries ds
&&
(independent_target out = independent_target ds && clean_test out = clean_test ds)
)
)
)
)
)
)
}
def robust_scale (1 ds : Dataset) : {
out : Dataset | ds_rows out = ds_rows ds
&&
(
ds_features out = ds_features ds
&&
(
ds_classes out = ds_classes ds
&&
(
is_balanced out = is_balanced ds
&&
(
coupled out = True
&&
(
has_missing out = has_missing ds
&&
(
is_timeseries out = is_timeseries ds
&&
(independent_target out = independent_target ds && clean_test out = clean_test ds)
)
)
)
)
)
)
}
def fill_mean (1 ds : Dataset) : {
out : Dataset | ds_rows out = ds_rows ds
&&
(
ds_features out = ds_features ds
&&
(
ds_classes out = ds_classes ds
&&
(
is_balanced out = is_balanced ds
&&
(
has_missing out = False
&&
(
coupled out = True
&&
(
is_timeseries out = is_timeseries ds
&&
(independent_target out = independent_target ds && clean_test out = clean_test ds)
)
)
)
)
)
)
}
def fill_most_frequent (1 ds : Dataset) : {
out : Dataset | ds_rows out = ds_rows ds
&&
(
ds_features out = ds_features ds
&&
(
ds_classes out = ds_classes ds
&&
(
is_balanced out = is_balanced ds
&&
(
has_missing out = False
&&
(
coupled out = True
&&
(
is_timeseries out = is_timeseries ds
&&
(independent_target out = independent_target ds && clean_test out = clean_test ds)
)
)
)
)
)
)
}
def fill_constant (value : Float) (1 ds : Dataset) : {
out : Dataset | ds_rows out = ds_rows ds
&&
(
ds_features out = ds_features ds
&&
(
ds_classes out = ds_classes ds
&&
(
is_balanced out = is_balanced ds
&&
(
has_missing out = False
&&
(
coupled out = True
&&
(
is_timeseries out = is_timeseries ds
&&
(independent_target out = independent_target ds && clean_test out = clean_test ds)
)
)
)
)
)
)
}
def predict (model : SklearnClassifier) (1 ds : Dataset | clf_features model = ds_features ds) : List
def predict_proba (model : SklearnClassifier) (1 ds : Dataset | clf_features model = ds_features ds) : List
def predict_value (model : SklearnRegressor) (1 ds : Dataset | reg_features model = ds_features ds) : List
def accuracy (model : SklearnClassifier) (1 ds : Dataset | clf_features model = ds_features ds && (clean_test ds = True && is_balanced ds = True)) : {f : Float | 0.0 ≤ f && f ≤ 1.0}
def precision (model : SklearnClassifier) (1 ds : Dataset | clf_features model = ds_features ds && (clean_test ds = True && is_balanced ds = True)) : {f : Float | 0.0 ≤ f && f ≤ 1.0}
def recall (model : SklearnClassifier) (1 ds : Dataset | clf_features model = ds_features ds && (clean_test ds = True && is_balanced ds = True)) : {f : Float | 0.0 ≤ f && f ≤ 1.0}
def f1 (model : SklearnClassifier) (1 ds : Dataset | clf_features model = ds_features ds && clean_test ds = True) : {f : Float | 0.0 ≤ f && f ≤ 1.0}
def roc_auc (model : SklearnClassifier) (1 ds : Dataset | clf_features model = ds_features ds && clean_test ds = True) : {f : Float | 0.0 ≤ f && f ≤ 1.0}
def confusion_matrix (model : SklearnClassifier) (1 ds : Dataset | clf_features model = ds_features ds && clean_test ds = True) : List
def classification_report (model : SklearnClassifier) (1 ds : Dataset | clf_features model = ds_features ds && clean_test ds = True) : String
def mse (model : SklearnRegressor) (1 ds : Dataset | reg_features model = ds_features ds && clean_test ds = True) : {f : Float | f ≥ 0.0}
def rmse (model : SklearnRegressor) (1 ds : Dataset | reg_features model = ds_features ds && clean_test ds = True) : {f : Float | f ≥ 0.0}
def mae (model : SklearnRegressor) (1 ds : Dataset | reg_features model = ds_features ds && clean_test ds = True) : {f : Float | f ≥ 0.0}
def r2 (model : SklearnRegressor) (1 ds : Dataset | reg_features model = ds_features ds && clean_test ds = True) : Float
def explained_variance (model : SklearnRegressor) (1 ds : Dataset | reg_features model = ds_features ds && clean_test ds = True) : Float
def classify_one (model : SklearnClassifier) (x : Vector) : Vector
def regress_one (model : SklearnRegressor) (x : Vector) : Float
def clf_n_features (model : SklearnClassifier) : {n : Int | n = clf_features model && n ≥ 0}
def clf_n_classes (model : SklearnClassifier) : {n : Int | n = clf_classes model && n ≥ 0}
def reg_n_features (model : SklearnRegressor) : {n : Int | n = reg_features model && n ≥ 0}
Uninterpreted
Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.
def df_rows : (df : DataFrame) → Int
def df_cols : (df : DataFrame) → Int
def ds_rows : (ds : Dataset) → Int
def ds_features : (ds : Dataset) → Int
def ds_classes : (ds : Dataset) → Int
def is_balanced : (ds : Dataset) → Bool
def clf_features : (m : SklearnClassifier) → Int
def clf_classes : (m : SklearnClassifier) → Int
def reg_features : (m : SklearnRegressor) → Int
def is_timeseries : (ds : Dataset) → Bool
def has_missing : (ds : Dataset) → Bool
def coupled : (ds : Dataset) → Bool
def clean_test : (ds : Dataset) → Bool
def independent_target : (ds : Dataset) → Bool
def ds_target : (ds : Dataset) → (name : String) → Bool