r/programming • u/Lost-Dragonfruit-663 • 7d ago

How to test if your numerical code is Mathematically correct?

https://medium.com/@aadyachinubhai/scikit-verify-translate-python-numpy-programs-to-symbolic-mathematics-c664d41ba571
34 Upvotes

78% Upvoted

10 comments sorted by

28

u/SaltMaker23 7d ago

You write math first

Verify it in lean and/or simulate it with whatever means are relevant and verifiable experimentally for your usecase Once you've proven the theorteical framework in lean and your ability to simulate it, you can integrate it to other systems

Needless to say its impractical in industry outside of research and no one will pay you for all that wasted time where you could have yolod until it works

3

u/Lost-Dragonfruit-663 6d ago

Right, lean is the gold standard. However, I think with more and more AI making its way, it’s a good time to start thinking about verification.

2

u/i_rate_slop 5d ago

What do you mean “however?” Lean is the verification and AI can help.

-1

u/SaltMaker23 6d ago edited 6d ago

AI can write Lean and convert code to formula, there's no bottleneck, at least no to someone that wants.

In a single prompt in most cases you can validate things.

Whatever the blog is showing is so basic and trivial that it's a bit useless to demonstrate it, you can just ask directly claude to check, or to write a test against some set of known results.

If you're doing work on prime distributions and returning the lowest dimensional contraction or excess of some form of advanced algebraic structure of the generalized Riemann hypothesis, then it might be a good call to use Lean.

We are in a programming sub, I don't believe many here has any form of code that warrant using Lean.

0

u/Lost-Dragonfruit-663 6d ago

There are other posts that verify more advanced mathematics, for example, verifying the closed-form cubic smoothing B-spline penalty. We just don't put that in the blog post because it complicates the main point. I know how complicated that problem is because I implemented it in SciPy.

I think you're right about Lean, though. I also don't think I would necessarily want AI-generated Lean code as the thing doing the verification. Using AI to verify AI may not be the best move, even if it is probably sufficient most of the time.

I'm not claiming this is a game changer. It's simply something I've found useful in my day to day work, particularly while working on SciPy. And in that ecosystem, at least from what I've seen, essentially nobody is using Lean.

4

u/SaltMaker23 6d ago

Lean doesn't care that you used AI for the whole thing all the way back, so long that the proof proves without "sorry", it's fine.

8

u/araujoms 4d ago

For example, if an existing implementation is GPL licensed, you may be unable to inspect or reuse its source code;

What kind of drivel is this?

4

u/Axman6 6d ago

Maths is full of useful identities which can be used to test the accuracy of algorithms. Probably a poor example, but when implementing sin/cos, you can use the ⍱x. sin2 (x) + cos2 (x) = 1 identity. 

There’s a book, which you can the pdf online of, called Modern Computer Arithmetic, which should cover a lot of what you want.