leanprover / LNSym

Armv8 Native Code Symbolic Simulator in Lean
Apache License 2.0
62 stars 18 forks source link

chore: fix geomean computation #196

Closed bollu closed 1 month ago

bollu commented 1 month ago

Description:

The geomean computation that was incorrectly suggested by @bollu failed to take into account that the TotalRunTime counter was adding the real runtimes, not multiplying them as one should for geomean.

We change the geomean computation algorithm, to accumulate the log of the runtimes, and then divide by n followed by exponentiation as a final step for better numerical accuracy.

$$ g \equiv (t_1 \times t_2 \times \dots \times t_n)^{1/n} = \exp \bigg(\frac{\log t_1 + \log t_2 + \dots \log t_n}{n} \bigg) $$

Testing:

What tests have been run? Did make all succeed for your changes? Was conformance testing successful on an Aarch64 machine?

Conformance succeeds.

License:

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.