How hard would it be to extend this proof to real coordinates? Is that ‘just’ a matter of formalizing some known, tedious math, or would it require new work?
For example, if one allows one coordinate of one corner to be non rational, I think the set of potential output coordinates used would be a subset of the reals (depending on the value of that coordinate), and to my (possibly very bad) intuition, formalizing that subset doesn’t feel like a hard problem.
Allowing two of such real points would make things more tedious, potentially way more tedious, but again, doesn’t feel like it would be impossible to handle.
There are two things here: The proof and how you would represent that in a program that you actually can run.
From the math side, I am confident that the construction and proof can be extended to the real numbers and that can be formalized in lean with minimal changes in the existing proof. (Mathematically speaking, we can replace the rationals with any ordered field and the proof should run through.)
I chose to model the problem with rational numbers because the intersections of polygons with rational coordinates have rational coordinates and rational numbers can easily be represented in the computer.
To have a computable implementation with real numbers, you have to make some choice about which part of the real numbers you want to be able to represent in the computer.
For example if sqrt(2) and sqrt(3) is important to you, I think you can have a program that can represent them if they occur in any input coordinates and can represent any resulting coordinates exactly symbolically besides the rational numbers (I think this requires minimal changes in the code, the required lean machinery to work with such numbers can be separated from the geometrical code), but a program can’t be able to represent all real numbers exactly since there are too many of them.
Another interesting direction to take this would be to allow spline segments instead of line segments, since intersections of splines with rational coordinates can have non rational coordinates, but I think can still be represented exactly in the computer. This would require a bigger change and would be interesting geometrically.
Yes, the core supports exact rationals. This is easier to deal with in formal verification than floating point.
I made the UI snap to a fixed precision, such that its easy to reproduce special cases with overlapping edges, coinciding vertices etc. that make up much of the complexity of the algorithm.
In a past life i tried to implement Delaunay triangulation in floating point for data that can come in a rotated square grid. Normal precision doesn't work in that case. I learned a lot about arbitrary precision numbers doing that. The question about floats here gave me flashbacks.
I am eager for a lean equivalent of flocq in rocq. When I did some lean verification of numerical algorithms I did the same thing with rationals or the reals from mathlib. The big gap between that and the actual code is the lack of a solid theory library to pull in that would give me IEEE floats that is at the same level of quality as Flocq. I’m eager for that to come along (unless it has and I just haven’t found it yet).
I think to do efficient formally verified geometry with floating point we would also need something like Shewchuk robust predicates. (I worked with them in the past to write robust software that is not formally verified. Did not read up, if there is a formally verified library for them.) Shewchuk robust predicates give certain consistency guarantees that are nice to have when implementing computational geometry with floating points and I think can be formalized.
This is a great use for AI! Calculating intersections is tedious and there are an surprising number of edge cases that are tedious to track down and fix.
Thanks! I am currently working on a follow up project for 3D polyhedrons for which the case handling really starts to get tedious. It's nice when AI can handle it without humans having to read the code and many unit tests to trust it.
Sure, what the program does is not interesting by itself, neither is that you can use AI to create programs to do polygon intersection.
The main feature, that I hope is interesting in this submission, is that the program is formally verified and how I used formal verification together with AI to create it.
Formal verification means that a mathematical proof is provided that the program satisfies a specification. And that proof is checked automatically by a deterministic system, the lean checker, which we can trust, in constrast to error prone LLMs.
I gave the agent a formal specification m1.interior ∩ m2.interior = result.interior and it produced an implementation together with such a formal proof. With this approach we can treat much of the work of the agent as a black box, which we don't have to review to judge correctness.
I think the project shows that as AI agents get more capable, an approach like this is starting to get practical for certain problems like polygon intersection for which there is a concise way to specify the problem.
Nice I get it now.
And from your usage, a natural question is how much effort was put by the AI to find the verified answer ? Did it need to run significantly longer or less that without these constraints ?
Opus 4.8 ran autonomously for about 8 hours to provide program and proof of correctness, given the formal specification. And in previous experiments, Opus 4.7 failed and I was only able to do it using that model when I cut the work for the agents in smaller steps.
Much of the work the agent is to provide the proof of correctness. The upside is that less time is needed for human review and we can guarantee the absence of bugs that might be expensive when they come up in production.
Historically formal verification was only worth it for very critical software. In the readme I reference related work from NASA, that implemented and verified a different algorithm concerned with polygons, with the intended application to compute keep out zones for autonomous vehicles. This was 2021 before capable LLMs and in the paper they mention that they manually wrote 700 lemmas to produce such a formal proof manually.
I hope that as it gets cheaper now, formal verification is used more widely.
Yes, the webassembly is compiled from lean. The JS UI that calls the webassembly is not built from lean and not formally verified. So a human reviewer that does not trust the code, needs to review the formal spec and the UI code. But the geometry with rare special cases that we want to treat correctly happens in the verified core.
How hard would it be to extend this proof to real coordinates? Is that ‘just’ a matter of formalizing some known, tedious math, or would it require new work?
For example, if one allows one coordinate of one corner to be non rational, I think the set of potential output coordinates used would be a subset of the reals (depending on the value of that coordinate), and to my (possibly very bad) intuition, formalizing that subset doesn’t feel like a hard problem.
Allowing two of such real points would make things more tedious, potentially way more tedious, but again, doesn’t feel like it would be impossible to handle.
There are two things here: The proof and how you would represent that in a program that you actually can run.
From the math side, I am confident that the construction and proof can be extended to the real numbers and that can be formalized in lean with minimal changes in the existing proof. (Mathematically speaking, we can replace the rationals with any ordered field and the proof should run through.)
I chose to model the problem with rational numbers because the intersections of polygons with rational coordinates have rational coordinates and rational numbers can easily be represented in the computer.
To have a computable implementation with real numbers, you have to make some choice about which part of the real numbers you want to be able to represent in the computer. For example if sqrt(2) and sqrt(3) is important to you, I think you can have a program that can represent them if they occur in any input coordinates and can represent any resulting coordinates exactly symbolically besides the rational numbers (I think this requires minimal changes in the code, the required lean machinery to work with such numbers can be separated from the geometrical code), but a program can’t be able to represent all real numbers exactly since there are too many of them.
Another interesting direction to take this would be to allow spline segments instead of line segments, since intersections of splines with rational coordinates can have non rational coordinates, but I think can still be represented exactly in the computer. This would require a bigger change and would be interesting geometrically.
Does this use integer coordinates or floating point coordinates?
It uses exact rational coordinates, not floating-point coordinates in the verified core. See: https://github.com/schildep/verified-polygon-intersection/bl...
Yes, the core supports exact rationals. This is easier to deal with in formal verification than floating point.
I made the UI snap to a fixed precision, such that its easy to reproduce special cases with overlapping edges, coinciding vertices etc. that make up much of the complexity of the algorithm.
In a past life i tried to implement Delaunay triangulation in floating point for data that can come in a rotated square grid. Normal precision doesn't work in that case. I learned a lot about arbitrary precision numbers doing that. The question about floats here gave me flashbacks.
I can relate. Working in floating point hardware design gave me an irrational distaste for it. The horrors!
I am eager for a lean equivalent of flocq in rocq. When I did some lean verification of numerical algorithms I did the same thing with rationals or the reals from mathlib. The big gap between that and the actual code is the lack of a solid theory library to pull in that would give me IEEE floats that is at the same level of quality as Flocq. I’m eager for that to come along (unless it has and I just haven’t found it yet).
Thanks for the pointer, I will look into it.
I think to do efficient formally verified geometry with floating point we would also need something like Shewchuk robust predicates. (I worked with them in the past to write robust software that is not formally verified. Did not read up, if there is a formally verified library for them.) Shewchuk robust predicates give certain consistency guarantees that are nice to have when implementing computational geometry with floating points and I think can be formalized.
This is a great use for AI! Calculating intersections is tedious and there are an surprising number of edge cases that are tedious to track down and fix.
Thanks! I am currently working on a follow up project for 3D polyhedrons for which the case handling really starts to get tedious. It's nice when AI can handle it without humans having to read the code and many unit tests to trust it.
I'm not sure if the feature is intersection or the use of AI to write it...
Polygon intersection is a well known thing. Video games and geographic information systems (topology) do that for decades.
Tell me more, what should I look at ?
Sure, what the program does is not interesting by itself, neither is that you can use AI to create programs to do polygon intersection.
The main feature, that I hope is interesting in this submission, is that the program is formally verified and how I used formal verification together with AI to create it.
Formal verification means that a mathematical proof is provided that the program satisfies a specification. And that proof is checked automatically by a deterministic system, the lean checker, which we can trust, in constrast to error prone LLMs.
I gave the agent a formal specification m1.interior ∩ m2.interior = result.interior and it produced an implementation together with such a formal proof. With this approach we can treat much of the work of the agent as a black box, which we don't have to review to judge correctness.
I think the project shows that as AI agents get more capable, an approach like this is starting to get practical for certain problems like polygon intersection for which there is a concise way to specify the problem.
Nice I get it now. And from your usage, a natural question is how much effort was put by the AI to find the verified answer ? Did it need to run significantly longer or less that without these constraints ?
Yes, it runs significantly longer.
Opus 4.8 ran autonomously for about 8 hours to provide program and proof of correctness, given the formal specification. And in previous experiments, Opus 4.7 failed and I was only able to do it using that model when I cut the work for the agents in smaller steps.
Much of the work the agent is to provide the proof of correctness. The upside is that less time is needed for human review and we can guarantee the absence of bugs that might be expensive when they come up in production.
Historically formal verification was only worth it for very critical software. In the readme I reference related work from NASA, that implemented and verified a different algorithm concerned with polygons, with the intended application to compute keep out zones for autonomous vehicles. This was 2021 before capable LLMs and in the paper they mention that they manually wrote 700 lemmas to produce such a formal proof manually. I hope that as it gets cheaper now, formal verification is used more widely.
Impressive work. It's nice to see LEAN being used for real-world algorithms.
Thanks! Yes, I hope AI and Lean will enable formally verified practical software.
Is the web demo compiled from the lean?
Yes, the webassembly is compiled from lean. The JS UI that calls the webassembly is not built from lean and not formally verified. So a human reviewer that does not trust the code, needs to review the formal spec and the UI code. But the geometry with rare special cases that we want to treat correctly happens in the verified core.
Nice. So is the js/lean interface using exact rationals?
Yes