编译时错误控制与区间算术?

计算科学 精确 数字 区间算术
2021-12-06 22:14:55

我使用区间算术进行可靠计算。现在,以良好的区间算术实现编码的过程可能需要大约八倍于没有区间算术执行的相同过程(如果运行时间的最大份额由浮点计算占据)。有时有人问我为什么不手动进行舍入误差分析。对我来说,这看起来不是一个好的选择:它相当于以牺牲人力来节省计算机时间,并为人为错误创造了更多机会。

现在,对我来说有意义的是在计算机的帮助下有一个用于限制舍入误差的系统。期望计算机在相当复杂的程序中分析总错误可能是不现实的,但是人和计算机可能能够比单独工作的人更快、更可靠地完成工作,并生成正确的证书以启动. 参照。在计算机辅助下如何更容易地生成正式证明。

(特别是:我会对如何在严格证明的上下文中使用例如威尔金森意义上的错误分析感兴趣。我可以看到如何通过计算机辅助系统来实现它正式证明的产生。在实践中是否做过这样的事情?)

注意:也许它显示了,但是——我是一个纯粹的数学家;如果我说的话似乎有点幼稚,请随时告诉我。

1个回答

我发现 8 倍开销有点令人惊讶,我想到的最激烈的操作是 4 倍开销,即乘法。其余的可能是由于图书馆效率低下。

我正在使用JuliaIntervals并且从来没有这么慢过。

关于您的问题,Interval Arithmetics 会沿着您采用的计算路径计算错误,然后您可以拒绝解决方案或继续使用它。结果间隔基本上是对一组输入的证明。

正式验证某个输入的区间是否具有可接受的范围与执行区间算术一样昂贵。正式验证某个集合的所有输入范围是否可接受是一个难题。因为您要么必须尝试所有组合(浮点数有限),要么使用更聪明的证明系统。可悲的是,自行验证乘数的属性仍然是一个活跃的研究领域,更不用说通用非线性函数了。

概括:

  • 寻找更好的图书馆
  • 如果您知道给定输入间隔的误差上限,您总是可以从输入中获得上限和下限,进行快捷计算并创建新的间隔。
  • 区间算术就像导数,简单的规则可以被计算机快速应用。形式验证需要搜索,如果这样的问题属于某些功能的 NP 复杂性类别,我不会感到惊讶。