CrocSwapのPRが整数乗算の指数κを0.003の大台へ押し上げ
Κ = 0.003 for integer multiplication crossed
CrocSwap/integer-mult-boundsのPR #4441で、クエリ間引きとヘルパー再タイミングを組み合わせ、条件付き境界 T(n) = O(n (log n)^(1 - 0.00300105)) を導出した。κは前回の0.00296から1.39%増、固定プロファイルの根は区間証明で厳密に挟み込まれている。ただし著者自身がレビュー待ちの条件付き構成と明言し、無条件定理や実用性能は主張していない。
本PRは著者自身が検証した条件付き構成であり、レビューを待つ段階にある。
HNでの議論
22- jdb1729
@platypii と私は、kappa の改善を Lean で検証する取り組みをここで進めています: https://github.com/platypii/integer-mult-bounds-lean
キャンペーンの現状: Mathlib の TM2 マシン上で kappa >= 2^-14.38 が無条件に証明済み。貢献歓迎です！
- joeldw
この高速化が具体的にどう機能するのか、簡単に理解する方法を誰か知りませんか？標準的な O(N log N) の乗算は、IIUC では FFT による周波数分解を使いますが、この構成はどんな形になるのでしょうか？
- readthenotes1
「検証済みの fresh-helper リタイミングを、#4440 の p17 クエリ間引き複素コントローラの全 19 個の完全ネイティブ呼び出しすべてに適用する。16 個の有償クエリシェア、アイドル呼び出し全体、メイン演算子、そしてより強力な BIT サプライヤはすべて保持される。」
これらの単語の多くは理解できますが、文脈の中ではどうやら一つも理解できていないようです……