ProofOfThought: Suy luận dựa trên LLM sử dụng chứng minh định lý Z3

• ProofOfThought kết hợp mô hình ngôn ngữ lớn (LLM) với bộ chứng minh định lý Z3 để hỗ trợ suy luận mạnh mẽ và có thể diễn giải
• Dự án này cung cấp kết quả suy luận chính xác và đáng tin cậy cho truy vấn ngôn ngữ tự nhiên
• Thông qua API Python cấp cao, các nhà phát triển có thể dễ dàng triển khai và thử nghiệm các tác vụ suy luận phức tạp
• Thông qua Z3DSL, dự án cũng cung cấp khả năng tiếp cận DSL cấp thấp dựa trên JSON, cho phép tùy biến linh hoạt
• Việc được giới thiệu tại Sys2Reasoning Workshop NeurIPS 2024 cho thấy lợi ích thực tiễn hóa của các thành tựu nghiên cứu mới nhất

---

Giới thiệu dự án mã nguồn mở ProofOfThought

ProofOfThought là một thư viện suy luận mã nguồn mở áp dụng phương pháp tổng hợp chương trình neuro-symbolic (thần kinh-ký hiệu) kết hợp mô hình ngôn ngữ lớn (LLM) với bộ chứng minh định lý Z3. Điểm có ý nghĩa quan trọng cả trong ứng dụng thực tế lẫn nghiên cứu là khả năng cung cấp kết quả suy luận vững chắc và có thể diễn giải cho các bài toán phức tạp trong thế giới thực.

Với đặc tính mã nguồn mở, bất kỳ ai cũng có thể tự do sử dụng cho nghiên cứu, dịch vụ và phát triển. So với các hệ thống suy luận đơn thuần dựa trên LLM hiện có, dự án có ưu điểm là dễ xác minh quá trình suy luận và phân tích lỗi. So với các hệ thống suy luận khác, đặc trưng nổi bật là tính minh bạch về cấu trúc theo luồng: đầu vào ngôn ngữ tự nhiên → tự động chuyển đổi thành chương trình logic → suy luận dựa trên Z3.

Kiến trúc hệ thống và các thành phần chính

• API cấp cao (z3dsl.reasoning) :

  • Thực hiện truy vấn suy luận dựa trên ngôn ngữ tự nhiên
  • Cung cấp giao diện Python dễ áp dụng ngay cả với người mới bắt đầu

• DSL cấp thấp (z3dsl) :

  • Cho phép truy cập bộ chứng minh định lý Z3 dựa trên JSON
  • Thuận lợi cho việc tùy biến phức tạp và xây dựng pipeline tự động hóa

Ví dụ các tính năng chính

• LLM chuyển truy vấn đầu vào thành biểu thức logic (chương trình ký hiệu)

• Thông qua bộ chứng minh Z3, tạo ra kết quả đúng/sai (yes/no) hoặc diễn giải dựa trên điều kiện

• Ví dụ:

  • Truy vấn: "Nancy Pelosi có công khai chỉ trích việc phá thai không?"
  • Kết quả: False (không)

• Cung cấp pipeline đánh giá (EvaluationPipeline):

  • Có thể đánh giá theo lô trên tập dữ liệu quy mô lớn
  • Tự động báo cáo như độ chính xác

Ứng dụng và trường hợp sử dụng

• Tự động hóa benchmark suy luận cho mục đích nghiên cứu
• Dịch vụ tự động chứng minh cho knowledge graph dựa trên LLM hoặc các bài toán logic bậc cao
• Có tiềm năng áp dụng vào nhiều dịch vụ AI như truy vấn chính sách phức tạp, tự động phân định tranh luận ngôn ngữ tự nhiên

Ý nghĩa nghiên cứu và đặc điểm

• Được trình bày tại workshop Sys2Reasoning của NeurIPS 2024
• Độ tin cậy dựa trên diễn giải ký hiệu giúp khắc phục giới hạn hiện có của LLM (sự bất định trong suy luận)
• Tính minh bạch và khả năng diễn giải của kết quả suy luận cùng căn cứ đi kèm là thế mạnh lớn cho phát triển dịch vụ thực tế

Kết luận

ProofOfThought kết hợp ưu điểm của LLM và bộ chứng minh định lý Z3 để mang lại giá trị thực tiễn cho các nhà phát triển và nhà nghiên cứu muốn xây dựng hạ tầng suy luận AI mạnh mẽ và có thể diễn giải. Giấy phép và cấu trúc của dự án được thiết kế phù hợp với hệ sinh thái mã nguồn mở, nên hấp dẫn cho cả nghiên cứu học thuật lẫn ứng dụng công nghiệp.

[GN⁺]

Ý kiến trên Hacker News

• Chia sẻ một trải nghiệm thú vị với Gemini 2.5 Pro. Khi đang thử giải hệ phương trình trên một hệ thống CAS trực tuyến nhưng CAS không hoạt động như mong đợi, người viết đã nhờ Gemini trợ giúp và Gemini đưa ra lời giải trực tiếp. Gemini giải thích rằng đã dùng gói sympy của Python. Tác giả chia sẻ ấn tượng rằng việc kết hợp một LLM mơ hồ với các công cụ nghiêm ngặt có thể tạo ra hiệu quả rất mạnh
  • Cảm giác này khá giống con người. Chúng ta yếu trong các phép tính phức tạp nhưng đã tạo ra những cỗ máy tính tuyệt vời để làm việc đó. Và sau rất nhiều nỗ lực, chúng ta cũng tạo ra được những chương trình dựa trên tính toán số để dự đoán văn bản khá ổn, dù vẫn kém ở các phép tính khó. Cuối cùng, chương trình này lại học được cách dự đoán việc tạo ra và sử dụng những chương trình giỏi tính toán số
  • Tôi thực sự thích sự kết hợp giữa LLM và sympy trong toán học. Nếu để LLM viết mã sympy, ta có thể tin rằng các phép biến đổi ký hiệu được thực hiện đúng. Bản thân mã nguồn cũng được giữ lại như một đầu ra để con người hoặc LLM có thể sửa dần và cải thiện, đồng thời có thể quản lý bằng lịch sử git, v.v. Việc vượt qua kiểm thử và xác minh giúp duy trì niềm tin vào độ chính xác toán học. Tôi cũng dùng các hàm trợ giúp để chuyển từ mã sympy sang latex một cách dễ dàng. Gần đây tôi cũng làm phần toán học liên quan đến thí nghiệm quantum eraser theo cách này. liên kết github
  • Tôi hiểu rằng theo dõi quá trình giải quyết vấn đề cùng LLM bằng công cụ là một cách làm ổn. Trên thực tế, nó hoạt động tốt hơn mong đợi. Nhưng không dùng CAS mà lại dẫn LLM đi làm toán thì giống như chuyển nhà bằng cách đi xe buýt nhiều chuyến thay vì dùng xe tải chở hàng. Quan điểm này là vậy dù bạn đã có sẵn vé xe buýt
• Nhấn mạnh rằng LLM suy cho cùng vẫn là mô hình ngôn ngữ thống kê. Theo kinh nghiệm, việc sinh chương trình logic, đặc biệt là mã nguồn Prolog, hoạt động tốt hơn mong đợi. Có lẽ vì Prolog từng được đưa vào xử lý ngôn ngữ tự nhiên mang tính ký hiệu và trong tập dữ liệu huấn luyện cũng có nhiều mẫu dịch. Cũng đáng cân nhắc thử cú pháp Datalog của Z3 thay vì cú pháp SMTLib. Khuyến nghị xem demo liên quan và cú pháp Z3 Datalog
  • Cú pháp Datalog trong Z3 khá tuyệt. Chúng tôi dùng SMT trong bài báo về grammars vì lý do chính là tính tương thích cao nhất với nhiều solver. Nhưng trong quá trình phản biện NeurIPS, chúng tôi đã thử và thấy cách đó cũng hoạt động tốt với PROLOG. Tôi cũng kỳ vọng nó sẽ chạy được với Datalog. liên kết bài báo, ví dụ datalog
• Đây là một hướng tiếp cận thú vị. Nhóm chúng tôi cũng từng làm một nguyên mẫu tương tự, dùng LEAN để mã hóa các chính sách vận hành doanh nghiệp. Trước tiên LLM chuyển cơ sở tri thức trong wiki nội bộ hoặc Google Docs thành mã LEAN. Sau đó chạy solver để kiểm tra tính nhất quán. Mỗi khi wiki được sửa, toàn bộ quy trình sẽ chạy lại, đóng vai trò như một kiểu linter cho quy trình. Tuy vậy, việc chuyển sang LEAN vẫn cần kỹ sư rà soát nên mới dừng ở mức nguyên mẫu. Nhưng đây là hướng đi đầy hứa hẹn cho các lĩnh vực đòi hỏi tuân thủ pháp lý và tài chính
  • Xin nhắc rằng rào cản của autoformalization thực sự rất cao. Trong bài báo NeurIPS 2025 của chúng tôi, chúng tôi đã định lượng và phân tích độ bất định của autoformalization trên các ngữ pháp được định nghĩa rõ. liên kết bài báo Nếu muốn thảo luận chi tiết hơn, cứ liên hệ bất kỳ lúc nào
  • Giới thiệu dành cho những ai thắc mắc LEAN là gì. Đây là Lean Theorem Prover do Microsoft tạo ra. liên kết dự án
  • Tôi tò mò về ví dụ thực tế. Muốn nghe xem những chính sách nào trong đời thực lại được mô tả chính xác đến mức có thể định nghĩa bằng LEAN
  • Có vẻ cách này rất hữu ích vì nó cho phép xác định một cách có hệ thống các hướng dẫn mâu thuẫn nhau
• Đây là một lĩnh vực nghiên cứu rất thú vị. Vài năm trước tôi từng dùng các bộ máy suy luận dựa trên logic và xác suất để kiểm tra xem các tiền đề có thực sự dẫn tới kết luận hay không. Tôi cũng dùng các agent để tổng hợp, hình thức hóa và phê bình tri thức miền. Nó không phải viên đạn bạc, nhưng có thể bảo đảm một mức độ chính xác nhất định. Tôi cho rằng một mức độ tính biểu tượng nào đó và khái niệm agent-as-a-judge sẽ có triển vọng trong tương lai. bài báo tham khảo
  • Tôi đã đọc nghiên cứu đó. Khá ấn tượng. Gần đây tôi cũng có trải nghiệm xây dựng một agent autoformalization trong AWS ARChecks. Chưa công khai, nhưng có những sản phẩm dùng được rộng rãi nên cũng đáng tham khảo AWS blog
  • Tôi cho rằng dùng Agent/LLM làm giám khảo sẽ có thiên lệch và chỉ phù hợp để bootstrap. Khi hiệu năng đủ cao, giám khảo LLM sẽ trở thành giới hạn nhân tạo, nên cuối cùng vẫn phải chuyển sang giám khảo là chuyên gia con người hoặc oracle tất định
• Có nhắc đến việc kernel rolling kiểu knife-edge của RHEL được dùng trong proof of concept
• Người viết cảm thấy repository thiếu mô tả chi tiết, có thể vì nó đóng vai trò như sản phẩm phụ trợ cho bài báo. Về bản chất, nó giống một API để cho LLM thử tạo chương trình Z3. Mục tiêu là khiến nó biểu diễn các truy vấn thế giới thực một cách logic, bao gồm đầy đủ sự kiện, quy tắc suy luận và mục tiêu. Chức năng giám sát nằm ở chỗ có thể đọc trực tiếp mô tả logic và chạy solver để kiểm tra đúng/sai. Điểm gây nghi ngờ là: ai sẽ đọc từng quy tắc SMT và đối chiếu với góc nhìn thực tế, ai sẽ xác minh các giá trị hằng, và liệu LLM có vô tình hoặc vì muốn đạt mục tiêu mà thêm vào các quy tắc lệch khỏi logic hay thực tế hay không. Trong bài báo, họ ghi nhận 51% false positive theo benchmark logic, đây là con số đáng ngạc nhiên là rất cao, được hiểu như tín hiệu cho thấy LLM yếu trong việc mô hình hóa logic hoặc tạo ra quy tắc chưa đầy đủ. Phần đánh giá còn mỏng nên chưa giải thích rõ tại sao điều đó xảy ra
  • Có ý kiến cho rằng bài báo này được làm bằng GPT-4o từ năm ngoái, và với các mô hình mới hơn thì tình hình đã cải thiện đáng kể. Chẳng hạn trong bài báo gần đây Tab 1, họ so sánh hiệu năng dạng văn bản và dạng SMT. o3-mini cho thấy sự khớp khá tốt giữa text reasoning và kết quả trên SMT. Trong sản phẩm thương mại AWS Automated Reasoning Checks, họ xây dựng mô hình miền, xác minh nó, rồi ở bước sinh câu trả lời, các cặp Q/A của LLM sẽ trải qua xác minh nghiêm ngặt bằng solver để kiểm tra có tuân thủ chính sách hay không. Nhờ đó, họ nhấn mạnh có thể bảo đảm hơn 99% tính hợp lệ liên quan đến chính sách của các cặp Q/A AWS blog
• Đây là câu hỏi xem cách hiểu của tôi có đúng không. Nếu cấu trúc là đầu ra xác suất của LLM được chuyển sang mô hình logic, thì chẳng phải vẫn chỉ là “rác vào thì rác ra” sao, người viết bày tỏ nghi ngờ
  • Logic hình thức đóng vai trò như một bộ lọc. Tức là “rác vào, rác đã được lọc đi ra”. Một phép ví von được đưa ra là tiến hóa cũng giống như các đột biến ngẫu nhiên “rác” được môi trường tự nhiên sàng lọc
  • Có ý kiến cho rằng không phải lúc nào cũng ra “rác”. Vì khá thường xuyên nó tạo ra đầu ra hữu ích nên điều đó có ý nghĩa
  • Đây là vấn đề đánh giá mang tính chủ quan. Những thứ nhân loại tạo ra trong hàng nghìn năm qua cũng đều có thể bị coi là rác. Nếu cố xét cho cùng thì có khi cuộc sống trong hang động còn đơn giản hơn
• Điều rất thú vị là AI không chỉ suy nghĩ mà còn để lại một cuốn nhật ký có thể kiểm chứng. Giống như một triết gia sống cùng một công chứng viên mật mã. Đây thực sự là công trình đáng kinh ngạc
• Ý tưởng cốt lõi là LLM phác thảo quá trình suy luận dưới dạng có cấu trúc bằng JSON DSL, rồi quá trình đó được chuyển một cách tất định sang logic bậc nhất để thử chứng minh định lý bằng Z3. Vì vậy đầu ra cuối cùng là một kết luận có thể chứng minh được hoặc một phản ví dụ, nhấn mạnh rằng điều này khác với một chuỗi văn bản chỉ có vẻ thuyết phục
• Nghiên cứu này rất thú vị. Tôi vào repo vì tò mò về ví dụ DSL nhưng khá khó tìm được ví dụ rõ ràng. Sẽ rất tốt nếu README có một đoạn mã ví dụ
  • Cảm ơn vì đã quan tâm, chúng tôi sẽ sớm bổ sung. Trong lúc đó, từ trang 11 của bài báo có mô tả nhiều tình huống khác nhau PDF bài báo