The issue I have with all these formally verified numerical algorithms is that, at the end of the day, I need this implemented using actual floating point. It's great that it's verified, but not for the case that is practically meaningful. Unless it's implemented using hardware accelerated floating point, most of these algorithms are not sufficiently performant to be practically useful.
Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
11–20 of 57 posts
Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
#12> A human reviewer only needs to read 93 lines of formal specification and run the Lean checker to certify the correctness of the kernel, skipping the intricate 1000+ lines of AI-written implementation. To prove correctness, AI autonomously wrote over 60,000 lines of Lean proofs, which also never have to be inspected by a human. I am curious about the approach as I find claims like this hard to believe. There is a th…
Maybe what you mean is that kernels of proof assistants must be small. Here I am referring to a geometry processing kernel (that is formally verified by a proof assistant). The implementation of the algorithm can be very long, the proof that it conforms to the spec can be very long. But lean checks the proof. And so you only have to trust the spec and that the lean proof assistant is correct.
In the 93 lines I assumed a reviewer already trusts that the kernel of the Lean proof assistants is correct. We have to trust somethings.
Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
#13[flagged]
Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
#14Congrats with this achievement. Do you see it possible that this project can be integrated into, for example, FreeCAD?
Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
#15The issue I have with all these formally verified numerical algorithms is that, at the end of the day, I need this implemented using actual floating point. It's great that it's verified, but not for the case that is practically meaningful. Unless it's implemented using hardware accelerated floating point, most of these algorithms are not sufficiently performant to be practically useful.
It is possible to prove things involving floats, you just have to addionally trust a small set of axioms on floats.
See https://github.com/schildep/verified-3d-mesh-intersection#pe...
Don't know if there is something like this in Lean. But there is https://flocq.gitlabpages.inria.fr
Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
#16Congrats with this achievement. Do you see it possible that this project can be integrated into, for example, FreeCAD?
I think this would need to be reimplemented for performance. But maybe the spec can be reused. As agents get better we might reimplement the same spec for performance with minimal human effort. (See notes regarding performance and floats in readme.)
Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
#17The issue I have with all these formally verified numerical algorithms is that, at the end of the day, I need this implemented using actual floating point. It's great that it's verified, but not for the case that is practically meaningful. Unless it's implemented using hardware accelerated floating point, most of these algorithms are not sufficiently performant to be practically useful.
> The issue I have with all these formally verified numerical algorithms is that, at the end of the day, I need this implemented using actual floating point.
You can go a very long way using discrete math though. I'm pretty sure it's doable to implement, say, a 3D slicer (to prepare layers/paths for 3D printing I mean) without using any floating point operation.
P.S: FWIW I was coding intros and demos using 3D effects on the Commodore Amiga and then on 386 PCs without using the 387 (the FP co-processor of the 386, when present). I'm not saying it's useful to play games in 4K: what I'm saying is that there are certainly applications where formally verified algos using integer math do make sense.
Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
#18This seems like very cool work. I'm sorry if I missed it: I'm still not sure how we go from verified proof (Great!) to an implementation (by LLM or by Human) which you're sure actually conforms to the proof? How do we know that the implementation maps precisely to the description within the proof?
Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
#19This seems like very cool work. I'm sorry if I missed it: I'm still not sure how we go from verified proof (Great!) to an implementation (by LLM or by Human) which you're sure actually conforms to the proof? How do we know that the implementation maps precisely to the description within the proof?
Both the implementation and the proof are written in Lean.
In the files I reference here https://github.com/schildep/verified-3d-mesh-intersection#mi...
there are theorems about the function that does the mesh intersection computation.
The implementation is in the CSG/Impl folder. The proof is in the CSG/Proof folder. They are imported and tied together in the human reviewed file. Lean checks that these theorems in the human reviewed file are proven via the proofs.
Re: Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code
#20Honestly I think I'd have an easier time understanding 1000s of lines of slop than 93 lines of proofs lol.
Does anyone have any recommended learning resources for this type of thing? Skimming the repo, it looks like a lot of unicode and math terminology, but this project seems really compelling to me.