AxiomaticF2EXP and AxiomaticF2LOG scores can drop by 1 ulp when term frequency crosses a power of two

AxiomaticF2EXP and AxiomaticF2LOG compute tfln = freq / (freq + s + s * docLen / avgdl) in double and return the score as a float. Because freq appears both in the numerator and in a denominator that is rounded at freq's scale, the score can drop by one float step when freq crosses a power of two: with the default constructors, boost 1 and the statistics of a real index, 1.0134975 at freq 2^29 - 32 becomes 1.0134974 at 2^29 (F2LOG: 0.10277987 to 0.102779865). That breaks the SimScorer#score rule that a higher freq never gives a lower score, which impacts-based pruning relies on: on a real index a pruned top-1 search returns doc 0 while an exhaustive search returns doc 300. Every release from 8.0.0 to 10.6.0 and main are affected. The trigger is contrived (a frequency near 2^29 and statistics on a float rounding midpoint) and the effect is a 1-ulp near-tie swap, so the priority is low; the fix is a two-line rewrite like the one BM25 got in LUCENE-9071.

tfln = freq / (freq + s + s * docLen / avgdl) (AxiomaticF2EXP.java:72, AxiomaticF2LOG.java:62). F2 has tf = ln = 1 and gamma = 0, so the score is tfln * idf, times the boost, at least 0 (Axiomatic.java:107-116), and BasicSimScorer.score returns (float) of that double (SimilarityBase.java:186). In exact arithmetic tfln only grows with freq. In floating point the numerator freq is exact, but the denominator (freq + s) + (s * docLen / avgdl) is rounded to the double grid at freq's size, and the quotient is rounded again. docLen is the decoded norm read from a float table (SimilarityBase.java:150-154, :180-182), so a field length of 1,073,741,848 (norm byte 248) is used as (float) 1,073,741,848 = 1,073,741,824.

c = s + s * docLen / avgdl = 0.25 + 0.25 * 1,073,741,824 / 1,533,824,654.9 = 0.4250105236...

The exact tfln rises by 4.7e-17, less than the denominator's rounding error, so the computed tfln falls by one double step. The two floats around the score are 1.0134974 and 1.0134975, with midpoint 1.013497412204742431640625: the first double is one double step above it and rounds up, the second is exactly on it and rounds to even, down. Usually the float cast hides a double-level drop; it survives only on such a midpoint. F2LOG shows the same pattern with its own statistics: 0.10277987 to 0.102779865.

A postings block's impacts keep only the highest freq per norm (CompetitiveImpactAccumulator.java:67), and the block's max score is the score of that freq (MaxScoreCache.java:74-89). On the study's real index (default codec, 611 documents; docs 0 and 301 with freq 2^29, doc 300 with 2^29 - 32, all with field length 1,073,741,848), the block of docs 256-511 gets max score 1.0134974, below doc 300's 1.0134975. After doc 0 the collector asks for at least Math.nextUp(1.0134974) = 1.0134975 (TopScoreDocCollector.java:160), and ImpactsDISI skips the block (ImpactsDISI.java:75-88). Pruned top-1: doc 0; exhaustive top-1: doc 300.

• Who. Applications that set AxiomaticF2EXP or AxiomaticF2LOG (both @lucene.experimental) as their similarity. The study's monotonicity analysis of all 73 SimilarityBase model combinations flagged only these two.
• Frequency. With the default s = 0.25, a power of two around 2^29 or 2^30 (the verifier's search found no double-level drop at 2^28 or below with docLen >= freq). That is 5.4e8 occurrences of one term in one field, or custom term frequencies through TermFrequencyAttribute, for example DelimitedTermFrequencyTokenFilter reading word|536870912 (DelimitedTermFrequencyTokenFilter.java:67); the field length then grows by the custom frequency (IndexingChain.java:2054-2060). A smaller s moves the boundary down: the finder's case used s = 0.0010000225, boost 0.88 and freq 2^24.
• Alignment. The statistics (and boost) must put the double score on a float rounding midpoint: the verifier's random search found about 10 such points per 2.5e9 random index-realizable statistics at 2^29 and 2^30.
• Visible effect. For a ranking change, a document with the higher freq and the same norm must share a postings block with the true best hit. The pruned search then returns a hit 1 float ulp (about 1e-7 relative) below the true best, silently. IndexSearcher.search(query, n) prunes once it has counted more than max(n, 1,000) hits (IndexSearcher.java:100, :599; TopScoreDocCollectorManager.java:69).
• How likely. Long-standing (8.0.0 to main), but highly contrived: ordinary corpora are unlikely to reach it; the finding record rates it contrived, priority low.

The test sits in org.apache.lucene.search.similarities for locality but uses only public classes: the default constructors, Similarity#scorer with FieldStats/TermStats, SimScorer#score, and SmallFloat.intToByte4, which is how computeNorm encodes a field length (byte 248 for 1,073,741,848 tokens, 244 for 805,306,392). SmallFloat is marked @lucene.internal; a version without it can take the norm from Similarity#computeNorm(FieldInvertState) instead, as the cross-model reviewer's own test did. The statistics are those of the two real indexes on which the pruned and exhaustive top hits differ; sumDocFreq and the term's totalTermFreq are not read by F2 and only satisfy the stats assertions.

On releases the same test fails with CollectionStatistics/TermStatistics instead of FieldStats/TermStats (renamed on main by GITHUB#15929), and on 8.0.0 to 9.0.0 also with the older LuceneTestCase package.

As the regression test it is this same method. ./gradlew tidy (google-java-format) reflows the assertion message's string concatenation (formatting only); :lucene:core:check -x test then passes.

# gradle, main 645d4fe14a20, seed DEADBEEF, assertions on
TestAxiomaticF2ScoreMonotonicInFreq > testScoreDoesNotDecreaseWhenFreqReachesPowerOfTwo FAILED
    java.lang.AssertionError: expected no drop, got F2EXP 1.0134975 -> 1.0134974, F2LOG 0.10277987 -> 0.102779865
        at __randomizedtesting.SeedInfo.seed([DEADBEEF:8FD97C542809A73B]:0)
        at org.junit.Assert.fail(Assert.java:89)
        at org.junit.Assert.assertTrue(Assert.java:42)
        at org.apache.lucene.search.similarities.TestAxiomaticF2ScoreMonotonicInFreq.testScoreDoesNotDecreaseWhenFreqReachesPowerOfTwo(TestAxiomaticF2ScoreMonotonicInFreq.java:46)
:lucene:core:test (FAILURE): 1 test, 1  failure
# assertions off (-Ptests.asserts=false): the same AssertionError
# with fix A or fix B, assertions on and off: :lucene:core:test (SUCCESS): 1 test

# consequence on a real index (the study verifier's index-level class on 645d4fe14a20, -ea and -da; not the repro)
F2EXP: getMaxScore(511)=1.0134974 < score(doc300)=1.0134975; exhaustive top1=300 pruned top1=0
F2LOG: getMaxScore(511)=0.102779865 < score(doc300)=0.10277987; exhaustive top1=300 pruned top1=0

• The contract (Similarity.java:207-209): "Score must not decrease when {@code freq} increases, ie. if {@code freq1 > freq2}, then {@code score(freq1, norm) >= score(freq2, norm)} for any value of {@code norm} that may be produced by {@link Similarity#computeNorm(FieldInvertState)}." No similarity is exempted.
• The tests. BaseSimilarityTestCase lists "scores don't decrease as term frequencies increase" (:260-261) and compares score(Math.nextDown(freq)) or score(freq - 1) with score(freq), failing on any decrease (:403-435). TestAxiomaticF2EXP and TestAxiomaticF2LOG extend it through AxiomaticTestCase; random sampling practically never lands on an aligned power of two. Both models are also in the test framework's RandomSimilarity rotation (RandomSimilarity.java:126-127).
• History. LUCENE-7997 (#9045) added these checks; Robert Muir wrote there "The other 4 models (F1EXP, F1LOG, F2EXP, F2LOG) are all fine". LUCENE-8010 (#9058) made the core similarities pass them, F2 with no change. LUCENE-8119 wrote the rule into the javadoc. LUCENE-9071 (#10113) rewrote BM25's freq / (freq + norm) as 1 - 1 / (1 + freq * 1/norm) "In order to guarantee monotonicity" (BM25Similarity.java:258-264), and in #13299 Adrien Grand explained that the naive form can give "a lower score evern [sic] though freq is greater by one ulp". F2's tfln has that naive form.

The strongest case: the classes are @lucene.experimental, the effect is a 1-ulp near-tie with a contrived trigger, and in #9131 (LUCENE-8083, 2017) Robert Muir wrote about IB/SPL, F2EXP and F2LOG: "These similarities can't work with maxScore. We should remove or move them out". So it could be a known limitation.

Why it fails: that remark came before LUCENE-8010, after which F2EXP and F2LOG passed the monotonicity tests unchanged; LUCENE-8010 itself added them to the random test rotation, three weeks after the remark, they are still in core and in that rotation, and #9131 was closed as "invalidated by the indexing of impacts"; no mechanism was named and nothing documents an exemption. @lucene.experimental is about API stability, not about the contract pruning depends on. The contract has no tolerance, and Lucene already fixed this exact 1-ulp class for BM25. Verdict: a defect, low priority. The cross-model reviewer rated the intended-behaviour argument weak.

Both options were run on a scratch worktree of 645d4fe14a20 (OpenJDK 25.0.3), removed afterwards. Both rewrite tfln so freq appears once: each IEEE operation with round-to-nearest is monotone in each argument, so the composition, the multiplication by the positive idf and boost, Math.max(0, .) and the float cast are all monotone in freq, the same argument as the comment in BM25's doScore. Both stay monotone in the document length. The exact value is unchanged; only rounding differs. In a probe of 50,000,000 random power-of-two boundaries (random s, document length and average length) the stock form had 561,849 double-level decreases and each option 0; that is a check, not a machine-checked proof.

In AxiomaticF2EXP.tfln and AxiomaticF2LOG.tfln, compute c = s + s * docLen / avgdl once and return 1 / (1 + c / freq).

   protected double tfln(BasicStats stats, double freq, double docLen) {
-    return freq / (freq + this.s + this.s * docLen / stats.getAvgFieldLength());
+    // freq / (freq + c) rewritten as 1 / (1 + c / freq): freq appears once, so every rounding
+    // step is monotone and the result cannot decrease as freq grows
+    double c = this.s + this.s * docLen / stats.getAvgFieldLength();
+    return 1.0 / (1.0 + c / freq);
   }

Trade-offs

• Keeps today's precision (no cancellation): worst relative error against an exact evaluation 3.65e-16, vs 3.49e-16 for the stock form, over freq 1e-3 to 1e9, document length up to 2e9 and average length 1 to 1e6 (1e6 samples).
• Same number of divisions as the BM25 form; both use one more division per call than the stock form (3 instead of 2), and no scoring benchmark was run (c could be cached per norm). freq is finite and positive by contract, so c / freq is defined; s = 0 gives tfln = 1, as today.
• Scores change only by rounding; the explain text ("computed as freq / (freq + s + s * dl / avgdl)") stays true.

What the checks validated

• Stock 645d4fe14a20: the repro fails through gradle with assertions on and off.
• With the fix: the repro passes with assertions on and off; the whole org.apache.lucene.search.similarities package passes (27 classes, 119 tests, seeds DEADBEEF and 5EED1234, 0 failures); :lucene:core:check -x test passes (after tidy reflowed the repro test only).
• The study verifier's index-level class (the pruned vs exhaustive top hit) passes 4 of 4 with the fix shadowed onto the main jars, assertions on and off.

Compute cInv = 1 / (s + s * docLen / avgdl) and return 1 - 1 / (1 + freq * cInv), the rewrite LUCENE-9071 made in BM25.

double cInv = 1.0 / (this.s + this.s * docLen / stats.getAvgFieldLength());
return 1.0 - 1.0 / (1.0 + freq * cInv);

Trade-offs

• The same algebraic pattern as BM25's rewrite (BM25 does it in float, with a cached inverse norm), so reviewers know it; cInv could later be cached per norm as BM25 does.
• Loses precision when freq / c is tiny, because 1 - 1/(1 + x) cancels: worst relative error 3.06e-5 over the wide range above (for example a small sloppy freq in a field far longer than average). In a typical range (integer freq 1 to 1,000, document length up to freq + 100,000, average length 10 to 10,000) none of 1e6 float-rounded tfln values differs from the exact one, for either option.

What the checks validated

• The same gradle runs as the recommended option: the repro passes with assertions on and off, 119 similarities tests on two seeds, :lucene:core:check -x test.
• Earlier, with the fix shadowed onto the main jars: the verifier's index-level class 4 of 4 and upstream TestAxiomaticF2EXP/TestAxiomaticF2LOG 4 of 4; the cross-model reviewer agreed that it fixes the bug.

Method: formal (the study's tier: the tool's own counterexample).

• A monotonicity-typing analysis, a sound abstract interpretation over the exact Java expression trees under stated axioms (correctly rounded IEEE operations are monotone in each argument; Math.log/Math.pow semi-monotone), proved freq- and norm-monotonicity for 71 of the 73 SimilarityBase combinations. The two open ones were F2EXP and F2LOG, the only place where freq reaches an operator from both sides with opposite directions.
• A cvc5 query in the theory of floating point (QF_FP) over that expression returned a double-level counterexample in about 9 minutes. A second stage showed which idf and boost values let the drop survive the float cast, and a scan on the real class found an index-realizable point at freq 2^24 with s = 0.0010000225 and boost 0.88; the finder wrote a JUnit test on a real index.
• An independent verifier wrote its own test and search tool, found the default-parameter case at 2^29 without a boost, showed the pruned vs exhaustive top hit on two real indexes and documented the BM25-style fix direction. It was later reduced to the one-method test.