Comment by kragen
2 days ago
I'm curious about how you'd do that, too. I haven't tried doing anything like that, but I'd think you'd start by trying to formalize the usual optimality proof for the Kalman filter, transfer it to actual program logic on the assumption that the program manipulates real numbers, try to get the proof to work on floating-point numbers, and finally extract the program from the proof to run it.
https://youtu.be/_LjN3UclYzU has a different attempt to formalize Kalman filters which I think we can all agree was not a successful formalization.
It is really not that difficult. Here is a paper that formalizes a version of feed forward networks to prove properties about them.
https://arxiv.org/pdf/2304.10558
I only skimmed this paper, but it doesn't mention floating point (it's only modeling the FNN as a function on reals), and I don't think you can extract a working FNN implementation from an SMT-LIB or Z3 problem statement, so I think you have to take on faith the correspondence between the implementation you're running and the thing you proved correct.
But that's the actual problem we're trying to solve; nobody really doubts Kalman's proof of his filter's optimality.
So this paper is not a relevant answer to the question, "how would you prove an implementation of a Kalman filter is correct?"
In most cases the data a kalman filter is working on has some precision which is much lower than the available precision in the floating format you are using. The problem is inherently a statistical one, since the expected precision depends on the statistics of your data source.
So you would probably adopt some conservative approach in which you showed that the worst case floating point rounding error is << some quantile of error due to the data.
But, I think specialised tools are more commonly used than general process. Eg, see https://github.com/arpra-project/arpra
1 reply →