Toán học và tính toán

Thí nghiệm ma trận ngẫu nhiên

Các ma trận lớn điền số ngẫu nhiên, chéo hóa lặp đi lặp lại để nghiên cứu thống kê của các giá trị riêng.

Câu hỏi nó trả lời: Các giá trị riêng của một ma trận ngẫu nhiên ổn định vào mẫu hình nào, và nó có khớp với các lĩnh vực toán học và vật lý khác không?

Bỏ qua: Chỉ lấy mẫu một góc nhỏ xíu của không gian vô hạn các ma trận có thể có.

Chạy trên: khoảng 10¹² FLOPS sơ lược một cụm máy của trường đại học tạo và chéo hóa nhiều ma trận lớnTừ: 1955 Công trình sớm của Wigner về thống kê giá trị riêng của ma trận ngẫu nhiên

Thí nghiệm đồ thị ngẫu nhiên

Đồ thị được tạo bằng một quy tắc ngẫu nhiên, từng nút hoặc từng cạnh một, để xem những tính chất nào, chẳng hạn tính kết nối hay độ tụ cụm, thường xuất hiện.

Câu hỏi nó trả lời: Một mạng “điển hình” trông ra sao dưới quy tắc thêm nút và cạnh này?

Bỏ qua: Mạng ngoài đời hiếm khi sạch sẽ như quy tắc sinh ra mô hình.

Chạy trên: khoảng 10¹⁰ FLOPS sơ lược chạy trên máy tính để bàn cho đồ thị tới hàng triệu nútTừ: 1959 Mô hình đồ thị ngẫu nhiên của Erdős và Rényi

Mô phỏng thấm

Một mạng tinh thể hoặc mạng lưới với các vị trí hoặc liên kết được mở ngẫu nhiên, theo dõi điểm mà tại đó một đường nối liền đột nhiên bắc qua toàn hệ.

Câu hỏi nó trả lời: Ở mật độ nào thì một mạng ngẫu nhiên đột nhiên liền thông từ đầu đến cuối?

Bỏ qua: Các mạng tinh thể lý tưởng hóa hoạt động gọn gàng hơn bất kỳ vật liệu xốp hay mạng nào ngoài thực tế.

Chạy trên: khoảng 10¹⁰ FLOPS sơ lược một máy tính để bàn cho các lượt quét mạng tinh thể lớnTừ: 1957 Việc Broadbent và Hammersley giới thiệu lý thuyết thấm

Tìm kiếm toán học thực nghiệm

Tìm kiếm số bằng sức mạnh thô để tìm các mẫu, phản ví dụ hay quan hệ chính xác giữa các con số, chạy vượt xa những gì có thể kiểm tra bằng tay.

Câu hỏi nó trả lời: Giả thuyết này có đúng với mọi trường hợp mà người ta đủ sức kiểm tra không, và có xuất hiện quy luật nào không?

Bỏ qua: Dù tìm thấy bao nhiêu trường hợp đúng, không số lượng trường hợp đã kiểm tra nào là một chứng minh.

Chạy trên: khoảng 10¹¹ FLOPS sơ lược một cụm máy của trường đại học chạy nhiều ngày cho một lần tìm kiếmTừ: 1963 đến năm 1963, máy tính tìm kiếm các quan hệ số nguyên và quy luật của số nguyên tố

Ước lượng hằng số bằng Monte Carlo

Lấy mẫu ngẫu nhiên dùng để ước lượng một hằng số hay tích phân toán học, như rải điểm để ước lượng diện tích, như một bài tập chứ không phải cho mô hình vật lý.

Câu hỏi nó trả lời: Chỉ riêng lấy mẫu ngẫu nhiên mù có thể xác định một đại lượng toán học chính xác đến mức nào?

Bỏ qua: Hội tụ chậm hơn nhiều so với hầu như mọi phương pháp số tinh vi hơn.

Chạy trên: khoảng 10⁹ FLOPS sơ lược chạy trên máy tính xách tay trong vài giây đến vài phútTừ: 1946 Ý tưởng của Ulam năm 1946; von Neumann đề xuất một phiên bản máy tính điện tử vào tháng 3 năm 1947, và phương pháp được công bố lần đầu năm 1949 nguồnTrong cây mô phỏng: Phương pháp Monte Carlo

Chạy mô hình tương tác

Tìm kiếm trong lý thuyết số tính toán

Các số lớn được kiểm tra tính nguyên tố, phân tích thừa số, hoặc tìm kiếm các tính chất đặc biệt như số hoàn hảo, bằng thuật toán chạy ở quy mô lớn thay vì bằng tay.

Câu hỏi nó trả lời: Con số khổng lồ này có tính chất ta đang tìm không, và cuộc tìm kiếm có thể đẩy kỷ lục đi xa tới đâu?

Bỏ qua: Những lượt tìm kiếm phá kỷ lục nói rất ít về các số chưa ai nghĩ đến kiểm tra.

Chạy trên: khoảng 10¹³ FLOPS sơ lược một dự án tính toán tình nguyện phân tán trên nhiều máy được hiến tặngTừ: 1951 Phép thử bằng tay của Lucas cho số nguyên tố Mersenne, lần đầu chạy bằng máy tính năm 1951

Số học điểm hút hỗn loạn

Một tập nhỏ phương trình phi tuyến được tích phân từng bước để lộ sự phụ thuộc nhạy cảm vào điều kiện ban đầu và một điểm hút fractal.

Câu hỏi nó trả lời: Vì sao một hệ tất định đơn giản lại trở nên không thể dự đoán?

Bỏ qua: Làm tròn số nghĩa là một quỹ đạo dài không phải quỹ đạo thật, chỉ là một quỹ đạo bám sát nó.

Chạy trên: khoảng 10³ FLOPS sơ lược một vài phương trình, vài giây trên máy tính xách tay.Từ: 1963 Dòng chảy không tuần hoàn xác định của Lorenz, một mô hình đối lưu chạy trên máy tính. nguồnTrong cây mô phỏng: Đối lưu hỗn loạn của Lorenz

Thí nghiệm mạng phi tuyến

Một chuỗi các khối lượng nối bằng lò xo phi tuyến, khởi động ở một chế độ rồi theo dõi xem năng lượng có lan đều ra như nhiệt động lực học gợi ý hay không.

Câu hỏi nó trả lời: Một chuỗi phi tuyến có chia đều năng lượng cho mọi chuyển động của nó không?

Bỏ qua: Kết quả phụ thuộc vào chuỗi và trạng thái ban đầu được chọn.

Chạy trên: khoảng 10³ FLOPS sơ lược nhỏ xíu so với chuẩn hiện đại; bản gốc dùng vài chục khối lượng.Từ: 1955 Các nghiên cứu của Fermi, Pasta và Ulam về các bài toán phi tuyến trên một máy tính số đời đầu. nguồn

Thí nghiệm số về soliton

Một phương trình sóng phi tuyến được giải trên một lưới để xem các xung đi xuyên qua nhau mà vẫn giữ nguyên hình dạng, điều mà sóng tuyến tính không làm được.

Câu hỏi nó trả lời: Vì sao một số sóng phi tuyến đi xuyên qua nhau mà không thay đổi?

Bỏ qua: Nó cho thấy một họ phương trình, chứ không phải hành vi chung của sóng phi tuyến.

Chạy trên: khoảng 10⁴ FLOPS sơ lược một lưới một chiều, ngày nay chỉ là chuyện nhỏ.Từ: 1965 Tương tác của các soliton trong plasma không va chạm và sự quay lại của các trạng thái ban đầu của Zabusky và Kruskal. nguồn

Dựng hình tập fractal

Một công thức lặp đơn giản được thử tại mỗi vị trí trên mặt phẳng phức để xem nó có thoát ra vô cùng hay không, vẽ nên biên của tập các điểm ổn định.

Câu hỏi nó trả lời: Tập hợp mà một phép lặp đơn giản còn bị chặn có hình dạng thế nào?

Bỏ qua: Các phép thử thoát chỉ gợi ý tư cách thành viên, và hình ảnh là một lần lấy mẫu độ phân giải hữu hạn của một tập chi tiết vô hạn.

Chạy trên: khoảng 10⁹ FLOPS sơ lược phóng đại sâu cần phép lặp độ chính xác mở rộng tại hàng triệu điểm.Từ: 1980 Các khía cạnh fractal của phép lặp z thành lambda z(1-z) của Mandelbrot, những hình ảnh máy tính đầu tiên của tập Mandelbrot. nguồn

Tính tới hạn tự tổ chức của đống cát

Các hạt rơi xuống một lưới và sụp đổ khi dốc quá mức, tạo ra những trận lở có đủ mọi kích cỡ mà không cần điều chỉnh, như một mô hình về cách các hệ thống đạt đến trạng thái tới hạn.

Câu hỏi nó trả lời: Vì sao tuyết lở ở mọi cỡ đều xuất hiện mà không cần chỉnh gì?

Bỏ qua: Việc các hệ thống thật có chung quy luật co giãn như vậy hay không còn đang tranh cãi.

Chạy trên: khoảng 10⁹ FLOPS sơ lược các lần chạy dài trên lưới lớn để xem quy mô.Từ: 1987 Tính tới hạn tự tổ chức của Bak, Tang và Wiesenfeld: một lời giải thích cho nhiễu 1/f. nguồn

Tính không điểm của hàm zeta Riemann

Các giá trị của hàm zeta dọc theo đường tới hạn của nó được tính để định vị và đếm các không điểm, kiểm tra xem chúng có nằm đúng nơi giả thuyết nói không.

Câu hỏi nó trả lời: Mọi không điểm không tầm thường của hàm zeta có nằm trên một đường thẳng không?

Bỏ qua: Một lần kiểm tra hữu hạn, dù dài đến đâu, cũng không thể chứng minh rằng không có không điểm nào nằm ngoài đường thẳng đó ở phía bên kia giới hạn của nó.

Chạy trên: khoảng 10¹⁸ FLOPS sơ lược hàng thập kỷ thời gian CPU ở các cuộc tìm kiếm lớn nhất.Từ: 1953 Các phép tính hàm zeta Riemann của Turing. nguồn

Các chữ số của pi bằng máy tính

Các chuỗi cho pi được cộng đến số chữ số khổng lồ bằng số học chính xác, thử cả con số lẫn cỗ máy.

Câu hỏi nó trả lời: Các chữ số của pi trông có ngẫu nhiên không, và có thể tin cỗ máy ở quy mô này không?

Bỏ qua: Các chữ số không trả lời câu hỏi mở nào, và các phép kiểm tra chỉ bắt được lỗi phần cứng nếu phương pháp độc lập.

Chạy trên: khoảng 10¹⁷ FLOPS sơ lược vài tháng trên một máy chủ cho hàng trăm nghìn tỷ chữ số.Từ: 1950 Reitwiesner dùng ENIAC xác định pi và e đến hơn 2000 chữ số thập phân (công bố 1950, in lại trong Pi: A Source Book). nguồn

Khám phá phỏng đoán có AI dẫn đường

Học máy trên các bảng lớn của các đối tượng toán học tìm ra những tính chất nào liên kết với nhau, để gợi ý một giả thuyết mà các nhà toán học sau đó thử chứng minh.

Câu hỏi nó trả lời: Mối quan hệ chưa thấy nào giữa các đại lượng toán học này đáng được chứng minh?

Bỏ qua: Nó chỉ gợi ý các khuôn mẫu và tự nó không chứng minh gì, và một số quy luật trong dữ liệu có thể là hiện vật của cách dữ liệu được tạo ra.

Chạy trên: khoảng 10¹⁵ FLOPS sơ lược vài ngày trên vài GPU cho mỗi bộ dữ liệu.Từ: 2021 Davies và các đồng nghiệp, thúc đẩy toán học bằng cách dẫn dắt trực giác con người với AI. nguồn

Tìm kiếm thuật toán và cấu trúc bằng học máy

Một hệ thống chơi game hoặc mô hình ngôn ngữ tìm kiếm những quy trình hoặc đối tượng toán học mới, với một máy tính kiểm tra tính đúng đắn của từng ứng viên.

Câu hỏi nó trả lời: Một chương trình có thể khám phá một thuật toán nhanh hơn hoặc một ví dụ lớn hơn những gì con người đã tìm ra không?

Bỏ qua: Mỗi kết quả chỉ là một ví dụ mới, và cuộc tìm kiếm chỉ bao phủ các loại đối tượng mà người thiết kế đã dựng thành trò chơi.

Chạy trên: khoảng 10¹⁷ FLOPS sơ lược vài ngày đến vài tuần trên các cụm bộ tăng tốc.Từ: 2022 AlphaTensor của Fawzi và các đồng nghiệp, khám phá các thuật toán nhân ma trận nhanh hơn bằng học tăng cường. nguồn

Kiểm tra mô hình

Mọi trạng thái có thể đạt tới của một hệ hữu hạn, như một giao thức hay một thiết kế mạch, được máy tính liệt kê để kiểm tra rằng một tính chất đúng trong tất cả chúng.

Câu hỏi nó trả lời: Có trạng thái nào đạt tới được mà thiết kế này phá vỡ chính quy tắc của nó không?

Bỏ qua: Không gian trạng thái bùng nổ vượt quá khả năng kiểm tra, nên các thiết kế thật được đơn giản hóa trước.

Chạy trên: khoảng 10¹² FLOPS sơ lược một cụm máy của trường đại học vét cạn một không gian trạng thái lớn nhưng có giới hạnTừ: 1981 Việc Clarke và Emerson giới thiệu kiểm tra mô hình

Tìm kiếm chứng minh định lý tự động

Một cuộc tìm kiếm qua các chuỗi suy luận logic, do máy tính tạo từng bước, để tìm một chứng minh hoặc bác bỏ cho một mệnh đề toán học.

Câu hỏi nó trả lời: Có tồn tại một chuỗi bước logic hợp lệ từ các tiên đề đến mệnh đề này không?

Bỏ qua: Tìm ra những chứng minh mà không con người nào chọn, và đôi khi chẳng tìm được gì trong tầm với.

Chạy trên: khoảng 10¹¹ FLOPS sơ lược một cụm máy của trường đại học tìm kiếm vài giờ đến vài ngàyTừ: 1956 Logic Theorist, một chương trình tìm kiếm chứng minh tự động từ rất sớm

SAT và giải ràng buộc

Hàng triệu tổ hợp giá trị đúng hoặc sai được tìm kiếm có hệ thống để thỏa mãn một tập lớn các ràng buộc logic, dùng để lập lịch, định tuyến hay kiểm chứng thiết kế.

Câu hỏi nó trả lời: Có phép gán giá trị nào thỏa mãn đồng thời mọi ràng buộc này không?

Bỏ qua: Một số bài toán khó đến mức không bộ giải nào, dù giỏi đến đâu, chạy xong kịp lúc.

Chạy trên: khoảng 10¹¹ FLOPS sơ lược từ một máy trạm đến một cụm máy, tùy quy mô bài toánTừ: 1962 thủ tục Davis-Putnam để tìm kiếm tính thỏa mãn

Mô hình hóa tấn công mật mã

Một sơ đồ mã hoặc trao đổi khóa bị tấn công hàng triệu lần trong mô phỏng, bằng vét cạn, thiên lệch thống kê hay một điểm yếu được mô hình hóa, để đo xem phá nó thật sự tốn bao nhiêu công sức.

Câu hỏi nó trả lời: Thực sự cần bao nhiêu phép tính để phá được cái này, và con số đó có còn lớn đến mức an toàn không?

Bỏ qua: Chỉ kiểm tra các cuộc tấn công mà nhà phân tích nghĩ để mô hình, chứ không phải cuộc tấn công chưa ai tìm ra.

Chạy trên: khoảng 10¹⁴ FLOPS sơ lược một cụm phân tán gồm nhiều máy chạy các lần thử tấn côngTừ: 1976 đến năm 1976, phân tích bằng máy tính về độ mạnh của mật mã và trao đổi khóa

Mô phỏng rò rỉ kênh bên

Công suất tiêu thụ, thời gian hoặc phát xạ điện từ của một thiết bị được mô hình hóa khi nó chạy một thao tác mật mã, để xem người nghe bên ngoài có thể biết được gì từ đó.

Câu hỏi nó trả lời: Bao nhiêu khóa bí mật bị rò ra qua hành vi vật lý của thiết bị, chứ không phải qua toán học?

Bỏ qua: Điều kiện phòng thí nghiệm bắt được tín hiệu sạch hơn mức một thiết bị thật đầy nhiễu thường để lộ.

Chạy trên: khoảng 10¹⁰ FLOPS sơ lược một máy trạm mô hình hóa vết công suất hoặc thời gian của một thiết bịTừ: 1996 Kocher chứng minh các cuộc tấn công thời gian vào việc triển khai mật mã

Kiểm chứng giao thức an ninh

Mọi thông điệp mà kẻ tấn công có thể gửi, phát lại hay giả mạo trong một giao thức truyền thông, được máy tính liệt kê để kiểm tra xem có thể ép lộ một bí mật hay một danh tính từ nó không.

Câu hỏi nó trả lời: Có chuỗi thông điệp nào có thể lừa giao thức này làm lộ bí mật hoặc chấp nhận một danh tính giả không?

Bỏ qua: Xác minh giao thức như được đặc tả, chứ không phải các lối tắt mà một bản triển khai thật dùng.

Chạy trên: khoảng 10¹¹ FLOPS sơ lược từ một máy trạm đến một cụm máy kiểm tra không gian thông điệp của một giao thứcTừ: 1989 mô hình Dolev-Yao, nền tảng cơ bản cho việc xác minh giao thức

Chứng minh có máy tính hỗ trợ bằng kiểm tra vét cạn các trường hợp

Một định lý được rút gọn thành một danh sách hữu hạn các trường hợp, mỗi trường hợp được kiểm chứng bằng chương trình, vì không con người nào kiểm tra hết được.

Câu hỏi nó trả lời: Một chứng minh có thể được hoàn tất bằng một cỗ máy kiểm tra mọi trường hợp không?

Bỏ qua: Sự tin cậy chuyển sang chương trình, phần cứng và lập luận rút gọn trường hợp.

Chạy trên: khoảng 10⁹ FLOPS sơ lược khoảng một nghìn giờ trên máy tính lớn cho bản gốc; ngày nay ít hơn nhiều.Từ: 1977 Chứng minh của Appel và Haken rằng mọi bản đồ phẳng đều tô được bằng bốn màu, dùng tính khả quy được máy tính kiểm tra. nguồn

Tính toán số được xác thực

Các phép tính thực hiện với cận bảo đảm, nên một kết quả số chứng minh một mệnh đề toán học, như sự tồn tại của một điểm hút hỗn loạn.

Câu hỏi nó trả lời: Một đáp án được tính ra có thể được chứng minh là đúng, chứ không chỉ có khả năng cao là chính xác không?

Bỏ qua: Các cận có thể phình lên qua thời gian dài, giới hạn việc chứng minh trong những bài toán ngắn hoặc có hành vi tốt.

Chạy trên: khoảng 10⁹ FLOPS sơ lược số học khoảng nhân chi phí lên một hệ số khiêm tốn.Từ: 2002 Bộ giải ODE chặt chẽ của Tucker và bài toán thứ 14 của Smale, chứng minh sự tồn tại của tập hút Lorenz. nguồn

Liệt kê máy Turing

Mọi chương trình nhỏ của một cỗ máy tối giản được chạy để xem cái nào dừng và cái nào chạy mãi, nhằm tìm chương trình dừng chạy lâu nhất ở mỗi cỡ.

Câu hỏi nó trả lời: Một chương trình bé xíu có thể chạy bao lâu trước khi dừng?

Bỏ qua: Tính bất khả quyết định có nghĩa là một số cỗ máy không bao giờ được phân loại, dù chạy bao lâu.

Chạy trên: khoảng 10¹⁵ FLOPS sơ lược hàng tỷ máy, kèm chứng minh cho những máy không dừng.Từ: 1965 Các nghiên cứu máy tính của Lin và Rado về các bài toán máy Turing. nguồn

Kiểm tra mô hình thống kê

Một hệ thống có hành vi ngẫu nhiên được mô phỏng nhiều lần để ước tính một cách đáng tin xem khả năng nó vi phạm một tính chất là bao nhiêu.

Câu hỏi nó trả lời: Một hệ thống ngẫu nhiên có khả năng vi phạm quy tắc an toàn đến đâu?

Bỏ qua: Các lần chạy thống kê cho ra một xác suất kèm mức tin cậy, không phải một chứng minh, và những lỗi hiếm cần lấy mẫu theo tầm quan trọng.

Chạy trên: khoảng 10⁹ FLOPS sơ lược hàng nghìn đến hàng triệu lần thực thi được lấy mẫu.Từ: 2002 Xác minh xác suất các hệ sự kiện rời rạc bằng lấy mẫu chấp nhận của Younes và Simmons. nguồn

Kiểm thử fuzz

Một chương trình được cho ăn số lượng khổng lồ các đầu vào ngẫu nhiên hoặc đột biến để tìm những đầu vào làm nó sập, về bản chất là mô phỏng một thế giới thù địch hoặc cẩu thả.

Câu hỏi nó trả lời: Đầu vào nào sẽ làm phần mềm này hỏng?

Bỏ qua: Nó chỉ tìm ra những lỗi mà đầu vào ngẫu nhiên chạm tới, và một chương trình có thể qua nhiều năm mà vẫn giấu một lỗi sau một trường hợp hiếm.

Chạy trên: khoảng 10¹⁴ FLOPS sơ lược năm-máy thời gian CPU cho một cơ sở mã lớn.Từ: 1990 Miller, Fredriksen và So, nghiên cứu thực nghiệm về độ tin cậy của các tiện ích UNIX. nguồn

Thực thi biểu tượng

Một chương trình được chạy với các đầu vào chưa biết viết dưới dạng ký hiệu, thu thập các điều kiện trên từng đường đi, rồi một bộ giải tìm các giá trị đi theo từng nhánh.

Câu hỏi nó trả lời: Những đầu vào nào làm cho từng đường đi của chương trình này chạy, và có đường nào chạm tới lỗi không?

Bỏ qua: Số đường đi tăng theo hàm mũ cùng với kích thước chương trình, nên các chương trình lớn chỉ được bao phủ một phần.

Chạy trên: khoảng 10¹² FLOPS sơ lược giờ giải cho mỗi chương trình, tăng dốc theo số đường đi.Từ: 1976 Thực thi biểu tượng và kiểm thử chương trình của King. nguồn

Diễn giải trừu tượng

Một chương trình được chạy trên các tập giá trị có thể, như các khoảng, thay vì từng giá trị đơn lẻ, để chứng minh các tính chất đúng với mọi đầu vào.

Câu hỏi nó trả lời: Chương trình này có bao giờ chia cho không hoặc tràn số, với bất kỳ đầu vào nào không?

Bỏ qua: Xấp xỉ an toàn gây báo động giả, nên con người vẫn phải kiểm tra từng cảnh báo.

Chạy trên: khoảng 10¹¹ FLOPS sơ lược giờ trên một máy trạm cho một cơ sở mã điện tử hàng không lớn.Từ: 1977 Diễn giải trừu tượng của Cousot và Cousot, một mô hình dàn thống nhất để phân tích tĩnh các chương trình. nguồn

Kiểm tra mô hình có giới hạn

Hành vi của một thiết kế trong một số bước cố định được viết thành một công thức logic và giao cho bộ giải thỏa mãn để tìm bất kỳ đường ngắn nào dẫn đến lỗi.

Câu hỏi nó trả lời: Mạch hay chương trình này có thể đạt trạng thái lỗi trong một số bước nhất định không?

Bỏ qua: Nó không chứng minh gì ngoài giới hạn bước, trừ khi có một lập luận riêng cho thấy giới hạn đó là đủ.

Chạy trên: khoảng 10¹³ FLOPS sơ lược giờ trên một máy chủ cho mỗi tài sản.Từ: 1999 Kiểm tra mô hình biểu tượng của Biere, Cimatti, Clarke và Zhu mà không cần BDD. nguồn

Kiểm thử ngẫu nhiên dựa trên tính chất

Một quy tắc lẽ ra luôn đúng được phát biểu ra, và máy tính tạo nhiều trường hợp ngẫu nhiên, thu nhỏ mọi lỗi thành một phản ví dụ nhỏ.

Câu hỏi nó trả lời: Mã này có tuân theo đặc tả của chính nó trên một dải rộng các đầu vào không?

Bỏ qua: Các trường hợp ngẫu nhiên có thể không bao giờ chạm tới một điều kiện hiếm, và tính chất được viết ra có thể không phải điều quan trọng.

Chạy trên: khoảng 10⁹ FLOPS sơ lược vài phút trên một máy tính xách tay cho hàng nghìn trường hợp.Từ: 2000 QuickCheck của Claessen và Hughes, một công cụ nhẹ để kiểm thử ngẫu nhiên các chương trình Haskell. nguồn

Kiểm chứng mạng nơ-ron

Các bộ giải ràng buộc chứng minh rằng với mọi đầu vào trong một vùng, đầu ra của một mạng nơ-ron nằm trong giới hạn, thay vì thử các mẫu.

Câu hỏi nó trả lời: Một thay đổi nhỏ ở đầu vào có bao giờ khiến mạng đưa ra câu trả lời sai không?

Bỏ qua: Các chứng minh chỉ mở rộng được đến những mạng nhỏ, và tập nhiễu loạn có thể kiểm tra rất hẹp.

Chạy trên: khoảng 10¹³ FLOPS sơ lược vài giờ đến vài ngày trên một máy chủ cho một mạng nhỏ.Từ: 2017 Reluplex của Katz và các đồng nghiệp, một bộ giải SMT để kiểm chứng mạng nơ-ron sâu. nguồn

Mô phỏng kiến trúc máy tính

Đường ống, bộ nhớ đệm và bộ dự đoán rẽ nhánh của một bộ xử lý được đề xuất được mô hình hóa từng lệnh một, để ước tính tốc độ của một con chip trước khi chế tạo.

Câu hỏi nó trả lời: Thiết kế bộ xử lý này sẽ chạy các chương trình thật nhanh đến mức nào, trước khi cắt một mảnh silicon nào?

Bỏ qua: Đơn giản hóa đủ phần của con chip thật nên silicon cuối cùng luôn khác mô hình một chút.

Chạy trên: khoảng 10¹¹ FLOPS sơ lược một cụm máy của trường đại học chạy các chương trình chuẩn qua mô hìnhTừ: 1990 đến năm 1990, các trình mô phỏng bộ xử lý chính xác từng chu kỳ cho nghiên cứu kiến trúc

Mô phỏng hệ phân tán và đồng thuận

Nhiều máy tính được mô hình hóa gửi thông điệp cho nhau với độ trễ, rơi gói và sự cố, để kiểm tra xem một thuật toán phân tán có còn đồng thuận về câu trả lời đúng không.

Câu hỏi nó trả lời: Thuật toán này có còn đạt đúng thỏa thuận khi thông điệp bị mất, chậm hay các nút sập không?

Bỏ qua: Các sự cố được tiêm vào là những sự cố nhà thiết kế đã lường trước, chứ không phải những sự cố bất ngờ xuất hiện trong môi trường thực.

Chạy trên: khoảng 10¹⁰ FLOPS sơ lược một cụm máy mô phỏng hàng trăm nút ảoTừ: 1978 Công trình sớm của Lamport về thứ tự và sự cố trong các hệ phân tán

Mô phỏng hệ thống lưu trữ

Đĩa, ổ và hệ thống tệp được mô hình hóa theo cách chúng bố trí dữ liệu, hỏng hóc và phục hồi, để thử một thiết kế lưu trữ trước khi mua và lấp đầy ổ thật.

Câu hỏi nó trả lời: Thiết kế lưu trữ này hoạt động và sống sót thế nào khi hỏng, ở quy mô quá tốn kém để thử thật trước?

Bỏ qua: Ổ đĩa thật hỏng theo những cách lộn xộn, có tương quan hơn tỷ lệ hỏng ngẫu nhiên của mô hình.

Chạy trên: khoảng 10¹⁰ FLOPS sơ lược từ một máy trạm đến một cụm máy nhỏ mô hình hóa một dàn lưu trữTừ: 1988 đến năm 1988, các mô hình mô phỏng về độ tin cậy của dàn đĩa

Mô phỏng bộ lập lịch hệ điều hành

Một dòng tác vụ tính toán được mô hình hóa khi chúng đến và tranh nhau một bộ xử lý, chạy theo các quy tắc lập lịch khác nhau để xem quy tắc nào công bằng hoặc nhanh nhất.

Câu hỏi nó trả lời: Cách sắp thứ tự hàng đợi nhiệm vụ nào hoàn thành được nhiều việc nhất, hoặc công bằng nhất với mọi nhiệm vụ?

Bỏ qua: Khối lượng công việc tổng hợp hiếm khi khớp với hỗn hợp nhiệm vụ bất thường mà một máy thật gặp phải.

Chạy trên: khoảng 10⁹ FLOPS sơ lược chạy trên máy tính xách tay hoặc máy trạm trong vài giây đến vài phútTừ: 1968 đến năm 1968, các nghiên cứu mô phỏng về chính sách lập lịch bộ xử lý

Tìm kiếm tối ưu hóa trình biên dịch và chương trình

Số lượng khổng lồ các biến thể nhỏ của một đoạn mã được thử và đo, tìm phiên bản nhanh nhất hoặc ngắn nhất mà vẫn làm đúng việc đó.

Câu hỏi nó trả lời: Trong mọi cách tương đương để viết đoạn mã nhỏ này, cách nào thực sự nhanh nhất?

Bỏ qua: Các chương trình tìm được đôi khi bất thường đến mức không có lời giải thích vì sao chúng hoạt động.

Chạy trên: khoảng 10¹⁰ FLOPS sơ lược một cụm máy tìm kiếm trong một không gian lớn các biến thể mãTừ: 2006 đến năm 2006, tìm kiếm siêu tối ưu trên các chuỗi lệnh ngắn

Kiểm thử thực nghiệm hiệu năng thuật toán

Một thuật toán được chạy hàng nghìn lần trên các đầu vào ngẫu nhiên hoặc thực tế có kích thước tăng dần, đo xem thời gian chạy của nó thực sự tăng ra sao thay vì chứng minh trên giấy.

Câu hỏi nó trả lời: Thời gian chạy của thuật toán này thực sự tăng thế nào trong thực tế, trên những đầu vào nó sẽ thật sự gặp?

Bỏ qua: Một trường hợp xấu nhất vắng mặt trong các đầu vào kiểm thử vẫn không bị phát hiện cho đến khi nó xảy ra.

Chạy trên: khoảng 10⁹ FLOPS sơ lược chạy trên một máy trạm qua nhiều đầu vào kiểm thử được tạo raTừ: 1970 đến năm 1970, việc kiểm thử thực nghiệm có hệ thống về thời gian chạy của thuật toán

Thực thi chương trình bằng mô hình ngôn ngữ

Một mô hình ngôn ngữ viết ra từng bước các trạng thái trung gian khi lần theo những gì một chương trình sẽ tính.

Câu hỏi nó trả lời: Một mô hình ngôn ngữ có thể mô phỏng việc chạy mã không?

Bỏ qua: Đầu ra không đảm bảo đúng, và các chương trình dài thì hỏng.

Chạy trên: khoảng 10¹⁴ FLOPS sơ lược Suy luận cho mỗi truy vấnTừ: 2021 Show your work: scratchpads for intermediate computation with language models (2021) nguồn

Mô phỏng đồng thuận blockchain

Một mạng các nút tạo và chia sẻ khối trong điều kiện có độ trễ, để thử xem kích thước khối, thời điểm và kẻ tấn công ảnh hưởng thế nào đến an ninh và thông lượng.

Câu hỏi nó trả lời: Một blockchain an toàn và nhanh đến đâu khi mạng bị trễ và bị tấn công?

Bỏ qua: Hành vi nút thật và cấu trúc mạng chỉ được đo một phần.

Chạy trên: khoảng 10⁸ FLOPS sơ lược các lần chạy theo sự kiện hàng nghìn nút.Từ: 2016 Phân tích an ninh và hiệu năng của Gervais và các đồng nghiệp về các blockchain bằng chứng công việc với một trình mô phỏng. nguồn

Mô phỏng sự kiện rời rạc song song

Một mô phỏng các sự kiện theo thời gian được chia cho nhiều bộ xử lý, mỗi bộ tự tiến đồng hồ của mình và quay lui nếu có thông điệp đến muộn.

Câu hỏi nó trả lời: Làm sao một mô phỏng khổng lồ hướng sự kiện, như một mạng hay một chiến trường, chạy nhanh trên nhiều máy?

Bỏ qua: Việc hoàn nguyên có thể dây chuyền, và mức tăng tốc phụ thuộc nhiều vào mức độ các sự kiện gắn chặt với nhau.

Chạy trên: khoảng 10¹⁴ FLOPS sơ lược giờ trên một siêu máy tính cho hàng tỷ sự kiện.Từ: 1985 Thời gian ảo của Jefferson, cơ chế Time Warp cho đồng bộ hóa lạc quan. nguồn

Mô phỏng kiến trúc bộ xử lý đồ họa

Các lõi, warp và bộ nhớ của một bộ xử lý đồ họa được mô hình hóa từng chu kỳ, chạy các chương trình thật để đánh giá thiết kế trước khi chế tạo.

Câu hỏi nó trả lời: Một thay đổi thiết kế sẽ ảnh hưởng thế nào đến tốc độ của các chương trình song song trên chip đồ họa?

Bỏ qua: Chi tiết của các chip thật là bí mật hoặc chưa biết, nên mô hình chỉ khớp sơ lược với các con số của những thiết kế hiện có.

Chạy trên: khoảng 10¹² FLOPS sơ lược vài giờ đến vài ngày thời gian máy chủ cho mỗi giây thực thi mô phỏng.Từ: 2009 Phân tích của Bakhoda và các đồng nghiệp về khối lượng công việc CUDA bằng một trình mô phỏng GPU chi tiết. nguồn

Mô phỏng hệ thống tăng tốc bằng FPGA

Một thiết kế chip được nạp vào nhiều mạch có thể cấu hình lại, chạy chính xác từng chu kỳ ở tốc độ megahertz, mô phỏng cả máy chủ và mạng lưới của chúng.

Câu hỏi nó trả lời: Bộ xử lý này và cụm máy của nó sẽ hoạt động thế nào khi chạy phần mềm thật, trước khi được chế tạo?

Bỏ qua: Nó chậm hơn con chip thật rất nhiều, và một thiết kế không vừa với các mạch thì không chạy được.

Chạy trên: khoảng 10¹⁵ FLOPS sơ lược vài ngày trên một đám mây gồm hàng trăm mạch có thể cấu hình lại.Từ: 2018 FireSim của Karandikar và các đồng nghiệp, mô phỏng hệ thống mở rộng chính xác đến từng chu kỳ, tăng tốc bằng FPGA trên đám mây công cộng. nguồn

Mô phỏng toàn hệ thống

Cả một máy tính, với bộ xử lý, bộ nhớ, ổ đĩa và card mạng, được mô phỏng đủ tốt để khởi động một hệ điều hành nguyên bản và chạy các chương trình của nó.

Câu hỏi nó trả lời: Phần mềm thật hành xử ra sao trên một cỗ máy chưa tồn tại, hoặc có thể tạm dừng và phát lại tùy ý?

Bỏ qua: Thời gian được tính gần đúng cho nhanh, nên nó không thể cho hiệu năng chính xác, chỉ cho hành vi chức năng.

Chạy trên: khoảng 10¹¹ FLOPS sơ lược gần thời gian thực trên một máy chủ cho mỗi máy mô phỏng.Từ: 2002 Simics của Magnusson và các đồng nghiệp, một nền tảng mô phỏng toàn hệ thống. nguồn

Mô phỏng mạng nhẹ

Hàng chục hay hàng trăm máy chủ và bộ chuyển mạch ảo chạy phần mềm mạng thật trên một máy tính xách tay, nối bằng cáp giả lập với tốc độ và độ trễ đặt trước.

Câu hỏi nó trả lời: Chương trình điều khiển mạng này có chạy được trên cả một cấu trúc liên kết trước khi triển khai không?

Bỏ qua: Bộ xử lý của máy chủ được dùng chung cho mọi nút ảo, nên các liên kết nhanh bị làm chậm.

Chạy trên: khoảng 10¹⁰ FLOPS sơ lược thời gian thực trên một máy trạm.Từ: 2010 Lantz, Heller và McKeown, "A network in a laptop", tạo mẫu nhanh cho mạng xác định bằng phần mềm. nguồn

Luyện kim mô phỏng

Một máy tính làm nguội từ từ một mô hình nguyên tử hay một thiết kế, đôi khi chấp nhận những cách sắp xếp tệ hơn, để tìm lời giải tốt cho một bài toán tối ưu khó.

Câu hỏi nó trả lời: Đâu là bố cục hay lịch trình gần tối ưu trong vô số khả năng?

Bỏ qua: Nó không đảm bảo đáp án tốt nhất, và kết quả phụ thuộc vào lịch trình làm nguội.

Chạy trên: khoảng 10¹² FLOPS sơ lược giờ trên một máy trạm cho một lần bố trí chip.Từ: 1983 Kirkpatrick, Gelatt và Vecchi, tối ưu hóa bằng luyện kim mô phỏng. nguồn

Tính toán Bayes xấp xỉ

Một trình mô phỏng được chạy với nhiều giá trị tham số thử, rồi những giá trị cho ra dữ liệu gần với dữ liệu quan sát được thì được giữ lại, cho một bức tranh về những giá trị nào khả dĩ.

Câu hỏi nó trả lời: Những thiết lập nào của một mô hình phức tạp có thể đã tạo ra dữ liệu ta quan sát?

Bỏ qua: Kết quả phụ thuộc vào việc dùng những tóm tắt nào của dữ liệu và mức khớp phải gần đến đâu mới được tính.

Chạy trên: khoảng 10¹³ FLOPS sơ lược hàng triệu lần chạy bộ mô phỏng trên một cụm máy.Từ: 1997 Suy luận thời gian hợp nhất từ dữ liệu trình tự DNA bằng mô phỏng của Tavaré và cộng sự. nguồn