Skip to content

Add a refinement-typed ML library and Titanic example - #492

Open
joaokorreia wants to merge 13 commits into
alcides:masterfrom
joaokorreia:machine_learning_library
Open

Add a refinement-typed ML library and Titanic example#492
joaokorreia wants to merge 13 commits into
alcides:masterfrom
joaokorreia:machine_learning_library

Conversation

@joaokorreia

@joaokorreia joaokorreia commented Aug 18, 2026

Copy link
Copy Markdown
Contributor

What changed

  • move ML ownership rules into Aeon with linear DataFrame, Dataset, DatasetSplit, TrainingDataset, and TestingDataset types
  • express target bounds, split fractions, feature compatibility, split provenance, train/test roles, and bounded accuracy as Aeon refinement contracts
  • keep the Python binding thin: pandas/scikit-learn operations only, without runtime consumption fields, provenance tokens, custom restriction exceptions, or duplicated runtime guards
  • make the external CSV schema boundary explicit with assume_columns
  • replace runtime-oriented restriction checks with paired positive/negative Aeon programs
  • keep one end-to-end Titanic pipeline as a runtime smoke test
  • write examples and documentation in English

Design

The binding now represents datasets and split parts with ordinary pandas objects and tuples. Linear consumption and compatibility are checked by Aeon before evaluation.

Properties that depend on the contents of an arbitrary external CSV cannot be inferred from its path alone. This revision therefore does not claim unverified class-count or per-class distribution facts. The Titanic example explicitly supplies its audited column count through assume_columns; a future version could replace this trusted schema assumption with a dedicated witness if that is the preferred API.

The arbitrary four-row requirement was removed because it does not guarantee that an arbitrary stratified split is valid.

Static guarantees covered by examples

  • all five ML resources must be bound and consumed linearly
  • target indices are non-negative and within the declared column count
  • split fractions are strictly between 0 and 1
  • training and testing values cannot be interchanged
  • training/test feature counts and logical split provenance match the classifier
  • target row/feature metadata is preserved
  • accuracy is between 0 and 1

Validation

  • pytest tests/machine_learning_test.py -q -- 39 passed
  • pytest tests/array_qtt_test.py tests/test_imports.py -q -- 17 passed
  • all non-mypy pre-commit hooks passed
  • mypy aeon tests --no-strict-optional --ignore-missing-imports --explicit-package-bases --platform linux -- passed (352 files)

The default Windows mypy invocation still reports the repository's existing Unix-only signal.SIGALRM, setitimer, and ITIMER_REAL attributes. The equivalent Linux-platform check above passes.

@cursor
cursor Bot force-pushed the machine_learning_library branch from 59c80fa to 76424c5 Compare August 19, 2026 03:01
Comment thread aeon/bindings/machine_learning.py Outdated
"""Owned wrapper around a pandas DataFrame."""

value: pd.DataFrame
_consumed: bool = field(default=False, init=False, repr=False)

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can't we have this verification just using linear types in the language, instead of spending memory with the field (and runtime cost)?

Or is there any reason for this choice that I'm missing?

Comment thread aeon/bindings/machine_learning.py Outdated

features: pd.DataFrame
target: pd.Series
split_token: object = field(repr=False)

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand that the split_token is.

Comment thread aeon/bindings/machine_learning.py Outdated

def _require_available(resource: LinearResource, expected_type: type, operation: str) -> None:
if not isinstance(resource, expected_type):
raise TypeError(f"{operation} esperava {expected_type.__name__}, recebeu {type(resource).__name__}")

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We need the errors (and everything) in English.

Comment thread aeon/libraries/MLCore.ae Outdated
# TODO: Consider moving the four-row validation to ``target``, where the
# target-class distribution is known.
def read_csv (path: String) :
{df: DataFrame | df_rows df >= 4 && df_cols df >= 2} :=

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we have a requirement of 4 rows?

let 1 df := read_csv "examples/machine_learning/titanic.csv" in
let first_dataset := target df 1 in
let second_dataset := target df 1 in
0.0

Copy link
Copy Markdown
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Boa! São estes os tipos de exemplos que precisamos!

Precisamos é da documentação em inglês.

@cursor
cursor Bot force-pushed the machine_learning_library branch 2 times, most recently from f2b20aa to a3f8029 Compare August 23, 2026 03:03
@alcides
alcides marked this pull request as ready for review August 31, 2026 13:04
@cursor
cursor Bot force-pushed the machine_learning_library branch from a3f8029 to 3629c5d Compare September 1, 2026 03:04
dataset handling and model training functions
- Introduced a new example for training and evaluating a decision tree classifier on the Titanic dataset.
- Updated `pyproject.toml` to include pandas and scikit-learn as dependencies.
- Created comprehensive tests for the machine learning library, covering data reading, dataset validation, and model training/evaluation.
- Ensured that the tests validate the ownership protocol and resource consumption rules in the library.
dataset handling and model training functions
- Introduced a new example for training and evaluating a decision tree classifier on the Titanic dataset.
- Updated `pyproject.toml` to include pandas and scikit-learn as dependencies.
- Created comprehensive tests for the machine learning library, covering data reading, dataset validation, and model training/evaluation.
- Ensured that the tests validate the ownership protocol and resource consumption rules in the library.
@cursor
cursor Bot force-pushed the machine_learning_library branch from 3629c5d to 1094e0a Compare September 2, 2026 03:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants