Chính thức hóa các bài toán nghịch trong thời đại AI cơ hội cạm bẫy và lời mời

Các proof assistant như Lean kiểm tra các chứng minh toán học đến tận các tiên đề, và các AI agent gần đây đã làm cho việc viết các chứng minh như vậy trở nên rẻ. Nhóm tác giả mô tả AutoIP, một thư viện Lean trong đó lý thuyết điều chuẩn tuyến tính cổ điển cùng với phân tích hàm mà nó dựa trên đã được AI agent tự formalize. Một chứng minh được kiểm tra bằng máy chỉ chứng nhận phát biểu formal mà nó chứng minh, vì vậy nhiệm vụ còn lại của con người là xác nhận rằng mỗi phát biểu formal nói đúng ý định. Nhóm tác giả tổ chức thư viện này xoay quanh nhiệm vụ đó: người đánh giá so sánh các phát biểu formal với các bản tương ứng bằng ngôn ngữ tự nhiên và không cần đọc chứng minh. Kinh nghiệm của nhóm tác giả cho thấy rủi ro nằm ở các phát biểu chứ không phải ở các chứng minh, và các bài kiểm tra tự động đơn giản trên các phát biểu có thể bộc lộ vấn đề ngay cả trong tài liệu đã được thiết lập. Nhóm tác giả minh họa điều này bằng một định lý sách giáo khoa có giả thuyết hạn chế hơn so với khẳng định. Nhóm tác giả mời cộng đồng bài toán nghịch mở rộng và xây dựng trên thư viện này.