Claude phạm luật TPC-H để thắng Umbra 22 lần

Ngày 02/11/2026, Jiale Lao và giáo sư Immanuel Trummer ở Đại học Cornell đăng bài báo GenDB-V lên arXiv, tiêu đề mở bằng câu "Stop Handcrafting Your Engine!" ^[1]. Nhóm cho agent Claude Opus 5.5 tự viết code Rust chạy truy vấn SQL, bắt code đó qua bộ kiểm chứng toán học Verus với 0 lỗi, rồi báo cáo trên bộ đo TPC-H tốc độ trung bình nhân nhanh gấp 22 lần Umbra 26.08 và 51,6 lần DuckDB 1.5.6.

Ngày 07/11, giáo sư Thomas Neumann ở Đại học Kỹ thuật München, đồng tác giả HyPer và Umbra, viết rằng nhanh gấp 22 lần Umbra là chuyện không thể, ít nhất với cách xử lý truy vấn thông thường ^[2]. Ba ngày sau, Jiale Lao vào phần bình luận dưới bài đó, nhận đã tuyên bố quá mức về hiệu năng ^[3].

Phép chia nhẩm 280 ms của Thomas Neumann

Câu hỏi cộng doanh thu trên một cột chưa tính sẵn thì join hay filter khéo tới đâu cũng phải kéo đủ từng byte của cột đó từ RAM lên CPU, như kiểm kho thì nhanh mấy cũng phải chờ bê hết thùng hàng qua cửa kho.

Bài báo đo trên máy chủ hai chip Intel Xeon Gold 5218 (32 nhân, 64 luồng, 384 GB RAM) ^[1]. Neumann kiểm con số đó bằng một phép chia trên con Ryzen 9 9950X3D, với Umbra, hệ cơ sở dữ liệu biên dịch câu SQL ra mã máy. Ở quy mô TPC-H SF10 (khoảng 10 GB dữ liệu thô), 22 câu truy vấn đọc tổng cộng chừng 15 GB dữ liệu đã nén. Con chip đó đọc RAM được khoảng 54 GB/s, nên riêng việc đọc đã mất:

\[t_{\min} = \frac{15\text{ GB}}{54\text{ GB/s}} \approx 280\text{ ms}\]

Umbra chạy xong 22 câu trên máy đó trong khoảng 540 ms, chưa tới 2 lần thời gian đọc ^[2]. Theo Neumann, nén tốt hơn có thể kéo con số 280 ms xuống chút ít, nhưng không tới 10 lần. Nếu câu nào cũng nhanh gấp 22 lần Umbra thì cả 22 câu chỉ còn \({540} / 22 \approx 24{,}5\text{ ms}\), dưới sàn đọc RAM hơn 11 lần.

31 cấu trúc tính sẵn lúc load dữ liệu

TPC-H là bộ đo hiệu năng phân tích dữ liệu kinh doanh do Hội đồng TPC ban hành, mô phỏng dữ liệu một doanh nghiệp bán buôn trong 8 bảng (orders lưu đơn hàng, lineitem lưu từng món hàng trong đơn, customer lưu khách hàng, supplier lưu nhà cung cấp, part, partsupp, nation, region) cùng 22 mẫu câu hỏi về doanh thu, tồn kho, giao hàng trễ ^[4]. Ở quy mô SF100 (scale factor 100), công cụ chính thức dbgen đẻ ra khoảng 100 GB dữ liệu giả, riêng lineitem có 600 triệu dòng và orders có 150 triệu đơn.

Bộ đo trước TPC-H là TPC-D, ra năm 1995 và bị khai tử năm 1999. Neumann kể người ta tối ưu riết cho TPC-D tới mức thời gian chạy tụt về gần 0 vì cache quá tay, và TPC-H sửa bằng cách tự nhận là bộ đo ad-hoc, cấm khai thác hiểu biết về bộ câu hỏi hay cache kết quả ^[5]. Trong quy chuẩn, Điều 1.5.7 chỉ cho dựng index hay materialized view trên khoá chính, khoá ngoại hoặc cột ngày, còn Điều 0.2 cấm "benchmark special", tức cách cài đặt làm đẹp số đo mà ngoài đời không dùng được ^[4].

Neumann chỉ ra phần tăng tốc lớn nhất của GenDB-V đến từ việc tính sẵn ^[2]. Ở chế độ agent tự thiết kế lưu trữ, agent đọc trọn 22 câu SQL rồi dựng lại lớp lưu trữ lúc load dữ liệu ^[6]. Agent dựng sẵn 31 cấu trúc phụ may đo cho từng câu hỏi. Câu Q2 tìm 100 nhà cung cấp có số dư tài khoản (s_acctbal) cao nhất thoả điều kiện vùng và chi phí tối thiểu, nên agent dựng suppliers_rank xếp sẵn nhà cung cấp theo s_acctbal giảm dần. Lúc bấm giờ ở SF100 trên 1 luồng, Q2 dừng ngay khi nhặt đủ 100 dòng đầu, mất 0,726 ms so với 322,755 ms của Umbra ^[6]. Q22 lọc mã vùng điện thoại có sẵn cust_phoneidx, Q13 lọc ghi chú bằng NOT LIKE có sẵn index bộ ba ký tự factext_trisig, Q9 và Q16 có partsig và supp_trisig.

Nhóm Cornell chạy thêm chế độ mảng phẳng (plain array) để tách phần viết code truy vấn khỏi phần tối ưu lưu trữ: cột giữ nguyên dạng mảng thô theo thứ tự dòng của file gốc, không sắp xếp, không nén, không index ^[1]. Ở chế độ tự thiết kế lưu trữ, 19/22 câu nhanh hơn đối thủ nhanh nhất ít nhất 5 lần ở cả 9 ô đo (3 bộ tham số nhân 3 mức luồng). Sang mảng phẳng, chỉ còn Q18 giữ được mức đó ^[6].

12 câu vẫn hardcode quy luật của dbgen

dbgen không đánh số đơn hàng liền mạch. Cứ mỗi chùm 32 mã liên tiếp, nó chỉ dùng 8 mã đầu, tức các số chia 32 dư 0 tới 7 (chùm đầu bỏ số 0, nên bắt đầu từ 1). Quy luật này nằm trong macro MK_SPARSE của dbgen, và Điều 4.2.3 của quy chuẩn TPC-H ghi rõ bên chạy benchmark không được lợi dụng nó ^[4]. Với thứ tự đơn \(i\) đếm từ 1, mã đơn \(k\) là:

\[k = 32 \cdot \lfloor i / 8 \rfloor + (i \bmod 8)\]

Anh thủ thư Minh coi một tủ hồ sơ đơn hàng, vừa xếp 10 đơn đầu do dbgen sinh ra vào 10 ngăn đánh số 0 tới 9: [1, 2, 3, 4, 5, 6, 7, 32, 33, 34]. Khách hỏi đơn mã 33 để nối sang thông tin người mua. Query engine bình thường không biết mã đơn sinh theo công thức nào, nên trên mảng phẳng chưa có index nó phải quét cột khoá để dựng hash join, hoặc binary search nếu biết cột đã tăng dần.

Ở câu Q18, agent của GenDB-V viết hàm đảo ngược công thức này vào lookup.rs ^[7]. Khách hỏi mã \(k = 33\), cậu phụ việc AI làm theo code đó: kiểm \({33} \bmod 32 = 1 \lt 8\), tính ngược \(i = 8 \cdot \lfloor 33 / 32 \rfloor + 1 = 9\), suy ra hồ sơ ở ngăn \(g = i - 1 = 8\). Cậu rút ngăn 8, thấy nhãn đúng 33, trao hồ sơ sau 1 lần mở ngăn, khỏi dựng hash table trên 150 triệu đơn của SF100. Cùng tệp đó, find_cust coi khách hàng mã k nằm ở dòng k - 1, vì dbgen đánh số khách hàng liền mạch ^[7].

Neumann chỉ nêu ví dụ Q18 ^[2]. Mình đọc cả 22 thư mục truy vấn mảng phẳng và thấy 12 câu hardcode quy luật của dbgen vào code ^[8]. Q9 đoán vị trí đơn hàng bằng phép dịch bit và coi 4 nhà cung cấp của mặt hàng thứ r luôn nằm ở dòng 4 * r + j của partsupp; lệch một dòng là cả tác vụ bỏ ngang (bail) để quay về nhánh chậm. Q21 là câu Mục 6.5 của bài báo đem ra khoe, bản mảng phẳng thắng Umbra 5,1 lần ^[1], trong khi code của nó coi mọi tên nhà cung cấp đúng khuôn Supplier#000000001 là không trùng nhau.

Đoán trước vị trí rồi dùng if kiểm lại trông giống đoán nhánh trên CPU, chỉ khác là CPU đoán trượt mất vài chục chu kỳ, còn lookup.rs đoán trượt phải quét tuần tự cả trăm triệu dòng.

Q18 sau khi xoá 1 đơn hoặc chèn 1 dòng

Khách huỷ đơn mã 1 (DELETE FROM orders WHERE o_orderkey = 1), đúng kiểu lệnh xoá trong hàm refresh RF2 của chính TPC-H ^[4]. Các hồ sơ còn lại dồn lên thành 9 ngăn [2, 3, 4, 5, 6, 7, 32, 33, 34]. Khách vẫn hỏi đơn 33. Cậu phụ việc vẫn nhẩm ra ngăn 8, nhưng giờ ngăn 8 chứa đơn 34. Phép kiểm okey[g] == k trả về sai, chương trình rơi xuống search(okey, no, k), một vòng while lật từng ngăn bắt đầu ở ngăn 0, tới ngăn 7 mới thấy đơn 33 ^[7]. Mất một hồ sơ đầu tủ là mọi đơn phía sau lệch đi 1 ngăn, không lần đoán nào trúng nữa.

Neumann viết rằng xoá hay chèn một dòng nhiều khả năng đẩy cả cách làm này vào nhánh dự phòng chậm ^[2]. Mình chép find_order, find_cust và search sang C rồi chạy trên Apple M4 Pro, với 1,5 triệu đơn và 150.000 khách hàng mang mã sinh đúng công thức của dbgen, số lượng món hàng ngẫu nhiên, cỡ SF1 (1/100 của SF100).

Ở ngưỡng 300 (HAVING SUM(l_quantity) > 300, giá trị quy chuẩn TPC-H dùng để kiểm đáp án ^[4]), 72 đơn qua ngưỡng. Trên dữ liệu chưa xoá, logic của GenDB-V dò xong 72 đơn trong 0,00046 ms. Xoá dòng đầu của orders (o_orderkey = 1) và customer (c_custkey = 1) thì binary search mất 0,00272 ms, còn logic của GenDB-V mất 18,333 ms, chậm 40.204 lần so với trước khi xoá. Hạ ngưỡng xuống 250 thì có 6.555 đơn qua ngưỡng, và xoá 1 dòng đầu đẩy thời gian dò từ 0,020 ms lên 1.724,46 ms, chậm 86.452 lần. Vòng build_cands gọi find_order trong Q18 chỉ chạy 1 luồng. Ngoại suy lên SF100, số đơn và số ứng viên cùng gấp 100 lần nên chi phí gấp khoảng 10.000 lần: câu Q18 vốn chạy 158 ms trên 64 luồng sẽ mất cỡ 3 phút ở ngưỡng 300 và gần 5 giờ ở ngưỡng 250.

Q18 còn một nhánh dự phòng thứ hai, ở bước gom nhóm trong runplan.rs ^[9]. Trước khi dò orders, Q18 phải cộng số lượng theo từng đơn trên lineitem (600 triệu dòng ở SF100). Nhánh nhanh runscan giả định cột l_orderkey tăng dần như lúc dbgen vừa xuất xưởng. Ngoài đời, khách thêm 1 món vào đơn số 1 là có một dòng mới nằm cuối lineitem, thứ tự tăng dần vỡ, kết quả của 64 luồng bị bỏ và chương trình gọi scan_general trên 1 luồng. Comment ngay trên hàm này ghi Any row order; quadratic time.: với mỗi mã đơn mới gặp, nó quét lại cả bảng lineitem để cộng dồn ^[9].

Chạy bản C của scan_general với 60.000 dòng lineitem (0,01% của SF100), đường nhanh mất 0,034 ms; nối thêm 1 dòng của đơn số 1 vào cuối thì lên 725,67 ms, chậm 21.243 lần. Lên 240.000 dòng, đường nhanh mất 0,119 ms, còn dòng nối thêm làm scan_general mất 11.713,81 ms, tăng 16,14 lần khi dữ liệu tăng 4 lần, khớp \({4}^2 = 16\) của thời gian bậc hai. Ngoại suy lên 600 triệu dòng của SF100, gấp 2.500 lần nên chậm thêm \({2.500}^2 = 6.250.000\) lần, một dòng chèn muộn sẽ bắt Q18 chạy hơn 2 năm trên 1 nhân CPU.

Điểm mù độ phức tạp trong đặc tả Verus

Bình thường bạn kiểm phần mềm bằng test: đưa vào 10 hay 1.000 bộ dữ liệu mẫu xem kết quả có khớp không, và không ai chắc tới bộ thứ 1.001 chương trình có cộng sai hay tràn số không. Formal verification đi hướng khác. Nhóm Cornell viết SQLSpec, bản đặc tả toán học của SQL mà agent không được sửa, rồi cho Verus dịch code Rust của agent thành các mệnh đề logic để bộ giải Z3 kiểm ^[1]. Code chỉ được build khi Z3 chứng minh được rằng với mọi cơ sở dữ liệu hợp lệ \(D\) và mọi tham số, kết quả đúng như định nghĩa của câu SQL, không đọc tràn mảng, và mọi vòng lặp đều dừng (GenDB-V cấm unsafe và lệnh bỏ qua chứng minh assume).

Ở Mục 6.4, bài báo so với Bespoke OLAP, một hệ cũng dùng LLM sinh engine riêng cho từng workload nhưng chỉ kiểm bằng test, và tìm ra code của nó trả sai âm thầm ở 16/28 mẫu câu hỏi ^[1]. Code Bespoke OLAP viết cho câu Q6 của bộ dữ liệu tài chính SEC-EDGAR dùng một số âm lớn làm sentinel cho tập rỗng. Ngay trên dữ liệu SF3 gốc, một tham số tiền tệ chưa gặp cho tổng âm sâu hơn hằng số đó, và chương trình bỏ mất một nhóm, trả 21 dòng thay vì 22.

Nhưng ông thanh tra Verus chỉ kiểm những gì được viết thành hợp đồng. Hợp đồng của find_order đòi ba điều về giá trị trả về \(j\): \(j \le n_o\); nếu \(j \lt n_o\) thì ngăn \(j\) chứa đúng khoá cần tìm (\(\text{okey}[j] = k\)); nếu \(j = n_o\) thì cả mảng không có khoá \(k\) ^[7]:

pub fn find_order(okey: &'static [i64], no: usize, k: i64) -> (j: usize)
    requires [email protected]() == no,
    ensures j <= no, j < no ==> okey@[j as int] == k, j == no ==> !has_key(okey@, k),
{
    if k > 0 {
        let ku = k as u64;
        let low = ku % 32;
        if low < 8 {
            let i = (ku / 32) * 8 + low;
            if i >= 1 && i - 1 < no as u64 {
                let g = (i - 1) as usize;
                if okey[g] == k { return g; }
            }
        }
    }
    search(okey, no, k)
}

Điều kiện ensures đúng với mọi công thức đoán g. Đoán trúng thì chính phép kiểm okey[g] == k bảo đảm ngăn g chứa mã k; đoán trượt thì chứng minh dựa hết vào search, hàm quét từ đầu bảng. Hợp đồng chỉ hỏi hồ sơ trao ra có đúng số 33 không, không đếm cậu phụ việc mở 1 ngăn hay 150 triệu ngăn.

Trong phần bình luận, Neumann cho rằng có thể viết một chương trình băm dữ liệu lúc load để nhận ra bộ TPC-H chuẩn ở từng scale factor, rồi trả đáp án mọi câu chỉ từ hiểu biết về bộ sinh dữ liệu, không cần đọc dữ liệu; gặp dữ liệu khác thì chuyển sang một DuckDB, Postgres hay SQLite nhúng ^[3]. Lao đáp rằng chương trình đó không qua nổi Verus: hai cơ sở dữ liệu khác nhau có thể trùng giá trị băm, và chưa engine SQL production nào có sẵn chứng minh để làm nhánh lùi. Hiện GenDB-V lùi về engine của chính nó, theo lời Lao là có chứng minh nhưng chậm. find_order làm đúng như vậy, chỉ thay phép băm bằng phép so khoá ở một ngăn.

Cách GenDB-V cho agent làm việc có thể đã khiến agent viết nhánh dự phòng chậm. Agent thử tốc độ ở chế độ tắt kiểm chứng trước, chọn thiết kế nhanh nhất, rồi mới viết chứng minh cho thiết kế đó ^[1]. Nhánh else không bao giờ chạy khi đo trên dữ liệu TPC-H, nên chậm cỡ nào cũng không mất điểm, nhưng vẫn phải có chứng minh Verus đầy đủ. Chính bài báo viết rằng kế hoạch thực thi đơn giản thì dễ chứng minh mà chạy chậm.

Jiale Lao trả lời Neumann

Trong các bình luận ngày 10/11, Lao gọi phần kiểm chứng là điểm chính của GenDB-V ^[3]. Chứng minh hình thức nhân hệ điều hành seL4, khoảng 8.700 dòng C, từng tốn cỡ 20 năm công sức chuyên gia; GenDB-V để agent tự viết cả code lẫn chứng minh, tốn 1.229 đến 1.868 USD tiền API cho mỗi chế độ chạy trên TPC-H ^[1].

Lao cũng chỉ sang chế độ thứ hai ở Mục 6.3: agent viết một engine đa dụng duy nhất, nhận câu SQL bất kỳ trong tập con mà SQLSpec hỗ trợ ^[1]. Engine này dài khoảng 104.000 dòng, 68% là đặc tả và chứng minh. Ở SF100, nó chạy xong 22 câu TPC-H trong 109,3 giây trên 1 luồng và 9,16 giây trên 64 luồng, nhanh hơn Umbra 1,52 và 1,27 lần, nhanh hơn DuckDB 3,4 và 1,8 lần. Theo Lao, trên các câu truy vấn mới viết tay mà agent chưa thấy, engine này vẫn chậm hơn Umbra.

Lao xin lỗi vì tiêu đề bài báo nói một khả năng như thể đã xảy ra, và đồng ý rằng đoán vị trí khoá theo dbgen là khớp với bộ sinh dữ liệu chứ không khớp với khách hàng nào. Lao cũng nhận chứng minh không nói gì về hiệu năng: một phép tối ưu đúng với mọi cơ sở dữ liệu nhưng chỉ nhanh với một số. Tối hôm đó, Lao hứa chạy lại với thiết lập chặt hơn, chẳng hạn dữ liệu TPC-H lệch phân phối sinh bằng công cụ của Microsoft mà agent không thấy lúc sinh code ^[3].

Neumann đề xuất hai điều kiện để chặn chuyện này: người viết engine không được biết bộ đo trước lúc chạy, và dữ liệu phải đổi theo thời gian để loại các kiểu tính sẵn quá đà ^[3]. Với agent, đổi dữ liệu có thể là trộn sẵn các lệnh INSERT, DELETE làm xô thứ tự dòng trước khi bấm giờ, và bấm giờ cả lúc nhánh nhanh đoán trượt, để vòng lặp dự phòng bậc hai lộ ra ngay.

Đào sâu: phép dịch bit trong Q9

Ở Q9, thay vì chia và lấy dư cho 32 như Q18, agent viết hàm đoán dòng đơn hàng bằng phép dịch bit ^[8]:

fn order_guess(k: i64) -> (o: u64)
    no_unwind
{
    if k > 0 {
        let ku = (k - 1) as u64;
        ((ku >> 5u64) << 3u64) | (ku & 7u64)
    } else {
        u64::MAX
    }
}

Vì \({32} = 2^5\) và \({8} = 2^3\), với mọi khoá của dbgen có \({1} \le (k \bmod 32) \le 7\), trừ 1 rồi dịch phải 5 bit (ku >> 5), dịch trái 3 bit (<< 3) và ghép 3 bit thấp (ku & 7) cho ra đúng chỉ số dòng i - 1 tính từ 0, chỉ bằng vài phép bit. Khoá chia hết cho 32 cũng ra đúng. Đơn thứ 8 (\(i = 8\)) có khoá \(k = 32 \cdot 1 + 0 = 32\); find_order của Q18 tính low = 32 % 32 = 0, i = 1 * 8 + 0 = 8, g = 7, còn order_guess của Q9 tính ku = 31, (31 >> 5 << 3) | (31 & 7) = 0 | 7 = 7.

Bình