计算科学 - 浮点算术中的关联性因两个值而失败 - 吾爱随笔录

浮点算术中的关联性因两个值而失败

计算科学浮点

2021-11-27 00:03:36

来自math.stackexchange的交叉发帖，因为这里可能有人熟悉这个话题。

假设在具有有限精度、有界指数和四舍五入的浮点运算中工作。

令为正。不难找到这样的例子 $x,y$

(x + y) - x > y

$(x+y)-x > y$

为了构建软件测试，我想找到一个示例或证明不存在以下示例：

让成为 x 的继任。 $s(x)$ $x$

是否可以同时拥有

\begin{aligned} (x + y) - x & > y \\ (x + y) - s (x) & > y \end{aligned}

$\begin{align}(x+y)-x&>y\\(x+y)-s(x)&>y\end{align}$

编写一个搜索这样一个示例的程序很容易，但测试所有可能性并证明该示例不以这种方式存在也是不可行的。到目前为止，我的代码还没有任何示例。

示例：如果看到的示例有所帮助，请使用然后。第一个不等式的例子还有很多。 $(x+y)-x>y$

\begin{aligned} x & = 1.1234567891234568 \\ y & = 1 e - 5 ( denoting 10^{- 5}) \end{aligned}

$\begin{align} x&=1.1234567891234568\\ y&=1e-5\text{ ( denoting }10^{-5}) \end{align}$

(x + y) - x = 1.0000000000065512 e - 05 > y

$(x+y)-x=1.0000000000065512e-05 > y$

1个回答

众所周知，这些浮点反例很难手动发现。通常，您确实希望随机蛮力搜索起作用，尤其是在 32 位浮点数上，但有时它会失败。

现在，您可以使用 SMT 求解器，例如 Z3，因此您可以尝试在 Z3 中制定公式，看看它是否可以找到反例。这是解决问题的“高科技”方法。这种方法很好，因为它不需要您非常了解浮点运算即可使用它。

我尝试了这个，使用 Haskell，使用 Z3 作为后端的 SBV 包。它只查看范围，其中 $x\in(1,2)$ $s(x) = x + \epsilon$

import Data.SBV

ε = 1.1920928955078125e-07

f :: SFloat -> SFloat -> SBool
f x y = 1 .< x &&& x .< 2 &&& fpIsNormal y &&& (x + y) - (x + ε) .> y

它立即找到了这个反例：

λ> sat f
Satisfiable. Model:
  s0 =       1.5 :: Float
  s1 = 3.9999998 :: Float

这满足： $(x+y)-s(x) > y$

julia> x, y = 1.5f0, 3.9999998f0
julia> ((x + y) - nextfloat(x)) - y
2.3841858f-7
julia> (x + y) - nextfloat(x) > y
true

注意查看您的示例，我不清楚您是否对和的大小有限制。例如，如果将其限制为、，则无法满足。但是只限制，而不是，看起来你得到非常大与。 $x$ $y$ $x\in(1,2)$ $y\in(0,1)$ $(x+y)-s(x)>y$ $x\in(1,2)$ $y$ $n$ $(x+y)-(x+n\epsilon) > y$

看一些小例子，似乎最坏的情况可以通过取（二进制，单精度）得到，因此。在双精度下，它可以采用和（这只是二进制中的所有），并且关系只会从开始分解.

x = 1.5 = (1.1)_{2}, y = 2^{k} \times (0.111111111111111111111111)_{2} = 2^{k} \times (1 - 2^{- 24}),

$x = 1.5 = (1.1)_2, \qquad y = 2^k\times (0.111111111111111111111111)_2 = 2^k\times (1-2^{-24}),$

n = 2^{k - 1}

$n=2^{k-1}$

(x + y) - (x + 2^{k - 1} ϵ) = y

$(x+y)-(x+2^{k-1}\epsilon)=y$

x = 1.5

$x=1.5$

y = (1 - 2^{- 53}) \times 2^{k}

$y=(1-2^{-53})\times 2^k$

k \geq 51

$k\geq51$

其它你可能感兴趣的问题

上一篇牵引力 -> 压力；应力->位移梯度下一篇为什么 LU 分解的各个部分的速度如此不同？