Bài báo này đề xuất Cobblestone, một công cụ tổng hợp chứng minh mới tận dụng mô hình ngôn ngữ quy mô lớn (LLM) để cải thiện hiệu quả xác minh hình thức bằng các trợ lý chứng minh như Coq. Cobblestone tạo ra các chứng minh tiềm năng bằng LLM, sau đó được sử dụng để chia nhỏ vấn đề. Nó tự động xác định các phần đã được chứng minh thành công và lặp lại các phần còn lại để cuối cùng đưa ra một chứng minh chính xác. Bất chấp sự không chắc chắn của LLM, Cobblestone đảm bảo tính chính xác của các chứng minh được tạo ra. Kết quả thực nghiệm cho thấy Cobblestone vượt trội hơn các công cụ tiên tiến hiện có, chứng minh nhiều định lý mà các công cụ dựa trên LLM khác không chứng minh được. Hiệu quả của nó được chứng minh bằng chi phí thực hiện trung bình là 1,25 đô la và thời gian chạy là 14,7 phút. Hơn nữa, nó có thể sử dụng đầu vào bên ngoài từ người dùng hoặc các công cụ khác để tận dụng cấu trúc chứng minh hoặc các bổ đề liên quan, chứng minh tới 58% các định lý. Nghiên cứu này chứng minh tiềm năng của việc tận dụng tiến trình từng phần và đầu vào bên ngoài để cải thiện hiệu quả của tự động hóa xác minh hình thức.
