Scaling Lean Theorem Proving for Real-World Code Verification

{"tags": ["EasyProver", "Lean", "Formal Verification", "Rust", "Aeneas", "Aegis", "Theorem Proving", "PutnamBench", "IMO 2026", "Reinforcement Learning"], "risks": ["Chi phí tính toán lớn với thời gian suy luận kéo dài (lên tới 30 phút cho mỗi mệnh đề cần chứng minh).", "Hiệu suất trên mã nguồn thực tế mới đạt 52,7%, chưa đủ độ tin cậy để thay thế hoàn toàn chuyên gia kiểm chứng.", "Phụ thuộc vào tính đúng đắn của chuỗi công cụ chuyển đổi (Aeneas) và chất lượng sinh đặc tả tự động."], "category": "Research", "entities": ["EasyProver", "Lean", "Aegis", "Rust", "Aeneas", "PutnamBench", "IMO 2026", "NTP4VC", "VERINA"], "summary_vi": "EasyProver là hệ thống chứng minh định lý bằng Lean dựa trên kiến trúc agent đệ quy với ngữ cảnh cô lập, tìm kiếm bất đồng bộ và kiểm tra tactic song song. Sử dụng mô hình frontier có sẵn mà không cần huấn luyện thêm, hệ thống đã giải quyết 669/672 bài PutnamBench, toàn bộ 6 bài IMO 2026, 597/600 điều kiện kiểm chứng NTP4VC và 189 tác vụ VERINA. Nhằm giải quyết tình trạng bão hòa của các benchmark hiện tại, nghiên cứu giới thiệu Aegis – quy trình chuyển đổi các bài toán lập trình thi đấu thành bài kiểm chứng mã nguồn Rust thực tế được dịch sang Lean qua Aeneas. Trên tập mẫu 2.000 mệnh đề của Aegis mang đầy đủ độ phức tạp thực tế, EasyProver chứng minh thành công 52,7% trong giới hạn 30 phút mỗi bài toán, mở ra hướng đi mới cho kiểm chứng mã nguồn và tạo tín hiệu thưởng cho học tăng cường.", "key_changes": ["Phát triển EasyProver: Hệ thống chứng minh định lý Lean dùng agent đệ quy với ngữ cảnh độc lập, tìm kiếm bất đồng bộ, thăm dò tactic song song và dịch vụ elaboration co giãn.", "Tận dụng mô hình frontier sẵn có không qua fine-tuning nhưng đạt hiệu suất gần như tuyệt đối trên các benchmark toán học và kiểm chứng: 669/672 PutnamBench, 6/6 IMO 2026, 597/600 NTP4VC, 189/189 VERINA.", "Giới thiệu benchmark Aegis: Chuyển đổi bài toán lập trình thi đấu thành tác vụ kiểm chứng mã nguồn Rust thực tế được chuyển ngữ sang Lean qua Aeneas.", "Tạo lập 2.045 cặp chương trình Rust-Lean kiểm chứng vi sai cùng 11.533 đặc tả ứng viên phản ánh độ phức tạp thực tế (số học độ rộng cố định, ép kiểu, vòng lặp, đột biến hàm hóa).", "Đạt tỷ lệ giải quyết 52,7% (1.054/2.000 mệnh đề) trong Aegis với ngân sách thời gian 30 phút/mệnh đề."], "sub_category": "Formal Verification", "novelty_score": 86, "business_score": 72, "research_score": 92, "why_it_matters": "Nghiên cứu tạo bước ngoặt trong việc chuyển dịch kiểm chứng hình thức từ các bài toán lý thuyết sang mã nguồn phần mềm thực tế với đầy đủ ràng buộc phần cứng và kiểu dữ liệu. Phương pháp sử dụng agent đệ quy trên mô hình frontier có sẵn chứng minh khả năng vượt trội mà không cần huấn luyện lại, đồng thời cung cấp bộ dữ liệu chuẩn Aegis và cơ chế sinh phần thưởng tự động đáng tin cậy cho học tăng cường.", "developer_score": 82, "importance_score": 88, "possible_use_cases": ["Kiểm chứng hình thức mã nguồn Rust an toàn trong các hệ thống hạ tầng trọng yếu (blockchain smart contracts, hệ điều hành, mật mã học).", "Tự động hóa giải toán và chứng minh định lý hình thức trong nghiên cứu toán học.", "Tạo môi trường và tín hiệu phần thưởng (reward signal) đã qua kiểm định kernel cho đào tạo mô hình AI bằng học tăng cường (RL).", "Đo lường và đánh giá năng lực của các mô hình ngôn ngữ lớn trên các bài toán suy luận logic và kiểm chứng thực tế."], "actionability_score": 68}