Formal Verification in Scientific Computing

[Steve Omohundro]

Formal Verification in Scientific Computing

https://www.youtube.com/watch?v=r-2kxq4SAu4

Scientific computing is used in many safety-critical areas, from designing and controlling aircraft, to predicting the climate. As such it is important to provide formal guarantees to the numerical results provided by scientific computing, by ensuring that the numerical solutions of differential equations are correct. Our work has focused on providing formally verified numerical solutions for ordinary differential equations, using interactive theorem provers. The results are fully end-to-end, in the sense that they formally prove that the solution computed by the C program is quantifiably close to the real solution of the differential equation. To achieve this, we combine formalization of traditional results from numerical analysis (such as the Lax equivalence theorem), with bounds on iterative methods and floating-point arithmetic, as well as formal C semantics. One challenge of formal verification for scientific computing is to make the formalizations more automatic, and general enough to apply to reasonably realistic scenarios. Another challenge for formal verification is to be relevant to the traditional scientific computing community. Since worst-case bounds are often too conservative in practice, we will discuss ideas on alternate results to formalize. This is joint work with Mohit Tekriwal and Karthik Duraisamy (Michigan), David Bindel and Ariel Kellison (Cornell), Andrew Appel (Princeton), and Geoffrey Hulette (Sandia).

Best,

Steve

[Quinn Dougherty]

Appell's and kellison's codebases here are currently strong reasons to plan for mechanical engineering stuff to be in coq rather than lean: 

- https://github.com/VeriNum/LAProof

- https://github.com/VeriNum/vcfloat 

Unless opus 3.5 is good enough at transpiling. 

I haven't seen any numerical analysis projects in lean 

--
You received this message because you are subscribed to the Google Groups "guaranteed-safe-ai" group.
To unsubscribe from this group and stop receiving emails from it, send an email to guaranteed-safe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/guaranteed-safe-ai/CAOLEBs9X41c9%3DgZuATcohZpiR%3DM%3DmNX%3DKD2RQKEOfh%2BBf%2BbVTQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[Steve Omohundro]

Very cool!

There's the "SciLean" library in Lean but it seems to be in an early stage of development:

SciLean: Scientific Computing in Lean

https://github.com/lecopivo/SciLean

Tyler Josephson's lab  at UMBC is working to formalize various sciences:

https://cbee.umbc.edu/josephson/

Creating “AI Scientists”: Tyler Josephson advances a new field of research through $650,000 NSF CAREER award

https://umbc.edu/stories/tyler-josephson-wins-nsf-career-award-ai/

AI and Theory-Oriented Molecular Science ATOMS Lab

https://atomslab.github.io/

Here's a course he did on "Lean for Scientists and Engineers", the links to video recordings of the classes work:

https://docs.google.com/spreadsheets/d/1ATL-RngI3IGM6uM1ZkXxQdZzYLOAxSn5ZN0MBrfq--o/edit?gid=2038742424#gid=2038742424

Best,

Steve

[Steve Omohundro]

And there's a book! (but it also seems pretty early):

Scientific Computing in Lean

https://lecopivo.github.io/scientific-computing-lean/

1. Introduction
   1. About
   2. Introduction
2. Working with Arrays
   1. Basic Operations
   2. Tensor Operations
   3. Optimizing Array Expressions
3. Examples
   1. Harmonic Oscillator

Best,

Steve

[Quinn Dougherty]

I think scilean is solving a different problem than the projects built on top of flocq and vst. 

Scilean seems to be starting to make it possible to do scientific computing in a type theory, while flocq and vst are big steps toward correctness proofs of the primitives that are actually running on critical systems. 

On one worldview, scilean's impact is greatest if it focuses on being a bare interface to common primitives than come in thru the FFI. Then, high level scientific logic could be proven correct and thru a precondition/postcondition schema gain confidence in the parts that get FFI'd out.

On another worldview, scilean ought to literally provide new primitives, replace blas or eigen or lapack, with proofs in lean replacing decades of battle hardened unit tests. 

The second worldview seems more difficult to support. I roughly consider myself of the first camp. 

[Quinn Dougherty]

I'm glad to see lecopivo started a docs book for the project!