Beyond LLM Judge: Mechanical Verification for Agentic Autoformalization

{"tags": ["Autoformalization", "Lean", "Formal Verification", "LLM-as-a-Judge", "Mechanical Verification", "DLMF", "Mathematical Reasoning"], "risks": ["Kiểm tra số trị khó áp dụng cho các cấu trúc toán học trừu tượng phi số trị hoặc không có công thức tính trực tiếp.", "Tăng chi phí tính toán và độ trễ khi kết hợp nhiều tầng kiểm chứng cơ học và suy luận LLM.", "Thư viện FLMF mới chỉ hình thức hóa một phần của NIST DLMF, cần kiểm nghiệm thêm trên quy mô lớn hơn.", "Vẫn phụ thuộc vào chất lượng trích xuất ngữ nghĩa ban đầu của LLM trước khi kiểm tra cơ học."], "category": "Research", "entities": ["Lean", "NIST DLMF", "FLMF", "GitHub"], "summary_vi": "Nghiên cứu giới thiệu phương pháp xác minh phát biểu hình thức hóa trong Lean cho quy trình tự động hóa tác tử (autoformalization), vượt qua giới hạn của phương pháp chỉ dùng LLM làm trọng tài. Bằng cách kết hợp đánh giá ngữ nghĩa của LLM với các kiểm tra cơ học (kiểm tra số trị và tính rỗng), hệ thống cung cấp phản hồi kiểm chứng được và bắt được các lỗi LLM bỏ sót. Nhóm tác giả áp dụng quy trình Extract-Verify-Proof để xây dựng thư viện FLMF (hình thức hóa một phần NIST DLMF), đạt tỷ lệ chấp nhận phát biểu sai thấp nhất trên 3 tập dữ liệu thử nghiệm và phát hiện nhiều lỗi trong các benchmark hiện tại. Mã nguồn được công khai trên GitHub.", "key_changes": ["Đề xuất phương pháp xác minh mới kết hợp đánh giá ngữ nghĩa bằng LLM với các kiểm tra cơ học (mechanical checks gồm kiểm tra số trị và kiểm tra tính rỗng/vacuity).", "Cung cấp cơ chế phản hồi có thể kiểm chứng được (checkable feedback), giúp phát hiện các lỗi sai mà LLM judge bỏ sót.", "Giới thiệu quy trình tự động hình thức hóa Extract-Verify-Proof để xây dựng thư viện FLMF (Formalized Library of Mathematical Functions) từ NIST DLMF.", "Đạt tỷ lệ chấp nhận phát biểu sai (accepted-error rate) thấp nhất trên ba tập dữ liệu benchmark có gán nhãn.", "Phát hiện nhiều lỗi dịch thuật và lỗi dữ liệu nguồn trong các tập dữ liệu hiện hữu thông qua đánh giá chuyên gia; công khai mã nguồn trên GitHub."], "sub_category": "Autoformalization & Formal Verification", "novelty_score": 82, "business_score": 55, "research_score": 88, "why_it_matters": "Khắc phục nhược điểm nghiêm trọng của LLM-as-a-Judge trong việc dễ chấp nhận các định lý sai hoặc đúng một cách rỗng (vacuous truth). Việc đưa các bước kiểm tra cơ học vào quy trình tác tử tạo tiền đề nâng cao tính chính xác và khả năng tự động hóa quy mô lớn trong số hóa tri thức toán học sang các hệ thống kiểm chứng hình thức.", "developer_score": 72, "importance_score": 80, "possible_use_cases": ["Tự động chuyển đổi các tài liệu, cẩm nang toán học chuẩn (như NIST DLMF) sang mã hình thức hóa Lean với độ tin cậy cao.", "Tích hợp vào các hệ thống AI tác tử chứng minh định lý tự động (automated theorem proving) để loại bỏ ảo giác và phát biểu sai.", "Kiểm định, làm sạch và lọc dữ liệu huấn luyện hoặc benchmark cho các mô hình AI toán học.", "Hỗ trợ phát triển các thư viện phần mềm và đặc tả hệ thống có chứng minh hình thức (formal verification) trong các lĩnh vực yêu cầu an toàn cao."], "actionability_score": 75}