IgnatiusPang opened a new pull request, #25744: URL: https://github.com/apache/datafusion/pull/25744
# Pull Request: Metric Non-Negativity and Boundedness in `cosine_distance` - **Target Repository**: `apache/datafusion` (`main`) - **Fork Branch**: `APAF-bioinformatics/datafusion:fix-cosine-distance-non-negative` - **Commit**: `4ecba5e52a19c0ec1398e074632288b0666d5c28` - **PR Comparison Link**: [https://github.com/apache/datafusion/compare/main...APAF-bioinformatics:datafusion:fix-cosine-distance-non-negative](https://github.com/apache/datafusion/compare/main...APAF-bioinformatics:datafusion:fix-cosine-distance-non-negative) --- ## 1. Pull Request Title ```text fix: clamp cosine_distance to enforce metric non-negativity and boundedness [0.0, 2.0] ``` --- ## 2. Pull Request Description Body ```markdown ## Which issue does this PR close? Closes #. ## Rationale for this change In `datafusion-functions-nested::cosine_distance`, the distance is evaluated as: ```rust builder.append_value(1.0 - dot / (sq1.sqrt() * sq2.sqrt())); ``` In IEEE-754 floating-point arithmetic, $\sqrt{S} \times \sqrt{S}$ does not always equal $S$. For example, with $S = 3.0$ (such as when comparing the identical unit vectors `[1.0, 1.0, 1.0]`): - `dot = 3.0` - `sq1 = 3.0`, `sq2 = 3.0` - `sq1.sqrt() * sq2.sqrt() = 2.9999999999999996 < 3.0` - `dot / (sq1.sqrt() * sq2.sqrt()) = 1.0000000000000002 > 1.0` - `1.0 - ratio = -2.220446049250313e-16 < 0.0` This violates fundamental metric axioms: 1. **Metric non-negativity**: $d(x, y) \ge 0$ for all $x, y$. 2. **Identity of indiscernibles**: $d(x, x) = 0$. 3. **Distance boundedness**: $d(x, y) \in [0.0, 2.0]$ for cosine distance. For opposite vectors, floating-point roundoff can similarly produce distances slightly exceeding `2.0` (e.g. `2.0000000000000004`). ## What changes are included in this PR? 1. **Cosine Similarity & Distance Clamping**: - Clamps the computed similarity ratio `(dot / (sq1.sqrt() * sq2.sqrt())).clamp(-1.0, 1.0)`. - Clamps the resulting cosine distance `(1.0 - sim).clamp(0.0, 2.0)`. - Preserves standard IEEE-754 `NaN` propagation (since `f64::clamp` on `NaN` evaluates `NaN < min` and `NaN > max` to `false`, propagating `NaN`). 2. **Formal Verification (Lean 4)**: - Formally verified theorem contract synthesized and applied via Lean 4 Three-Way Semantic Merge: - `cosine_distance_non_negative` 3. **Comprehensive Regression Tests**: - Unit tests in `cosine_distance.rs`: - `test_cosine_distance_identical_vectors_metric_non_negative`: Verifies that identical vectors prone to $\sqrt{3}^2$ roundoff return strictly `0.0` and never negative numbers. - `test_cosine_distance_opposite_vectors_bounded`: Verifies that opposite vectors return `2.0` and never exceed `2.0`. - Sqllogictest in `cosine_distance.slt`: Added query testing `select cosine_distance([1.0, 1.0, 1.0], [1.0, 1.0, 1.0]);` returning `0`. ## What is the testing strategy for this PR? - Full crate test suite pass for `datafusion-functions-nested` (155 tests total): ```bash cargo test -p datafusion-functions-nested ``` Result: `153 passed (unittests), 2 passed (doctests), 0 failed`. - Full sqllogictest suite pass for `cosine_distance.slt`: ```bash cargo test -p datafusion-sqllogictest --test sqllogictests -- cosine_distance ``` Result: `Progress: 1/1 files completed (100%), 0 failed`. ## Are there any user-facing changes? No breaking API changes. Bug fix only: `cosine_distance` will never return negative values (such as `-2.22e-16`) on identical vectors or values $> 2.0$ on opposite vectors due to floating-point roundoff. ``` -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected] --------------------------------------------------------------------- To unsubscribe, e-mail: [email protected] For additional commands, e-mail: [email protected]
