Bài báo này trình bày một phương pháp mới để thực hiện hiệu quả việc truy xuất tiền đề, đây là một bước quan trọng trong quá trình chính thức hóa toán học. Các phương pháp truy xuất dựa trên ngôn ngữ tự nhiên hiện có yêu cầu chuyên môn toán học từ người dùng và các phương pháp dựa trên ngôn ngữ chính thức (ví dụ: Lean) gặp vấn đề về hiệu suất kém do dữ liệu đào tạo không đủ. Trong nghiên cứu này, chúng tôi đã đào tạo một mô hình truy xuất tiền đề nhẹ nhưng hiệu quả bằng cách sử dụng dữ liệu được trích xuất từ Mathlib. Cụ thể, chúng tôi đã sử dụng một bộ phân tích cú pháp chuyên biệt cho ngữ liệu ngôn ngữ chính thức để nhúng các truy vấn (trạng thái chứng minh do Lean cung cấp) và tiền đề vào không gian tiềm ẩn và áp dụng phương pháp tính toán độ tương đồng chi tiết và mô-đun xếp hạng lại để cải thiện hiệu suất. Kết quả thử nghiệm cho thấy mô hình đề xuất đạt được độ chính xác cao hơn và chi phí tính toán thấp hơn so với các phương pháp hiện có. Công cụ tìm kiếm được phát triển được cung cấp dưới dạng mã nguồn mở.
