, стверджує, що розробляє прототип нової мови програмування.){kind=link}
Máy tính hiệu suất cao là cần thiết để giải quyết ngày càng nhiều tác vụ - chẳng hạn như xử lý hình ảnh hoặc các ứng dụng học sâu khác nhau trên mạng nơ-ron - nơi bạn cần xử lý một lượng lớn dữ liệu và thực hiện nó đủ nhanh, nếu không, nó có thể mất một lượng đáng kinh ngạc thời gian. Người ta tin rằng khi thực hiện các hoạt động như vậy, sự thỏa hiệp giữa tốc độ và độ tin cậy là không thể tránh khỏi. Theo suy nghĩ này, nếu tốc độ là ưu tiên, thì độ tin cậy có thể bị ảnh hưởng và ngược lại.
Tuy nhiên, một nhóm các nhà nghiên cứu chủ yếu có trụ sở tại Viện Công nghệ Massachusetts (MIT) đang thách thức quan điểm này, cho rằng bạn thực sự có thể có tất cả. Theo Amanda Liu, một nghiên cứu sinh năm thứ hai tại Phòng thí nghiệm Khoa học Máy tính và Trí tuệ Nhân tạo (CSAIL) của MIT, với một ngôn ngữ lập trình mới mà họ đã viết dành riêng cho máy tính hiệu suất cao, “tốc độ và độ chính xác không phải cạnh tranh. Ngược lại, họ có thể song hành, song hành cùng nhau trong những chương trình mà chúng tôi viết ra ”. Liu và nhóm của cô đã nói về tiềm năng của A Tensor Language (ATL) mới được tạo ra vào tháng trước tại hội nghị Nguyên tắc của Ngôn ngữ Lập trình ở Philadelphia.
Liu nói: “Mọi thứ trong ngôn ngữ của chúng tôi đều nhằm mục đích nhận được một số duy nhất hoặc một tenxơ”. Đến lượt mình, các căng là một tổng quát của vectơ và ma trận. Trong khi vectơ là các đối tượng một chiều (thường được biểu diễn bằng các mũi tên riêng lẻ) và ma trận là mảng hai chiều quen thuộc của các số, thì tenxơ là mảng n chiều có thể có dạng mảng 3 × 3 × 3, hoặc thậm chí. thứ nguyên cao hơn (hoặc thấp).
Bản chất của một thuật toán hoặc chương trình máy tính là bắt đầu một phép tính nhất định. Nhưng có thể có nhiều cách khác nhau để viết chương trình này - "một loạt các cách triển khai mã khác nhau đáng ngạc nhiên," như Liu và các đồng tác giả của cô viết trong bài báo của họ - một số trong số đó nhanh hơn đáng kể so với những cách khác. Cô giải thích lý do chính đằng sau ATL là: “Do máy tính hiệu suất cao tiêu tốn nhiều tài nguyên, bạn muốn có thể sửa đổi hoặc viết lại các chương trình ở dạng tối ưu để tăng tốc độ. Thường thì bạn bắt đầu với chương trình dễ viết nhất, nhưng đó có thể không phải là cách nhanh nhất để chạy nó, vì vậy bạn vẫn cần phải điều chỉnh thêm. "
Ngôn ngữ lệnh mới dựa trên ngôn ngữ Coq hiện có, bao gồm một trình trợ giúp bằng chứng. Đến lượt mình, trợ lý chứng minh có khả năng chứng minh các tuyên bố của nó một cách chính xác về mặt toán học. Coq có một đặc tính khác khiến nó trở nên hấp dẫn đối với nhóm MIT: các chương trình được viết bằng ngôn ngữ đó, hoặc một bản chuyển thể của nó, luôn kết thúc và không thể chạy vô thời hạn trong các vòng lặp vô hạn.
Giờ đây, nó là ngôn ngữ tensor đầu tiên và duy nhất cho đến nay có các tính năng tối ưu đã được xác minh chính thức. Tuy nhiên, nhóm nghiên cứu của MIT cảnh báo rằng ATL vẫn chỉ là một nguyên mẫu - mặc dù là một nguyên mẫu đầy hứa hẹn - đã được thử nghiệm trên một số chương trình nhỏ.
Đọc thêm: