Herbie: Tự động cải thiện các công thức dấu phẩy động không chính xác

Herbie viết lại biểu thức dấu phẩy động thành làm cho chúng chính xác hơn. Số học dấu phẩy động là không chính xác; thậm chí 0,1 + 0,2 ≠ 0,3 inch dấu phẩy động. Herbie giúp tìm và giải quyết những điều bí ẩn này sự không chính xác.

Để bắt đầu, hãy tải xuống và cài đặt Herbie. Sau đó bạn đã sẵn sàng để bắt đầu sử dụng nó.

Đưa ra biểu thức của Herbie

Bắt đầu Herbie với:

vợt -l herbie web

Ngoài ra, nếu bạn đã thêm herbie vào đường dẫn, bạn luôn có thể thay thế racket -l herbie bằng chỉ herbie.

Sau một thời gian chờ đợi, trình duyệt web của bạn sẽ mở và hiển thị bạn Cửa sổ chính của Herbie. Phần quan trọng nhất của trang này là chút:

Hãy bắt đầu bằng cách xem một ví dụ về Herbie đang chạy. Nhấp vào "Hiển thị ví dụ". Điều này sẽ điền trước biểu thức sqrt(x + 1) - sqrt(x) với x nằm trong khoảng từ 0 đến 1,79e308.

Bây giờ bạn đã có biểu thức và phạm vi cho từng biến, nhấp vào nút "Cải thiện với Herbie". Bạn sẽ thấy mục hộp màu xám và ngay sau đó một số văn bản sẽ xuất hiện mô tả những gì Herbie đang làm. Sau vài giây, bạn sẽ được chuyển hướng đến một trang có kết quả của Herbie.

Phần đầu của trang kết quả này cung cấp một số số liệu thống kê nhanh về những cách khác mà Herbie đã tìm ra để đánh giá điều này biểu thức:

Ở đây, bạn có thể thấy rằng phương án thay thế chính xác nhất của Herbie có một độ chính xác 99,7%, tốt hơn nhiều so với chương trình ban đầu 53,2%, và tổng cộng Herbie đã tìm thấy 5 lựa chọn thay thế. Một trong số đó các lựa chọn thay thế đều chính xác hơn biểu thức ban đầu và cũng nhanh hơn 1,9 lần. phần còn lại của trang kết quả hiển thị từng lựa chọn thay thế này, bao gồm chi tiết như cách chúng được bắt nguồn. Những chi tiết này đều được ghi lại nhưng vì lợi ích của hướng dẫn, hãy chuyển sang một ví dụ thực tế hơn.

Lập trình với Herbie

Bạn có thể sử dụng Herbie trên các biểu thức từ mã nguồn, toán học mô hình hoặc công cụ gỡ lỗi. Nhưng hầu hết người dùng đều sử dụng Herbie vì họ viết mã, hỏi nó về bất kỳ biểu thức dấu phẩy động phức tạp nào họ viết. Herbie có tùy chọn để đăng nhập tất cả các biểu thức bạn nhập để có thể tham khảo chúng sau này.

Nhưng để tập trung vào phần hướng dẫn, giả sử thay vào đó bạn theo dõi lỗi dấu phẩy động trong mã hiện có. Sau đó bạn sẽ cần bắt đầu bằng cách xác định dấu phẩy động có vấn đề biểu thức.

Để minh họa quy trình làm việc, hãy cùng xem qua lỗi 208 trong math.js, thư viện toán học dành cho JavaScript. Lỗi liên quan đến căn bậc hai không chính xác cho các hàm phức những con số. (Để biết thông tin đầy đủ về lỗi này, hãy xem một blog post của một trong những tác giả Herbie.)

Tìm biểu thức có vấn đề

Trong hầu hết các chương trình, có một hạt nhân nhỏ thực hiện các phép toán tính toán, trong khi phần còn lại của chương trình thiết lập các tham số, xử lý luồng điều khiển, trực quan hóa hoặc in kết quả, v.v. các cốt lõi toán học là điều mà Herbie sẽ quan tâm.

Ví dụ của chúng tôi, hãy bắt đầu trong lib/function/. Thư mục này chứa nhiều thư mục con; mỗi tập tin trong mỗi thư mục con định nghĩa một tập hợp các hàm toán học. Chúng tôi quan tâm đến hàm căn bậc hai phức tạp, được định nghĩa trong arithmetic/sqrt.js.

Tệp này xử lý việc kiểm tra đối số, các loại và lỗi khác nhau xử lý, cho cả căn bậc hai thực và căn bậc hai phức tạp. Không ai trong số đó là được Herbie quan tâm; chúng tôi chỉ muốn trích xuất toán học cốt lõi. Vì vậy, hãy chuyển xuống trường hợp isComplex(x):

var r = Math.sqrt(x.re * x.re + x.im * x.im);
if (x.im >= 0) {
  trả về phức hợp mới (
      0,5 * Math.sqrt(2.0 * (r + x.re)),
      0,5 * Math.sqrt(2.0 * (r - x.re))
  );
}
khác {
  trả về phức hợp mới (
      0,5 * Math.sqrt(2.0 * (r + x.re)),
      -0,5 * Math.sqrt(2.0 * (r - x.re))
  );

Đây là cốt lõi toán học mà chúng tôi muốn gửi tới Herbie.

Chuyển đổi mã có vấn đề sang đầu vào Herbie

Trong mã này, x thuộc loại Complex, a cấu trúc dữ liệu nhiều trường. Herbie chỉ giao dịch với số dấu phẩy động, không phải cấu trúc dữ liệu, vì vậy chúng ta sẽ xử lý nhập x dưới dạng hai đầu vào riêng biệt vào Herbie: xre và xim. Chúng ta cũng sẽ vượt qua từng trường đầu ra riêng biệt cho Herbie.

Mã này cũng phân nhánh giữa x.im không âm và âm x.im. Thông thường sẽ tốt hơn nếu gửi từng nhánh tới Herbie riêng biệt. Vì vậy, tổng cộng, mã này biến thành bốn Đầu vào Herbie: hai trường đầu ra, cho mỗi nhánh trong số hai nhánh.

Hãy tập trung vào trường đầu ra đầu tiên cho trường hợp không âm x.im.

Biến r là biến trung gian trong phần này khối mã. Các biến trung gian cung cấp cho Herbie những thông tin quan trọng thông tin mà Herbie có thể sử dụng để cải thiện độ chính xác, vì vậy bạn muốn mở rộng hoặc nội tuyến chúng. Kết quả trông như thế này:

0,5 * sqrt(2,0 * (sqrt(xre * xre + xim * xim) + xre))

Hãy nhớ rằng mã này chỉ chạy khi x.im không âm (nhưng nó chạy với tất cả các giá trị của x.re). Vì vậy, chọn toàn bộ phạm vi giá trị cho x.re nhưng hạn chế phạm vi của x.im, như thế này:

Điều này yêu cầu Herbie chỉ xem xét các giá trị không âm của xim khi cải thiện độ chính xác của biểu thức này. Số 1,79e308 xấp xỉ lớn nhất số có độ chính xác kép và sẽ tự động hoàn thành.

Kết quả của Herbie

Herbie sẽ khởi động trong vài giây và tạo ra trang kết quả. Trong trường hợp này, Herbie đã tìm ra 4 lựa chọn thay thế và chúng tôi quan tâm đến chính xác nhất, cần có một độ chính xác 84,6%:

Bên dưới những thống kê tóm tắt này, chúng ta có thể thấy biểu đồ về độ chính xác so với giá trị đầu vào. Theo mặc định, nó hiển thị độ chính xác so với xim; cao hơn thì tốt hơn:

Mức độ chính xác giảm khi xim lớn hơn về 1e150 thực sự nổi bật nhưng bạn cũng có thể thấy phương án thay thế của Herbie chính xác hơn cho xim nhỏ hơn các giá trị cũng vậy. Bạn cũng có thể thay đổi biểu đồ để vẽ chính xác thay vào đó là xre:

Cốt truyện này cho thấy rõ rằng lựa chọn thay thế của Herbie gần như là hoàn toàn chính xác cho xre dương, nhưng vẫn có một số lỗi cho âm xre.

Herbie cũng tìm thấy các lựa chọn thay thế khác kém chính xác hơn nhưng có thể là nhanh hơn. Bạn có thể xem tóm tắt trong bảng này:

Thuật toán của Herbie là ngẫu nhiên nên có thể bạn sẽ không thấy chính xác điều tương tự; bạn có thể thấy nhiều hoặc ít lựa chọn thay thế hơn và chúng có thể ít nhiều chính xác và nhanh chóng. Điều đó nói lên rằng, nhất phương án thay thế chính xác sẽ khá giống nhau.

Bản thân phương án thay thế đó được hiển thị ở phía dưới trang:

Một số tính năng của giải pháp thay thế này nổi bật ngay lập tức. Trước hết, Herbie đã chèn câu lệnh if. Câu lệnh if này xử lý một hiện tượng được gọi là hủy bỏ, và là một phần tại sao giải pháp thay thế của Herbie lại hiệu quả hơn chính xác. Herbie cũng thay thế phép tính căn bậc hai bằng hàm hypot tính toán khoảng cách nhiều hơn chính xác hơn phép tính căn bậc hai trực tiếp.

Nếu bạn muốn biết thêm về cách Herbie thu được kết quả này, bạn có thể nhấp vào từ "Derivation" để xem chi tiết từng bước giải thích về cách Herbie đã làm điều đó. Tuy nhiên, bây giờ chúng ta hãy chuyển sang hãy xem một giải pháp thay thế khác.

Phương án thứ năm do Herbie đề xuất kém chính xác hơn nhiều, nhưng nó nhanh gấp đôi so với chương trình ban đầu:

Phương án thay thế này hơi lạ: nó có hai nhánh và mỗi biến chỉ sử dụng một trong hai biến xre và xim. Điều đó giải thích tại sao nó nhanh nhưng vẫn chính xác hơn chương trình ban đầu vì nó tránh được các vấn đề về hủy và tràn đã gây khó khăn cho bản gốc.

Sử dụng các lựa chọn thay thế của Herbie

Trong trường hợp này, chúng tôi quan tâm đến kết quả chính xác nhất có thể triển khai, vậy nên chúng ta hãy thử sử dụng cách chính xác nhất của Herbie thay thế.

// Herbie 2.1 dành cho:
// 0,5 * sqrt(2,0 * (sqrt(xre*xre + xim*xim) + xre))
var r = Math.hypot(x.re, x.im);
var re;
if (xre + r <= 0) {
    re = 0,5 * Math.sqrt(2 * (x.im / (x.re / x.im) * -0,5));
} khác {
    re = 0,5 * Math.sqrt(2 * (x.re + r));
}
if (x.im >= 0) {
  trả về phức hợp mới (
      lại,
      0,5 * Math.sqrt(2.0 * (r - x.re))
  );
}
khác {
  trả về phức hợp mới (
      0,5 * Math.sqrt(2.0 * (r + x.re)),
      -0,5 * Math.sqrt(2.0 * (r - x.re)) );

Lưu ý rằng tôi đã để lại truy vấn Herbie trong nhận xét. Như Herbie tốt hơn, bạn có thể chạy lại nó trên biểu thức ban đầu này để xem liệu nó đưa ra những cải tiến về độ chính xác.

Nhân tiện, đối với một số ngôn ngữ, bao gồm cả JavaScript, bạn có thể sử dụng trình đơn thả xuống ở góc trên bên phải của khối thay thế để dịch đầu ra của Herbie sang ngôn ngữ đó. Tuy nhiên, bạn sẽ có lẽ vẫn cần phải cấu trúc lại và sửa đổi kết quả để phù hợp với bạn cấu trúc mã, giống như ở đây.

Các bước tiếp theo

Với thay đổi này, chúng tôi đã biến phần này của hình vuông phức tạp hàm gốc chính xác hơn nhiều và chúng ta có thể lặp lại các bước tương tự cho các ngành khác và các lĩnh vực khác trong chương trình này. Bạn bây giờ có hiểu biết khá tốt về Herbie và cách sử dụng nó. Vui lòng cho chúng tôi biết nếu Herbie đã giúp bạn và hãy kiểm tra tài liệu để tìm hiểu thêm về Các tùy chọn và đầu ra khác nhau của Herbie.