Birbla

Comments

Hacker News

Would you still be able to deal with coplanar faces if you were to expand this to floats?

by _bent

This is a really cool project. Love it. Why not extend to union, difference, and xor? Is that exercise left to the reader or is it not tractable? ;)

I'm also curious if you've consider fuzz testing this system to verify the results.

by peetle

Ok, that's very cool. I don't yet grasp exactly how this deals with numerical stability - the one true enemy of mesh-based CSG operations

by swiftcoder

> 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 theory behind proof kernels that they must be small because they have to be trusted and verifiable by a human. Otherwise the whole system breaks.

How does one trust an LLM generated kernel is proving the right things?

by agentultra

This 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?

by brandonpelfrey

This is really neat. I think CSG is one of the more intuitive ways to build 3d environments (especially 'indoor' ones). No geometry is ever destroyed in a proper CSG workflow. A hierarchy of brushes makes it possible to very rapidly iterate parameters like how long a hallway is or the time it takes to get from one objective to another. Often, you only have to apply a transform to a single brush to affect something that would take a non-CSG workflow an entire afternoon to recover from.

The current story with CSG around commercial game engines is pretty awful. Unity has some 3rd party options that can work well but they're also glitchy and don't integrate well with the other parts of the ecosystem. For a while I thinking about building my own CSG implementation but the exact things this project solved were what was stopping me. The EditorWindow integration stuff is not as scary to me (although it is painful). The advanced geometry and set operations is what kept me from trying. It appears that dragon has been (at least partially) slain.

by bob1029

Note that the claims are about the kernel that computes the mesh intersection, not the web demo: While the kernel is formally verified, the UI and glue code (that call the kernel) are not. I once hit a bug that looked like there were holes in the resulting mesh: I found that it was an overflow in the glue code (now fixed) that converts the exact rationals coordinates of the output mesh, for which we prove the specification, to floats before sending them to the GPU. All geometry is happening inside the kernel, for which we know the specification holds.

by permute

Join the discussion

Write your take first — we'll ask for email only when you're ready to publish.

Sign in
  • Hacker News
  • Would you still be able to deal with coplanar faces if you were to expand this to floats?
    by _bent
  • This is a really cool project. Love it. Why not extend to union, difference, and xor? Is that exercise left to the reader or is it not tractable? ;)

    I'm also curious if you've consider fuzz testing this system to verify the results.

    by peetle
  • How does it compare against https://github.com/elalish/manifold in performance and zero corruption?

    I spent a lot of time making elalish/manifold work in Godot Engine and it is now a method in Blender too.

    https://manifoldcad.org

    If it helps, feel free to use the apache2 licensed unit tests that were generated in manifold development https://github.com/elalish/manifold/tree/master/test

    by iFire
  • Ok, that's very cool. I don't yet grasp exactly how this deals with numerical stability - the one true enemy of mesh-based CSG operations
    by swiftcoder
  • > 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 theory behind proof kernels that they must be small because they have to be trusted and verifiable by a human. Otherwise the whole system breaks.

    How does one trust an LLM generated kernel is proving the right things?

    by agentultra
  • This 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?
    by brandonpelfrey
  • This is really neat. I think CSG is one of the more intuitive ways to build 3d environments (especially 'indoor' ones). No geometry is ever destroyed in a proper CSG workflow. A hierarchy of brushes makes it possible to very rapidly iterate parameters like how long a hallway is or the time it takes to get from one objective to another. Often, you only have to apply a transform to a single brush to affect something that would take a non-CSG workflow an entire afternoon to recover from.

    The current story with CSG around commercial game engines is pretty awful. Unity has some 3rd party options that can work well but they're also glitchy and don't integrate well with the other parts of the ecosystem. For a while I thinking about building my own CSG implementation but the exact things this project solved were what was stopping me. The EditorWindow integration stuff is not as scary to me (although it is painful). The advanced geometry and set operations is what kept me from trying. It appears that dragon has been (at least partially) slain.

    by bob1029
  • Note that the claims are about the kernel that computes the mesh intersection, not the web demo: While the kernel is formally verified, the UI and glue code (that call the kernel) are not. I once hit a bug that looked like there were holes in the resulting mesh: I found that it was an overflow in the glue code (now fixed) that converts the exact rationals coordinates of the output mesh, for which we prove the specification, to floats before sending them to the GPU. All geometry is happening inside the kernel, for which we know the specification holds.
    by permute