Xác thực hình học 3D: Tin tưởng 93 dòng đặc tả thay vì 1.000 dòng mã AI

Theo hiểu biết của tôi, đây là bản triển khai được xác minh hình thức đầu tiên cho một phép toán hình học khối xây dựng (CSG) 3D: giao lưới (mesh intersection), được thực hiện bằng Lean 4 và được xác minh dựa trên một đặc tả ngắn gọn giúp xác định chính xác bề mặt của lưới kết quả và đảm bảo các điều kiện về tính hợp lệ thực tế của quá trình tam giác hóa. (Xem thêm các công trình liên quan.)

Dự án này cũng là một thử nghiệm trong việc tránh phải tin tưởng vào mã nguồn do AI tạo ra. Người đánh giá chỉ cần đọc 93 dòng đặc tả hình thức và chạy trình kiểm tra Lean như mô tả bên dưới để chứng nhận tính đúng đắn của nhân (kernel), thay vì phải kiểm tra hơn 1000 dòng mã triển khai phức tạp do AI viết. Để chứng minh tính đúng đắn, AI đã tự động viết hơn 60.000 dòng chứng minh bằng Lean, những dòng này cũng không bao giờ cần con người kiểm tra. Trình kiểm tra Lean đảm bảo sự tuân thủ đặc tả tại thời điểm biên dịch, với mức độ tin tưởng bằng không vào bất kỳ LLM nào. Điều này cho phép chúng ta coi phần triển khai và các chứng minh như một "hộp đen". Tôi đã hướng dẫn tác nhân (agent) thông qua các cột mốc được mô tả bên dưới để đạt được kết quả trình bày tại đây.

Bản demo trên web

Hãy thử nghiệm bản demo trên web được xây dựng dựa trên nhân đã xác minh, nơi bạn có thể thực hiện phép giao các lưới mẫu hoặc nhập và giao các lưới từ tệp STL. Mã Lean đã biên dịch chạy cục bộ trong trình duyệt của bạn; không có dữ liệu nào được gửi đến máy chủ. Lưu ý rằng mặc dù nhân đã được xác minh hình thức, nhưng giao diện người dùng (UI) và mã kết nối (glue code) thì không.

Bản triển khai của chúng tôi chậm hơn nhiều so với các bản triển khai giao lưới hiện đại nhất: mất 24 giây để tính toán chính xác phép giao của hai mô hình Stanford bunny với 70 nghìn tam giác. Trong dự án này, chúng tôi ưu tiên giảm thiểu nỗ lực đánh giá tính đúng đắn của con người hơn là hiệu suất. Lưu ý rằng khoảng cách hiệu suất này không phải là hạn chế cơ bản của phần mềm được xác minh hình thức, vốn về nguyên tắc có thể nhanh như phần mềm thông thường. Xem chi tiết.

Các lưới đầu ra được đảm bảo đáp ứng các thuộc tính mô tả bên dưới, nhưng việc tạo lưới có thể chưa tối ưu so với các tiêu chí khác mà chúng tôi chưa hình thức hóa; ví dụ, nó có thể tạo ra một lưới mịn hơn mức cần thiết.

Bối cảnh và hình thức hóa

Một lưới tam giác là một tập hợp các tam giác, thường được kỳ vọng tạo thành một bề mặt kín không tự cắt, cùng với các điều kiện hợp lệ khác mà chúng tôi sẽ thảo luận bên dưới.

Con người theo trực giác liên tưởng lưới tam giác với một "khối rắn", tức là một thể tích trong không gian 3D: tập hợp tất cả các điểm không nằm trên bề mặt mà nằm "bên trong" lưới. ("Bên trong" có thể được mô tả toán học bằng cách đếm số lần giao tia có dấu.)

Khái niệm về khối rắn này cho phép chúng ta hiểu kết quả đầu ra của các thuật toán như thuật toán giao lưới nên trông như thế nào, ngay cả khi việc triển khai trên cấu trúc dữ liệu lưới thực tế rất phức tạp và phải xử lý nhiều trường hợp hình học đặc biệt bằng mã chuyên biệt.

Từ một thuật toán giao lưới, chúng ta kỳ vọng rằng phép giao tập hợp các khối rắn của các lưới đầu vào hợp lệ sẽ là khối rắn của lưới đầu ra và lưới đầu ra cũng là một lưới hợp lệ. (Chúng ta cũng kỳ vọng thuật toán phát hiện và báo cáo chính xác nếu các đầu vào không hợp lệ.)

Điều này xác định chính xác bề mặt của lưới kết quả như là ranh giới của các khối rắn đã giao.

Các thuật toán hoạt động trên lưới tam giác có thể tính toán hiệu quả các lưới đại diện cho các khối rắn mà chúng ta hình dung, nhưng các ngôn ngữ lập trình thông thường không thể diễn đạt "khối rắn" một cách tường minh hoặc đưa ra các khẳng định về chúng, vì đây là các tập hợp vô hạn. Trong Lean, điều này là khả thi và chúng ta có thể, ví dụ, giao các tập hợp vô hạn như vậy hoặc chứng minh rằng hai tập hợp vô hạn là bằng nhau. Hơn nữa, Lean cho phép chúng ta chứng minh rằng một hàm thỏa mãn một điều kiện cho tất cả các lưới đầu vào có thể có, trong khi các ngôn ngữ lập trình thông thường chỉ cho phép chúng ta kiểm tra xem hàm đó có thỏa mãn điều kiện cho các đầu vào cụ thể hay không.

Chúng tôi định nghĩa tính hợp lệ của lưới để nắm bắt các điều kiện thường được mong đợi bởi các công cụ xử lý lưới trong thực tế - bề mặt kín (watertight), bao quanh một khối rắn với độ bội một, định hướng hướng ra ngoài nhất quán, không có tam giác suy biến, không tự giao - với một sự nới lỏng: bề mặt có thể tự chạm vào chính nó, không phải ở phần bên trong của các mặt mà dọc theo các cạnh và đỉnh. Vì vậy, tính đa tạp 2 chiều (2-manifoldness) nghiêm ngặt là không bắt buộc. Xem lý do tại sao một thuật toán giao luôn tạo ra lưới đa tạp là không khả thi.

Đánh giá tối thiểu của con người mà không cần tin tưởng AI

Để chứng nhận tính đúng đắn của nhân, vốn kiểm tra các điều kiện tiên quyết về tính hợp lệ của đầu vào và tính toán phép giao lưới, người đánh giá chỉ cần đọc 93 dòng đặc tả hình thức và chạy trình kiểm tra Lean như mô tả bên dưới. Người đánh giá có thể bỏ qua hơn 1000 dòng mã triển khai thuật toán phức tạp do AI viết. Trình kiểm tra Lean đảm bảo sự tuân thủ đặc tả tại thời điểm biên dịch, với các giả định tin tưởng bằng không vào bất kỳ LLM nào.

Sự nén và đơn giản hóa từ phần triển khai sang đặc tả này là khả thi vì nhiều thứ mà phần triển khai phải xử lý có thể được tách biệt hoàn toàn khỏi đặc tả:

Nếu trong một commit tương lai, chúng tôi cải thiện thêm hiệu suất thời gian chạy hoặc chất lượng của lưới đầu ra, đặc tả đã được đánh giá vẫn giữ nguyên và chúng tôi đạt được tính đúng đắn đối với nó mà không cần đánh giá lại. Xem thêm cách tôi phát triển dự án này chỉ thông qua việc định hình đặc tả này.

Phát triển

Trong quá trình phát triển, tôi chỉ kiểm soát một đặc tả nhỏ, để các chứng minh và phần triển khai chi tiết như một hộp đen cho các tác nhân. Tôi bắt đầu với một đặc tả mà tôi ước tính là tương đối dễ triển khai và chứng minh hình thức tính đúng đắn, sau đó mới tăng dần các yêu cầu. Trong mỗi bước được liệt kê bên dưới, tôi đã yêu cầu tác nhân triển khai và chứng minh hình thức đặc tả đó. Sự tinh chỉnh từng bước này cho phép tôi ủy quyền các phần công việc lớn cho các tác nhân, đồng thời nhận phản hồi rằng đặc tả của tôi là có thể thỏa mãn và xác minh tiến độ của các tác nhân hướng tới mục tiêu cuối cùng của tôi tại mỗi cột mốc. Tôi đã hướng dẫn các tác nhân viết các chứng minh không hình thức trước khi tiến hành hình thức hóa.

Tôi bắt đầu bằng việc yêu cầu một tác nhân hình thức hóa một bài báo cung cấp khung toán học để mô tả các khối rắn dựa trên các chuỗi đơn hình (simplicial chains). Điều này mang lại cho tôi một kết quả tồn tại hình thức mà không cần triển khai cụ thể (xem CSG/Legacy/ChainIntersectionExistence.lean).

F. R. Feito và M. Rivero, "Geometric modelling based on simplicial chains," Computers & Graphics 22(5), 611–619 (1998). doi:10.1016/S0097-8493(98)00067-3

Sau đó, tôi yêu cầu một bản triển khai kèm chứng minh tính đúng đắn (CSG/Legacy/ChainIntersectionAlgorithm.lean). Bản này đã thỏa mãn một đặc tả hình thức tương tự như mục tiêu cuối cùng của tôi. Tuy nhiên, các tam giác chồng lấp và các vấn đề khác vẫn được cho phép và thực sự đã xảy ra.

Sau đó, tôi chỉ định các hạn chế cho lưới đầu ra (tương tự như trạng thái hiện tại của WellFormedMesh) để ngăn chặn các loại vấn đề từ bản triển khai đầu tiên. Tôi cũng đưa ra một hạn chế về vị trí tổng quát (general position) trên các đầu vào mà sau này tôi đã loại bỏ, để tránh việc phần triển khai phải xem xét quá nhiều trường hợp đặc biệt trong bước này. Các yêu cầu nghiêm ngặt hơn buộc phải triển khai lại hoàn toàn, nhưng một phần khung hình thức có thể được tái sử dụng.

Sau đó, tôi loại bỏ các hạn chế về vị trí tổng quát trên các đầu vào, buộc tác nhân phải xử lý chính xác tất cả các trường hợp hình học đặc biệt.

Sau đó, tôi yêu cầu các tác nhân tối ưu hóa phần triển khai bằng các cấu trúc phân cấp thể tích bao (bounding volume hierarchies) và các tối ưu hóa khác. Tôi không hình thức hóa yêu cầu về thời gian chạy, nhưng Lean đã xác minh rằng việc tối ưu hóa vẫn thỏa mãn cùng một đặc tả hình thức. Vì vậy, trong bước này, tôi không cần phải đánh giá lại bất cứ điều gì để đảm bảo tính đúng đắn.

Cuối cùng, tôi củng cố đặc tả hơn nữa và làm cho nó dễ đánh giá hơn.

Quá trình này dẫn đến đặc tả mà bạn có thể thấy ở cấp cao nhất của thư mục CSG/, chứng minh tại CSG/Proof/ và triển khai tại CSG/Impl/.

Đối với hầu hết các bước trên, tôi đã sử dụng Claude Opus 4.8. Đối với một số bước, tôi sử dụng Fable 5 để tạo chiến lược chứng minh không hình thức ban đầu và sau đó yêu cầu Opus viết các chứng minh hình thức và triển khai. Một số bước trên đã mất hơn 24 giờ làm việc tự động của tác nhân.

So sánh với "vibecoding" với đặc tả không hình thức

Trái ngược với "vibecoding" thông thường, việc kết hợp AI với xác minh hình thức mang lại những đảm bảo nghiêm ngặt mà chúng ta biết sẽ giữ vững cho tất cả các đầu vào và được thực thi với mỗi sửa đổi tiếp theo của chương trình. Nhưng giống như "vibecoding" thông thường, với mỗi bước, quá trình phát triển có thể tích lũy một số "nợ": cả phần triển khai và các chứng minh mà tôi có được đều không sạch sẽ và không tuân theo một thiết kế gắn kết như khi được kiểm soát bởi một con người có cái nhìn tổng quan về mọi thứ. Hơn nữa, có một số ràng buộc mà chúng tôi chưa hình thức hóa ở đây, chẳng hạn như hiệu suất thời gian chạy hoặc cách các mặt của khối rắn đầu ra được tam giác hóa ngoài điều kiện hợp lệ. Do đó, các ràng buộc này khó kiểm soát như với "vibecoding" thông thường.

Để so sánh, tôi đã đưa cho Opus 4.8 một mô tả không hình thức về đặc tả và yêu cầu nó triển khai bằng C++. Độ dài của phần triển khai không bao gồm các bài kiểm tra, mã kết nối, v.v., nằm trong cùng phạm vi 1000+ dòng như bản triển khai Lean. Mặc dù nó đã viết các bài kiểm tra đơn vị và lặp đi lặp lại việc sửa lỗi triển khai của chính mình, nhưng khi được kiểm tra bởi một tác nhân độc lập so sánh với bản triển khai Lean đã xác minh hình thức, 3 lỗi riêng biệt đã được phát hiện trong nhân hình học C++ và tái hiện trên các đầu vào cụ thể. Tất cả các lỗi này đều hiếm gặp và gần như không thể phát hiện bằng kiểm thử hộp đen. Việc đánh giá đối kháng lặp đi lặp lại mã nguồn bởi các tác nhân khác dựa trên đặc tả không hình thức có thể đã phát hiện ra các lỗi này. Nhưng nếu không có xác minh hình thức, không thể biết chắc chắn rằng không còn lỗi nào khác trong phần triển khai. (Nhân C++ có ít nhất 3 lỗi riêng biệt đã được tái hiện: 1. Trong một số cấu hình nhất định nơi một đỉnh của lưới hợp lệ nằm trên cả cạnh của một phần khác của lưới và mặt của một lưới hợp lệ khác. 2: Trên các lưới đầu vào hợp lệ khi một chuỗi các bài kiểm tra giao tia trong các tính toán nội bộ đều vô tình chạm vào các cạnh tam giác. 3: Trong một số cấu hình nhất định nơi một mặt lớn bị cắt bởi nhiều đặc điểm nhỏ.)

Triển khai một thuật toán giao lưới 3D chính xác. Viết bằng C++, biên dịch sang wasm, tạo ra một sản phẩm mà tôi có thể chơi cùng. Điều quan trọng là nhân, một hàm đơn giản, nằm trong một tệp riêng biệt khép kín, nhân hình học được tách biệt khỏi tất cả các mã kết nối. (Tệp này chỉ phụ thuộc vào một bản triển khai số lớn/số hữu tỉ chính xác riêng biệt, tệp riêng biệt), Hàm này chỉ nên nhận các lưới dưới dạng mảng các tam giác với tọa độ chính xác làm đầu vào/đầu ra.

Hàm này nên kiểm tra xem các đầu vào có phải là lưới hợp lệ theo nghĩa bên dưới hay không và tạo thông báo lỗi nếu không. Chỉ chạy phép giao nếu các đầu vào hợp lệ.

Định nghĩa của chúng tôi về "lưới hợp lệ" nắm bắt các điều kiện thường được mong đợi bởi các công cụ xử lý lưới trong thực tế - bề mặt kín, bao quanh một khối rắn với độ bội một với định hướng hướng ra ngoài nhất quán, không có tam giác suy biến, không tự giao - với một sự nới lỏng: bề mặt có thể tự chạm vào chính nó, không phải ở phần bên trong của các mặt mà dọc theo các cạnh và đỉnh (vì vậy tính đa tạp 2 chiều nghiêm ngặt là không bắt buộc). Sự nới lỏng này là cần thiết để phép giao của bất kỳ hai lưới hợp lệ nào cũng là hợp lệ.

Mọi thứ nên được tính toán bằng số hữu tỉ. Nó nên xử lý chính xác tất cả các trường hợp đặc biệt. Luôn tạo ra một lưới hợp lệ làm đầu ra nếu các đầu vào hợp lệ. Bạn có thể giao các tam giác theo cặp (sử dụng tối ưu hóa bvh), tạo ra các đa giác và tam giác hóa bằng steiner fans.

Nhược điểm của việc kết hợp xác minh hình thức với vibecoding:

Khi tôi viết những dòng này, khả năng của các tác nhân AI trong việc thực hiện các nhiệm vụ lớn được xác định rõ ràng đang tăng nhanh theo từng phiên bản mô hình. Khả năng của con người trong việc đánh giá đầu ra của chúng và suy luận về chúng thì không. Tôi hy vọng chúng ta có thể sử dụng xác minh hình thức cùng với các phương pháp khác như một đòn bẩy để duy trì quyền kiểm soát.

Xây dựng và kiểm tra