Skip to content

vinary-tree/adaptive-msm

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

3 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

adaptive-msm

Online-learned Move–Split–Merge time-series distance, and MSM as a weighted finite-state transducer.

adaptive-msm does two things over the Move–Split–Merge (MSM) time-series metric of Stefan, Athitsos & Das:

  1. Learns the metric's one free parameter online. MSM's split/merge constant $c$ trades off time differences against amplitude differences, and the right value is data-dependent. AdaptiveMsm adapts $c$ from observed costs in ~56 ns per round.
  2. Embeds MSM as a WFST. MsmWfst exposes the MSM alignment lattice as a lling_llang::Wfst<u8, TropicalWeight>, so MSM similarity can be composed with other weighted transducers and solved by generic shortest-distance.

Unlike DTW, MSM is a true metric (its triangle inequality is machine-checked upstream), which is what makes metric-space pruning sound.

[dependencies]
adaptive-msm = "0.1"                                          # learner + WFST
# adaptive-msm = { version = "0.1", default-features = false } # learner only

Quick start

use adaptive_msm::{AdaptiveMsm, AdaptiveMsmConfig, MsmConfig};

// Adapt the split/merge constant c online from a cost signal.
let mut learner = AdaptiveMsm::new(
    AdaptiveMsmConfig::new().initial_c(1.0).epsilon(1.0).seed(42),
);
let cost = learner.predict(&[1.0, 2.0, 3.0], &[2.0, 3.0, 4.0]);
learner.observe(cost);
println!("learned c = {}", learner.current_c());

// Or just take a distance with a fixed c.
let d = MsmConfig::new(1.0).distance(&[1.0, 2.0, 3.0], &[1.0, 2.5, 3.0]);

Getting started · Learner guide · WFST guide · Cookbook

Why this crate exists

It is the wfst::msm layer extracted out of liblevenshtein to break a package cycle — the WFST code needs lling-llang, which already depends on liblevenshtein. Lifting it into a crate that sits above both makes the graph a DAG again. See ADR 0001.

Acyclic dependency layering

Results

The learner converges. On a loss with a known minimizer $c^\star = 3$, $c$ moves from $7.0$ to $3.047$ — a 23× lower loss than a non-adaptive baseline. The measured trajectory matches the convergence theorem's prediction (round 1: predicted 6.20, measured 6.25). On real MSM distances it recovers a hidden $c^\star = 2.0$ as $2.07$. E1 ledger

Learner convergence

Pruning makes the lattice cheap. The unpruned lattice materializes the whole $(n{+}1)^2$ DP grid, but a max_cost threshold caps the state count at a constant independent of $n$ (at $n=64$: 4225 states → 80 at threshold 16, → 7 at threshold 4). E2 ledger

Performance (AMD Threadripper PRO 5975WX, single core): MSM distance is a clean $O(mn)$ (1.03 µs at $n{=}16$ → 4.58 ms at $n{=}1024$); one learner round is 55.8 ns. Benchmarks

Correctness

This crate cites the machine-checked foundations that already exist upstream (MSM is a metric; the tropical semiring laws; WFST semantics) and proves what is new:

Claim Status
MsmWeight's cost projection is a semiring homomorphism ✅ Rocq, axiom-free (docs/formal/rocq/MsmWeightHomomorphism.v)
MSM lattice shortest path = MsmConfig::distance ✅ Rocq, axiom-free (EmbeddingEquivalence.v) + executable test
max_cost pruning is sound ✅ Rocq, axiom-free (prune_sound)
Learner keeps $c \in [c_{\min}, c_{\max}]$, $c > 0$, terminates — under an adversarial gradient ✅ TLA+/TLC (docs/formal/tla/LearnerDynamics.tla)
FPTL $O(\sqrt{T\log\lvert\Sigma\rvert})$ regret for this learner not claimed — a convergence theorem is proven instead

That last row is deliberate. The learner is named for Follow-the-Perturbed- Tropical-Leader, but it is a scalar finite-difference method, not the FPL path-expert algorithm the regret theorem is about — so it does not inherit that bound. The gap is stated precisely, not papered over: Regret & the honest gap.

docs/formal/verify.sh      # compiles the Rocq proofs (axiom-free) + runs TLC

Documentation

Full corpus in docs/ — theory, design, architecture, engineering, usage, scientific ledger, and formal proofs.

Development

cargo test --all-features     # 70 unit + 9 integration + 3 doctests
cargo clippy --all-features --all-targets -- -D warnings
cargo build --no-default-features   # learner-only surface (no lling-llang edge)
scripts/run-experiments.sh          # reproduce every figure and CSV
docs/formal/verify.sh               # re-check every proof

No unsafe. See security & robustness and the honest known-issues register.

References

  • Stefan, A., Athitsos, V., & Das, G. (2013). "The Move-Split-Merge Metric for Time Series." IEEE TKDE 25(6), 1425–1438. DOI: 10.1109/TKDE.2012.88
  • Cortes, C., Kuznetsov, V., Mohri, M., & Warmuth, M. (2015). "On-Line Learning Algorithms for Path Experts with Non-Additive Losses." COLT, PMLR 40:424–447.
  • Mohri, M. (2002). "Semiring Frameworks and Algorithms for Shortest-Distance Problems." JALC 7(3), 321–350. DOI: 10.25596/jalc-2002-321

License

Apache-2.0

About

Online-learned Move–Split–Merge time-series distance, and MSM as a weighted finite-state transducer.

Resources

License

Stars

0 stars

Watchers

0 watching

Forks

Releases

No releases published

Packages

 
 
 

Contributors