Trong bài báo này, chúng tôi đề xuất Astrogator, một hệ thống sử dụng ngôn ngữ truy vấn chính thức để làm rõ ý định của người dùng và xác minh tính chính xác của mã được tạo ra, nhằm giải quyết vấn đề lỗi của các mô hình ngôn ngữ quy mô lớn (LLM) tạo mã dựa trên mô tả ngôn ngữ tự nhiên. Astrogator nhắm đến ngôn ngữ lập trình Ansible và bao gồm một ngôn ngữ truy vấn chính thức, một phương pháp tính toán biểu diễn hành vi của chương trình Ansible, và một trình thông dịch ký hiệu dùng để xác minh. Trong bài kiểm tra chuẩn mực gồm 21 tác vụ tạo mã, mã đúng được xác minh trong 83% trường hợp và mã sai được xác định trong 92% trường hợp.