Last week I visited Tobias Paxian and prof. Armin Biere at the University of Freiburg.
The topic of the visit was research into proof logging combinatorial optimisation solvers, i.e. methods that can generate not only optimal solutions, but also formal proofs of optimality that can then be verified independently of the implementation of the optimisation procedure. Proof logging offers a high-promise approach toward trustworthy AI since software used to verify the proofs is often far less complicated (and thus easier to trust) than the software used to compute the solutions. As such I believe in the potential of proof logging and am happy to be involved on the fore-front of extending it into optimisation.
I’d like to thank Tobias and Armin for being excellent hosts. I found the discussion fruitful and look forward to continuing the collaboration, hopefully visiting Freiburg in the future as well!
On the way back to Helsinki I had time for a quick hike up a mountain in Switzerland. 10.5km with 600m elevation, I am not sure I would be cut out to be a Swiss person….
Jeremias Berg 