Resolution Dùng Agent Để Tự Hình Thức Hóa Toán Học

Resolution cho biết việc tự hình thức hóa việc phân giải điểm kỳ dị có thể đặt nền cho nghiên cứu tự động sâu hơn về quan hệ giữa hình học của bề mặt mất mát và khả năng khái quát hóa. Đây là phần công việc mà công ty gắn với lý thuyết học thống kê.

Một nhà nghiên cứu bắt đầu bằng cách làm việc với agent để tạo ra 2 kế hoạch: một bản ở mức cao, dễ hiểu với con người, và một bản chi tiết 112 trang, chia thành các bước nguyên tử bám sát tài liệu hiện có. Sau đó, một agent điều phối được giao thực hiện kế hoạch, khởi chạy các agent khác để làm toán tay, viết Lean và kiểm tra công việc có đi đúng hướng hay không.

Công ty nói giai đoạn thực hiện cần rất ít khung đỡ ngoài bản kế hoạch ban đầu và một số kỹ năng agent được chưng cất từ các nỗ lực tự hình thức hóa nội bộ trước đó. Việc này diễn ra trong khoảng 1 tuần.

Khối lượng công việc ước tính gồm khoảng 100B token đầu vào, trong đó 90% là lần đọc từ bộ nhớ đệm, cùng khoảng 300 triệu token đầu ra. Tổng tiền token ước tính là 135.000 đô la, và kết quả là khoảng 600.000 dòng Lean.