Hai nhóm cùng giải bài toán tồn tại hơn một thập kỷ, hẹn nhau công bố lúc 15h

Mới đây, câu chuyện của hai nhóm nghiên cứu độc lập, trong đó có nhóm của TS Vũ Khắc Kỷ - giảng viên Bộ môn Toán, Trường Đại học FPT cùng công bố chứng minh cho giả thuyết Courtade - Kumar, bài toán được đặt ra từ năm 2013 trong lý thuyết thông tin và giải tích hàm Boolean đã nhận được nhiều quan tâm của giới khoa học.

Điều đặc biệt là hai nhóm không biết về công trình của nhau cho đến khi gần hoàn tất. Khi phát hiện cùng đi đến lời giải, thay vì cạnh tranh về thời điểm công bố, hai bên trao đổi để xác nhận tính độc lập của các chứng minh và thống nhất đưa hai bản thảo lên cộng đồng khoa học cùng ngày, vào đúng 15h theo giờ Hong Kong (Trung Quốc).

“Với tôi, đây là câu chuyện đẹp của nghiên cứu khoa học”, TS Vũ Khắc Kỷ nói.

PV Báo điện tử Báo Điện tử VTC News trao đổi với TS Vũ Khắc Kỷ về kết quả nghiên cứu và câu chuyện đặc biệt phía sau quá trình phối hợp của hai nhóm công bố cùng thời điểm.

Bài toán hơn 10 năm chưa có lời giải tổng quát

- Anh có thể giới thiệu ngắn gọn về giả thuyết Courtade-Kumar và kết quả vừa được công bố?

Có thể hình dung bài toán như sau: Ta có một nguồn dữ liệu gồm nhiều bit độc lập. Dữ liệu được truyền qua một kênh nhiễu, trong đó mỗi bit có thể bị thay đổi với một xác suất nhất định. Trước khi truyền, ta muốn nén toàn bộ dữ liệu thành một bit duy nhất.

Câu hỏi là nên chọn hàm nào của dữ liệu ban đầu để sau khi quan sát phiên bản bị nhiễu, ta vẫn thu được nhiều thông tin nhất về bit đã nén.

Giả thuyết Courtade - Kumar dự đoán rằng phương án tối ưu có cấu trúc rất đơn giản: chỉ cần chọn một bit ban đầu. Trong giải tích hàm Boolean, những hàm chỉ phụ thuộc vào tọa độ như vậy được gọi là dictator functions.

Điểm đáng chú ý là dù ta có thể kết hợp các bit đầu vào theo vô số cách phức tạp, không cách nào giữ lại nhiều thông tin hơn việc lựa chọn một tọa độ thích hợp.

Sau hơn một thập kỷ, hai bản thảo độc lập đưa ra hai chứng minh cho giả thuyết trong trường hợp tổng quát: một của GS Trần Mạnh Tuấn và tôi, một của nhóm bảy nhà khoa học đến từ Google, Chinese University of Hong Kong và một số trường đại học khác.

Tất nhiên, việc công bố bản thảo mới là bước đầu. Các chứng minh vẫn cần được cộng đồng đọc, kiểm tra và phản biện kỹ lưỡng.

- Vì sao một bài toán có phát biểu khá ngắn lại khó giải quyết?

Kể từ khi được đề xuất năm 2013, giả thuyết thu hút sự quan tâm liên tục của các nhà nghiên cứu trong lý thuyết thông tin, xác suất và giải tích hàm Boolean. Nhiều kết quả quan trọng được thiết lập cho những miền tham số hoặc lớp hàm đặc biệt nhưng trường hợp tổng quát vẫn còn mở.

Một lý do là lớp đối tượng cần kiểm soát có quy mô rất lớn. Một hàm Boolean trên (n) bit được xác định bởi giá trị của nó tại (2^n) đầu vào, nên tổng số hàm có thể có là (2^{2^n}). Trong khi đó, (n) có thể lớn tùy ý và tham số nhiễu biến thiên liên tục.

Vì vậy, ta không thể kiểm tra từng hàm, từng số chiều hay từng giá trị của tham số. Chứng minh phải tìm ra một nguyên lý áp dụng đồng thời cho mọi hàm Boolean, mọi số chiều và toàn bộ miền nhiễu.

Ngoài ra, thông tin tương hỗ là một đại lượng phi tuyến, phụ thuộc vào toàn bộ phân phối của hàm sau khi đi qua kênh nhiễu. Nhiều công cụ quen thuộc chỉ kiểm soát được một vài mômen, một phần phổ Fourier hoặc một lớp hàm cụ thể. Khoảng cách giữa trực giác đơn giản của phát biểu và một chứng minh hoàn chỉnh vì thế khá lớn.

- Hai chứng minh tiếp cận bài toán theo những hướng nào?

Chứng minh của chúng tôi phát triển một khung entropy - phổ mới, dựa trên sự tương tác giữa entropy, toán tử nhiễu và cấu trúc phổ Fourier của hàm Boolean. Bản thảo dài khoảng 36 trang; phần lõi là các lập luận giải tích, cùng một lượng nhỏ tính toán có thể tái lập để kiểm tra một số bất đẳng thức cụ thể.

Công trình của nhóm quốc tế phát triển phương pháp dựa trên phương trình vi phân và một bài toán Bellman hữu hạn chiều, kết hợp phân tích với các phép tính được chứng nhận bằng máy tính. Chứng minh của họ còn được hình thức hóa và kiểm tra bằng Lean.

Tôi chỉ muốn mô tả sự khác biệt ở mức đó. Việc đánh giá sức mạnh, khả năng mở rộng và ý nghĩa lâu dài của mỗi phương pháp nên thuộc về cộng đồng sau khi hai bản thảo được nghiên cứu đầy đủ.

Đối với chúng tôi, việc hai nhà toán học Việt Nam có thể xây dựng một chứng minh độc lập và hoàn chỉnh cho một bài toán đã được cộng đồng quốc tế theo đuổi hơn mười năm là một niềm vui lớn. Tuy nhiên, chúng tôi ý thức rằng giá trị của công trình cuối cùng phải được xác lập qua quá trình kiểm tra và phản biện khoa học.

Hai nhóm bất ngờ “gặp nhau” trước giờ công bố

- Cơ duyên nào đưa anh đến với giả thuyết này?

Khoảng 10 năm trước, khi tôi làm nghiên cứu sau tiến sĩ tại Viện ITCSC thuộc Chinese University of Hong Kong, GS Chandra Nair là người đầu tiên giới thiệu giả thuyết này với tôi.

Khi đó, tôi dành gần 2 năm theo đuổi bài toán nhưng chưa tìm được lời giải. Sau khi trở về Việt Nam và bắt đầu giảng dạy tại Trường Đại học FPT từ năm 2019, tôi vẫn thỉnh thoảng quay lại. Mỗi lần như vậy, tôi hiểu thêm một khía cạnh nhưng các công cụ khi đó chưa đủ để xử lý toàn bộ khó khăn.

Trong một thời gian dài, GS Nair và tôi gần như không trao đổi về giả thuyết Courtade - Kumar. Vì vậy, hai nhóm đã phát triển phương pháp của mình một cách độc lập.

- GS Trần Mạnh Tuấn đóng vai trò thế nào trong công trình?

Đây là công trình đồng tác giả theo đúng nghĩa. Anh Tuấn có nền tảng rất mạnh về xác suất rời rạc và tổ hợp, đồng thời đặc biệt thận trọng với những bất đẳng thức có vẻ hợp lý nhưng chưa được chứng minh đầy đủ.

Trong quá trình nghiên cứu, chúng tôi liên tục trao đổi các phiên bản của lập luận, tìm phản ví dụ, điều chỉnh giả thiết và làm sắc các ước lượng. Tôi thường tiếp cận vấn đề từ góc nhìn entropy và phổ Fourier; anh Tuấn nhìn thấy những cấu trúc xác suất và tổ hợp phía sau các biểu thức giải tích. Nhiều bước quan trọng chỉ trở nên chính xác sau các vòng phân tích và phản biện như vậy.

Phần lớn trao đổi của chúng tôi diễn ra qua Messenger. Một người đưa ra một mệnh đề hoặc một cơ chế, người kia cố gắng tìm điểm yếu. Quá trình ấy đôi khi khá căng thẳng, nhưng chính sự phản biện trực tiếp đó giúp bản thảo trở nên chắc chắn hơn.

- Anh biết nhóm của GS Chandra Nair cũng vừa hoàn thành một chứng minh thế nào?

Khi chứng minh của chúng tôi hoàn thành, tôi chủ động viết email cho GS Nair, ban đầu chỉ định thông báo rằng GS Tuấn và tôi đã hoàn thành một chứng minh.

GS Nair trả lời rằng nhóm của ông, cùng các đồng nghiệp tại Google và một số trường đại học khác, cũng vừa hoàn tất một công trình giải quyết cùng bài toán.

Đó là một tình huống hoàn toàn bất ngờ. Bản thảo của chúng tôi khi ấy đã được gửi lên arXiv và dự kiến xuất hiện vào sáng hôm sau. Sau khi nhận được thông tin, chúng tôi chủ động dừng lần công bố đó để hai bên có thời gian trao đổi.

Tôi cho rằng việc cần làm trước tiên là xác định tính độc lập của hai công trình và tìm một phương án phản ánh công bằng hơn lịch sử của kết quả. Tôi viết thư cho GS Nair, nói rằng chúng tôi sẵn sàng điều chỉnh lịch để nhóm của ông hoàn tất những bước cuối cùng.

Đó không phải là sự từ bỏ ưu tiên của bất kỳ bên nào. Chúng tôi chỉ muốn ghi nhận chính xác rằng hai nhóm đã làm việc độc lập và đi đến kết quả gần như đồng thời.

- Hai bên xác định tính độc lập của các công trình và thống nhất cách công bố ra sao?

Hai nhóm trao đổi ở mức cần thiết về cấu trúc và những ý tưởng chính. Qua đối chiếu, hai bên nhận thấy các chứng minh được xây dựng trên những khung phương pháp khác nhau và không phụ thuộc vào công trình của nhau.

Sau đó, hai nhóm thống nhất công bố trong cùng một ngày, vào đúng 15h theo giờ Hong Kong.

Không nhóm nào muốn biến vài giờ chênh lệch thành một cuộc cạnh tranh về thứ tự. Đối với tôi, hình ảnh đáng nhớ nhất là hai nhóm ở những nơi khác nhau cùng chờ đến thời điểm đã hẹn để đưa công trình của mình ra cộng đồng.

Không tranh công bố trước, cùng mở hướng hợp tác

- Hai bên còn trao đổi về cách ghi nhận công trình của nhau trong bản thảo?

Đây có lẽ là phần tinh tế nhất.

Nếu một bên mô tả phương pháp của mình dài hơn hoặc sử dụng những từ ngữ mang tính đánh giá, người đọc có thể cảm thấy rằng đóng góp của một nhóm đang được đặt cao hơn nhóm còn lại, dù đó không phải chủ ý của các tác giả.

Tôi đề xuất rằng mỗi công trình chỉ được tóm tắt bằng đúng một cụm từ: chứng minh của chúng tôi là một khung entropy-production and spectral, còn chứng minh của nhóm quốc tế là một differential-equation approach. Không bên nào giải thích phương pháp của mình dài hơn hoặc sử dụng tính từ để xếp hạng.

Hai bên tự nguyện áp dụng cùng một giới hạn đối với chính mình để bảo đảm sự cân bằng.

Nếu đặt hai đoạn ghi nhận cạnh nhau, có thể thấy chúng gần như đối xứng: cấu trúc và mức độ ghi nhận tương đương, chỉ thay đổi tên nhóm, góc nhìn và cụm từ mô tả phương pháp. Tôi nghĩ cả hai phía đều hài lòng với cách viết này.

Chi tiết ấy tuy nhỏ nhưng có ý nghĩa. Sự tôn trọng không chỉ được nói ra mà còn được thể hiện trong chính văn bản khoa học.

- Phản ứng của các nhà khoa học phía bên kia thế nào?

Tôi không muốn nói thay họ, nhưng qua những trao đổi trực tiếp, tôi cảm nhận được thái độ thiện chí, thẳng thắn và chuyên nghiệp.

GS Nair chia sẻ rõ ràng về tình trạng công trình của nhóm ông và cùng chúng tôi tìm phương án phù hợp. Hai bên thống nhất ghi nhận công khai.

Sau khi công bố, ông Vahab Mirrokni, một trong những lãnh đạo nghiên cứu tại Google và là đồng tác giả của công trình bên kia, cũng công khai chúc mừng chứng minh độc lập của chúng tôi. Tôi rất trân trọng điều đó.

Nhìn lại, điều khiến tôi hài lòng nhất không phải là nhóm nào xuất hiện sớm hơn, mà là hai bên đã đi qua một tình huống nhạy cảm trong sự tôn trọng lẫn nhau.

- Quan hệ giữa hai nhóm thay đổi thế nào sau lần công bố này?

Quan hệ giữa hai nhóm trở nên gần gũi hơn.

Sau khi công bố, chúng tôi thường xuyên trao đổi về những tiến triển trong các dự án liên quan, đặc biệt là một bài toán mở khác mà cả hai phía đang thu được một số kết quả khả quan. Các trao đổi không còn chỉ nhằm xử lý một tình huống phát sinh, mà đã trở thành những thảo luận khoa học thực sự.

Hai bên cũng đã gửi cho nhau những lời mời hợp tác. Tôi hy vọng từ những trao đổi này sẽ hình thành các công trình chung trong tương lai.

Từ một hoàn cảnh rất dễ dẫn đến căng thẳng về ưu tiên, hai nhóm xây dựng thêm sự tin tưởng và mở ra khả năng hợp tác lâu dài. Đối với tôi, đó là kết quả đáng quý.

- Được biết chứng minh của nhóm quốc tế còn được hình thức hóa và kiểm tra bằng Lean?

Đúng vậy. Theo thông tin công bố trong bản thảo, chứng minh của họ, bao gồm các bước giải tích và những chứng chỉ số, được hình thức hóa và kiểm tra đầu-cuối bằng Lean.

Kho hình thức hóa được thống kê có quy mô khoảng 50 triệu dòng. Phần lớn trong số đó là dữ liệu chứng chỉ số được tạo bằng máy và được lõi kiểm tra của Lean xác nhận, chứ không phải 50 triệu dòng lập luận được viết thủ công. Dù hiểu theo nghĩa chính xác ấy, quy mô của hệ thống vẫn rất ấn tượng.

Tôi thực sự ngưỡng mộ công trình này. Xây dựng một chứng minh trên giấy đã khó; xây dựng thêm cả một chuỗi kiểm chứng hình thức đầu-cuối ở quy mô như vậy còn đòi hỏi năng lực toán học, kỹ thuật, tính toán và tổ chức rất lớn.

Khi hiểu đầy đủ hơn về khối lượng công việc của họ, tôi càng thấy nhẹ nhõm vì chúng tôi đã không vội vàng để bản thảo xuất hiện ngay trong đêm hôm trước. Nếu khi ấy chúng tôi chỉ nghĩ đến việc công bố sớm hơn vài giờ, nỗ lực rất lớn của những đồng nghiệp tại Chinese University of Hong Kong, Google và các trường đại học liên quan có thể bị thu hẹp thành một câu chuyện đơn giản về việc ai xuất hiện trước.

Điều đó sẽ không phản ánh đúng đóng góp của họ, cũng không phản ánh đúng tinh thần mà chúng tôi muốn giữ gìn trong khoa học.

- Câu chuyện này để lại cho anh bài học gì?

Cạnh tranh trong khoa học là điều tự nhiên và có thể tạo động lực. Tuy nhiên, cạnh tranh không nhất thiết phải đi kèm với việc làm lu mờ người khác.

Trong những tình huống nhạy cảm, đôi khi điều khó không chỉ là chứng minh một định lý, mà còn là tìm được cách ứng xử để mọi đóng góp được ghi nhận công bằng.

Việc hai nhóm độc lập cùng đưa ra lời giải không làm giảm giá trị của bên nào. Trái lại, nó giúp cộng đồng có thêm cơ sở để kiểm tra kết quả, so sánh các phương pháp và tìm kiếm những hướng phát triển mới.

Tôi hy vọng điều còn lại sau câu chuyện này không phải là câu hỏi nhóm nào công bố trước vài giờ, mà là hình ảnh hai nhóm đã hẹn nhau đúng 15h theo giờ Hong Kong, cùng đưa công trình của mình ra cộng đồng và dành cho nhau sự ghi nhận cân bằng nhất có thể.

Nếu từ sự tôn trọng đó hình thành thêm những hợp tác mới thì đây sẽ là một kết quả đẹp hơn bất kỳ cuộc đua nào.

TS. Vũ Khắc Kỷ tốt nghiệp chương trình Cử nhân Tài năng - Trường Đại học Khoa học Tự nhiên, Đại học Quốc gia Hà Nội, năm 2009, sau đó hoàn thành chương trình thạc sĩ tại TU Kaiserslautern, Đức.

Năm 2012, ông là nghiên cứu sinh duy nhất tại Pháp nhận học bổng tiến sĩ của Microsoft Research Cambridge. Sau khi bảo vệ luận án tiến sĩ tại École Polytechnique, Pháp, ông làm việc hai năm tại Viện ITCSC, Hong Kong. Từ năm 2019, ông là giảng viên Bộ môn Toán tại Trường Đại học FPT.

Ông từng là thành viên của dự án Flyspeck và đồng tác giả của công trình hình thức hóa chứng minh giả thuyết Kepler, một bài toán có lịch sử hơn 400 năm. Dự án đã xây dựng một phiên bản chứng minh được máy tính kiểm tra đầy đủ, góp phần hình thành mối quan tâm của ông đối với sự kết hợp giữa trực giác toán học, tính toán và các phương pháp kiểm chứng hình thức.