Trừu xuất hình thức khác gì so với trừu xuất toàn thể trong triết học?

Trừu xuất toàn thể là quá trình rút ra khái niệm phổ quát bao quát từ các cá thể đơn lẻ theo chiều rộng phân loại, trong khi trừu xuất hình thức là thao tác tách biệt phương diện cấu trúc, quy luật nội tại hoặc hình thức thuần túy ra khỏi chất liệu vật chất cụ thể để khảo sát độc lập.

Dự án Tóm tắt hình thức trong Toán học (Formal Abstracts - FAB) có mục tiêu gì?

Dự án FAB tập trung hình thức hóa các định nghĩa, phát biểu định lý và giả thuyết của bài báo toán học thành các bản tóm tắt hình thức (formal abstracts) mà máy tính và con người đều đọc được, bỏ qua các bước chứng minh chi tiết nhằm tối ưu hóa nhân lực và tạo lập kho ngữ nghĩa số hóa quy mô lớn.

Trừu xuất hình thức và các cơ sở tri thức hình thức hóa hỗ trợ gì cho trí tuệ nhân tạo?

Bằng cách loại bỏ sự mơ hồ của ngôn ngữ tự nhiên và cung cấp các đồ thị tri thức nhất quán về mặt logic, trừu xuất hình thức cùng các kho dữ liệu hình thức hóa giúp các mô hình trí tuệ nhân tạo có thể suy luận chính xác, truy vấn tự động và hỗ trợ các nhà toán học phát hiện các giả thuyết mới.

Nguyên lý trừu xuất trong triết học toán học tân Frege hoạt động như thế nào?

Theo trường phái tân Frege, nguyên lý trừu xuất giới thiệu một thuật ngữ mới trỏ tới một đối tượng trừu tượng thông qua một quan hệ tương đương xác lập trên các thực thể cơ sở, như việc định nghĩa số lượng dựa trên quan hệ tương đương song ánh giữa các tập hợp theo Nguyên lý Hume.

Trừu xuất hình thức (formal abstraction) là gì?

Trừu xuất hình thức (formal abstraction) là thao tác nhận thức và phương pháp luận trí tuệ nhằm tách biệt các phương diện cấu trúc, cú pháp, quy luật liên kết hoặc hình thức thuần túy của một đối tượng ra khỏi chất liệu cụ thể, nội dung ngữ nghĩa hay giá mang hiện thực của nó. Trong lịch sử tư tưởng học thuật, khái niệm này giữ vai trò then chốt trong nhận thức luận kinh viện để xác lập các phân ngành khoa học lý thuyết, đồng thời cung cấp cơ sở nhận thức luận cho logic học hình thức hiện đại và các tiến trình hình thức hóa tri thức. Bài viết trình bày bản chất nhận thức luận, nền tảng logic học tân Frege, sự giao thoa với các chương trình hình thức hóa toán học đương đại cùng những ranh giới học thuật cốt lõi của thao tác nhận thức này.

Bản chất nhận thức luận và nguồn gốc triết học

Trong nhận thức luận và triết học cổ điển, quá trình nhận thức của con người đi từ các dữ liệu cảm tính trực tiếp đến các biểu tượng trừu tượng mang tính bản chất. Để hình thành khái niệm khoa học, trí năng bắt buộc phải thực hiện các thao tác trừu xuất nhằm cô lập những phương diện nhất định của thực tại. Trường phái triết học Tôma truyền thống đã thiết lập sự phân biệt căn bản giữa hai phương thức nhận thức: trừu xuất toàn thể (abstractio totalis) và trừu xuất hình thức (abstractio formalis).

Trừu xuất toàn thể là tiến trình tư duy đi từ cái cụ thể đến cái phổ quát bằng cách bóc tách một khái niệm toàn thể phổ quát ra khỏi các phần tử cá thể cấu thành bên dưới. Thao tác này loại bỏ các đặc điểm cá biệt của từng đối tượng để giữ lại lớp khái niệm chung mang tính bao trùm, chẳng hạn như từ việc quan sát các cá thể sinh học cụ thể để rút ra khái niệm loài hoặc giống. Ngược lại, trừu xuất hình thức là thao tác trí tuệ bóc tách một phương diện bản chất, một phẩm tính quy định hoặc một cấu trúc hình thức ra khỏi vật chất cá thể hóa hoặc nền tảng vật chất bao bọc nó. Mục đích của trừu xuất hình thức không phải là mở rộng phạm vi bao quát của khái niệm theo chiều rộng phân loại, mà là đi sâu vào khảo sát các quy luật cấu trúc nội tại và hình thức thuần túy của đối tượng.

Năm 1959, tác giả Simmons đã khảo cứu chi tiết học thuyết kinh viện trên tạp chí The Thomist, phân tích hệ thống ba cấp độ trừu xuất hình thức làm cơ sở phân định ranh giới giữa các khoa học lý thuyết:

Cấp độ trừu xuất thứ nhất (Khoa học vật lý và tự nhiên): Trí năng trừu xuất bản chất của sự vật chuyển động ra khỏi vật chất cá thể cụ thể, nhưng khái niệm vẫn duy trì mối liên hệ không thể tách rời với vật chất cảm tính nói chung. Bản chất của các hiện tượng như sự vận động, nhiệt độ hay biến đổi sinh học không thể định nghĩa một cách đầy đủ nếu loại bỏ hoàn toàn các thuộc tính vật chất cảm giác.
Cấp độ trừu xuất thứ hai (Khoa học toán học): Trí năng tiến hành trừu xuất các hình thức định lượng (độ đo liên tục trong hình học hoặc số lượng rời rạc trong số học) ra khỏi vật chất cảm tính và những phẩm tính vật lý cụ thể như màu sắc, khối lượng hay vận tốc. Khái niệm toán học chỉ giữ lại mối quan hệ với vật chất khả tri, tức là sự mở rộng kích thước và cấu trúc hình học thuần túy.
Cấp độ trừu xuất thứ ba (Khoa học siêu hình học): Trí năng tách biệt hoàn toàn đối tượng nhận thức ra khỏi cả vật chất cảm tính lẫn vật chất khả tri, hướng đến nghiên cứu tồn tại với tư cách là tồn tại, cùng các phạm trù phổ quát như tính chân lý, tính thiện và bản nguyên tồn tại tối cao.

Sự phân định mạch lạc giữa hai phương thức trừu xuất nhận thức được khái quát thông qua bảng đối chiếu dưới đây:

Tiêu chí so sánh	Trừu xuất toàn thể (Abstractio totalis)	Trừu xuất hình thức (Abstractio formalis)
Bản chất thao tác	Rút ra cái chung phổ quát từ các cá thể đơn lẻ	Tách cấu trúc hình thức hoặc bản chất ra khỏi vật chất cụ thể
Chiều hướng nhận thức	Mở rộng quy mô phân loại theo chiều rộng (giống, loài)	Đi sâu vào khảo cứu cấu trúc nội tại và quy luật hình thức
Quan hệ với cá thể	Bao hàm các cá thể như những bộ phận cấu thành	Cô lập phương diện hình thức để khảo sát độc lập
Phạm vi áp dụng tiêu biểu	Phân loại học, hình thành khái niệm thường nghiệm	Toán học thuần túy, logic hình thức, siêu hình học

Trừu xuất hình thức trong logic học và triết học toán học

Khi bước sang kỷ nguyên logic học hiện đại, trừu xuất hình thức chuyển hóa từ một học thuyết tâm lý nhận thức thành một phương pháp luận toán học nghiêm ngặt. Trọng tâm của logic hình thức là khảo sát tính hợp lệ của các cấu trúc suy luận suy diễn mà không phụ thuộc vào giá trị chân lý cảm tính của các mệnh đề cụ thể cấu thành nên lập luận đó.

Trong ngôn ngữ tự nhiên, các phát biểu luôn bị pha trộn bởi ngữ cảnh, sắc thái biểu cảm và sự mơ hồ ngữ nghĩa. Thông qua quá trình trừu xuất hình thức, nhà logic học thay thế toàn bộ các đối tượng nội dung cụ thể bằng các biến ký hiệu và hệ thống toán tử chuẩn hóa. Một cấu trúc tam đoạn luận hay một quy tắc suy diễn điều kiện được tách rời khỏi bất kỳ đối tượng vật lý nào để tồn tại dưới dạng một sơ đồ suy diễn hình thức phổ quát. Tính đúng đắn của một lập luận không còn phụ thuộc vào việc các đối tượng đề cập có tồn tại trong thực tế hay không, mà chỉ phụ thuộc vào tính chuẩn xác của các mối quan hệ hình thức giữa các thành phần mệnh đề.

Một đóng góp mang tính nền tảng khác của trừu xuất hình thức nằm ở triết học toán học, đặc biệt là chương trình tân Frege (Neo-Fregeanism). Năm 2001, các triết gia toán học Hale và Wright đã công bố chuyên khảo The Reason's Proper Study do Nhà xuất bản Đại học Oxford phát hành, khảo sát sâu sắc các nguyên lý trừu xuất (abstraction principles). Theo trường phái này, một nguyên lý trừu xuất giới thiệu một thuật ngữ mới trỏ tới một đối tượng trừu tượng thông qua một quan hệ tương đương được xác lập trên các thực thể nền tảng sẵn có.

Nguyên lý trừu xuất tổng quát có thể được biểu diễn thông qua cấu trúc logic sau:

\forall x \, \forall y \, (\Sigma(x) = \Sigma(y) \leftrightarrow x \approx y)

Trong công thức trên, các đại lượng được định nghĩa rõ ràng như sau:

Ký hiệu $x$ và $y$ biểu diễn các biến đối tượng cơ sở thuộc một tập hợp hoặc một miền xác định cho trước.
Ký hiệu $\Sigma$ là hàm toán tử trừu xuất, thực hiện phép gán mỗi đối tượng cơ sở sang một đối tượng trừu tượng tương ứng.
Dấu đẳng thức $=$ biểu thị quan hệ đồng nhất logic giữa hai đối tượng trừu tượng vừa được tạo lập.
Ký hiệu toán tử $\approx$ là một quan hệ tương đương mang tính phản xạ, đối xứng và bắc cầu được định nghĩa trên miền đối tượng cơ sở.
Toán tử logic $\leftrightarrow$ thể hiện mối liên hệ tương đương hai chiều giữa sự đồng nhất của các thực thể trừu tượng và mối quan hệ tương đương giữa các đối tượng xuất phát điểm.

Tiêu biểu cho cơ chế trừu xuất hình thức này là Nguyên lý Hume, trong đó số lượng của một khái niệm được xác lập thông qua quan hệ tương đương song ánh giữa các tập hợp, đặt cơ sở logic vững chắc cho việc định nghĩa số tự nhiên mà không cần dựa dẫm vào trực giác thời gian hay không gian tiên nghiệm.

Phân định với hình thức hóa và ứng dụng trong cơ giới hóa toán học

Trong nghiên cứu khoa học đương đại, việc phân định ranh giới giữa trừu xuất hình thức (formal abstraction) và hình thức hóa (formalization) có ý nghĩa phương pháp luận đặc biệt quan trọng. Trừu xuất hình thức là thao tác nhận thức bóc tách, lược bỏ bớt các yếu tố cụ thể để giữ lại các thuộc tính cấu trúc bản chất. Trong khi đó, hình thức hóa là quá trình chuyển dịch toàn bộ các mệnh đề, định nghĩa và bước suy luận từ ngôn ngữ tự nhiên sang một hệ thống ký hiệu và hệ tiên đề nhân tạo chặt chẽ mà máy tính có thể phân tích.

Năm 2018, trên tạp chí Notices of the American Mathematical Society, tác giả Avigad đã đưa ra những phân tích sâu sắc về quá trình cơ giới hóa toán học, chỉ ra rằng việc hình thức hóa toán học cho phép biểu diễn các định nghĩa và chứng minh trong một khuôn khổ tiên đề khép kín để máy tính có thể xác thực tính đúng đắn. Trong toán học truyền thống, các bài báo khoa học thường chứa đựng các khoảng trống ngầm hiểu qua những diễn đạt như "dễ thấy rằng" hay "chứng minh tương tự". Những khoảng trống này được khắc phục triệt để khi toàn bộ lập luận được hình thức hóa chi tiết.

Đỉnh cao của nỗ lực chứng minh hình thức toàn phần được thể hiện qua công trình của Thomas Hales cùng 21 đồng tác giả vào năm 2017 trên tạp chí Forum of Mathematics, Pi. Dự án Flyspeck này đã hoàn thành bản chứng minh hình thức cho Giả thuyết Kepler bằng các hệ thống HOL Light và Isabelle, khép lại bài toán hình học xếp cầu tồn tại suốt bốn thế kỷ. Để hỗ trợ các quy trình hình thức hóa quy mô lớn, năm 2015 tại hội nghị CADE-25, de Moura và các cộng sự đã giới thiệu hệ thống chứng minh tương tác mã nguồn mở Lean. Hệ thống này dựa trên lý thuyết kiểu phụ thuộc, cung cấp môi trường lập trình và kiểm chứng tự động cho các cấu trúc toán học từ đại số đến giải tích.

Dự án Tóm tắt hình thức trong Toán học (Formal Abstracts - FAB)

Mặc dù việc hình thức hóa toàn phần (full formalization) chứng minh từng dòng lập luận mang lại độ tin cậy tuyệt đối, phương thức này đòi hỏi chi phí lao động trí tuệ khổng lồ và khó có thể áp dụng đại trà cho mọi công bố toán học. Để giải quyết nút thắt này, Thomas Hales đã khởi xướng sáng kiến xây dựng các bản tóm tắt hình thức (Formal Abstracts).

Cần nhấn mạnh sự khác biệt rõ rệt về mặt thuật ngữ: trong dự án này, từ "abstract" được sử dụng với tư cách danh từ chỉ "bản tóm tắt bài báo khoa học" được viết bằng ngôn ngữ hình thức máy đọc được, hoàn toàn khác với danh từ "abstraction" chỉ thao tác "trừu xuất hình thức" trong nhận thức luận. Tuy nhiên, dự án tóm tắt hình thức phản ánh sinh động tư tưởng trừu xuất: thay vì mã hóa toàn bộ chi tiết chứng minh vi mô, dự án thực hiện thao tác cô lập và trừu xuất các kết quả định lý, định nghĩa cốt lõi để xây dựng một thư viện toán học số hóa.

Tại Việt Nam, dự án FAB (Formal Abstract in Mathematics) đã ghi nhận sự tham gia của các nhà toán học trong nước. Năm 2021, nhóm tác giả gồm Hà Huy Khoái, Nguyễn Thị Huyền Châu, Nguyễn Thị Trà My, Mai Thúy Nga và Ngô Thị Thanh Nga đã công bố nghiên cứu trên Tạp chí Khoa học Thăng Long: Khoa học Ứng dụng về vai trò của toán học thời kỳ 4.0 và dự án FAB. Nghiên cứu xác nhận Trường Đại học Thăng Long đã tham gia triển khai dự án này với sự phối hợp của 2 trường đại học lớn tại Mỹ là University of Pittsburgh và Carnegie Mellon University.

Bản tóm tắt hình thức trong dự án FAB được định hình bởi các đặc trưng sau:

Tập trung vào phát biểu cốt lõi: Dự án lược bỏ toàn bộ các bước chứng minh chi tiết, chỉ mã hóa các định nghĩa, cấu trúc xây dựng, phát biểu định lý và giả thuyết chính của bài báo khoa học.
Khả năng đọc hiểu song hành: Bản tóm tắt hình thức được thiết kế để cả con người lẫn các hệ thống máy tính đều có thể phân tích cú pháp và hiểu rõ ngữ nghĩa logic.
Liên kết tiên đề chuẩn mực: Mọi thuật ngữ trong phát biểu đều được kết nối chặt chẽ với các định nghĩa chuẩn tắc trong thư viện toán học hình thức, tránh hiểu lầm do xung đột ký hiệu.
Triển khai giai đoạn đầu: Trong giai đoạn đầu năm 2021, hệ thống Lean được lựa chọn để tiến hành hình thức hóa các phát biểu trong danh sách 100 định lý phổ biến của toán học, làm cơ sở kết hợp với ngôn ngữ tự nhiên có kiểm soát (CNL) ở giai đoạn tiếp theo.

Dưới đây là bảng đối chiếu giữa việc chứng minh hình thức toàn phần và việc xây dựng bản tóm tắt hình thức trong dự án FAB:

Tiêu chí so sánh	Chứng minh hình thức toàn phần (Full Formal Proofs)	Bản tóm tắt hình thức (Formal Abstracts - FAB)
Nội dung mã hóa	Bao gồm định nghĩa, phát biểu định lý và mọi bước chứng minh chi tiết	Chỉ mã hóa định nghĩa, phát biểu định lý và giả thuyết; bỏ qua các bước chứng minh
Chi phí thời gian và nhân lực	Đòi hỏi công sức khổng lồ, thường kéo dài nhiều năm cho một bài toán lớn	Tối ưu hóa nguồn lực, có thể áp dụng nhanh chóng trên quy mô lớn các công bố khoa học
Mục tiêu ứng dụng chính	Xác minh tính đúng đắn tuyệt đối của định lý phức tạp hoặc gây tranh cãi	Xây dựng đồ thị ngữ nghĩa toán học số hóa, phục vụ tìm kiếm thông minh và huấn luyện trí tuệ nhân tạo
Hệ thống công cụ đại diện	Coq, Isabelle/HOL, HOL Light, hệ thống Lean truyền thống	Dự án Formal Abstracts trên nền tảng Lean kết hợp ngôn ngữ tự nhiên có kiểm soát CNL

Ưu thế nhận thức luận và vai trò đối với trí tuệ nhân tạo

Sự kết hợp giữa trừu xuất hình thức trong tư duy lý thuyết và các công cụ hình thức hóa số đem lại những giá trị học thuật then chốt:

Loại trừ sự mơ hồ của ngôn ngữ tự nhiên: Thao tác trừu xuất hình thức buộc nhà nghiên cứu phải xác định tường minh mọi tiền đề, kiểu dữ liệu và phạm vi của biến số, loại bỏ những cách diễn đạt đa nghĩa và nâng cao độ tin cậy của các tuyên bố khoa học.
Xây dựng kho ngữ nghĩa chính xác cho trí tuệ nhân tạo: Các mô hình học máy hiện đại gặp khó khăn lớn khi tiếp cận tri thức toán học phi cấu trúc dưới dạng văn bản tài liệu PDF. Một mạng lưới tri thức được trừu xuất và hình thức hóa chuẩn xác cung cấp nguồn dữ liệu chất lượng cao, giúp các thuật toán trí tuệ nhân tạo có thể suy luận logic, phát hiện mối liên hệ liên ngành và hỗ trợ đề xuất các giả thuyết mới.
Tiêu chuẩn hóa tri thức liên ngành: Khi các lý thuyết thuộc nhiều lĩnh vực khác nhau được trừu xuất về các cấu trúc hình thức chung, rào cản thuật ngữ riêng biệt được dỡ bỏ, tạo điều kiện thuận lợi cho việc tích hợp tri thức giữa toán học thuần túy, vật lý lý thuyết và khoa học máy tính.

Ranh giới, hạn chế và thách thức học thuật

Bên cạnh những ưu thế vượt bậc, phương pháp trừu xuất hình thức cũng đối diện với những giới hạn nội tại và thách thức nhận thức sâu sắc mà giới học thuật cần nhận diện rõ ràng:

Khoảng cách nhận thức giữa trực giác và mã hình thức: Toán học không đơn thuần là sự thao tác trên các chuỗi ký hiệu vô cảm; tư duy toán học của con người phụ thuộc sâu sắc vào trực giác hình học, sự tương tự hóa và vẻ đẹp thẩm mỹ của các cấu trúc. Việc trừu xuất triệt để mọi nội dung sang dạng thức hình thức có nguy cơ làm xơ cứng tư duy sáng tạo, biến toán học thành trò chơi thao tác cú pháp cơ học và đánh mất đi cái nhìn toàn cảnh trực quan.
Vấn đề nghịch lý nền tảng: Lịch sử logic học cho thấy việc trừu xuất hình thức nếu không được kiểm soát chặt chẽ bởi các ràng buộc kiểu loại có thể dẫn tới những nghịch lý logic tai hại, tiêu biểu như Nghịch lý Russell phá vỡ hệ thống trừu xuất ngây thơ ban đầu của Frege. Do đó, việc xây dựng các hệ thống trừu xuất luôn đòi hỏi sự cân bằng tinh tế giữa năng lực biểu đạt phong phú và tính nhất quán logic.
Chi phí đào tạo và rào cản kỹ thuật: Để tham gia vào việc viết và thẩm định các bản trừu xuất hình thức, nhà nghiên cứu đòi hỏi phải thành thạo cả kiến thức chuyên ngành chuyên sâu lẫn kỹ năng lập trình trong các hệ thống chứng minh phức tạp như Lean hay Coq. Đây là một rào cản đào tạo không nhỏ đối với đại đa số cộng đồng nghiên cứu truyền thống.
Giới hạn bất toàn của hệ hình thức: Theo các định lý bất toàn của Gödel, trong bất kỳ hệ thống hình thức đủ mạnh nào chứa số học, luôn tồn tại những chân lý toán học không thể chứng minh cũng như không thể bác bỏ trong phạm vi nội bộ của hệ thống đó. Trừu xuất hình thức do đó không thể đóng vai trò như một giải pháp vạn năng để thâu tóm toàn bộ chân lý toán học khách quan.

Hướng phát triển và những vấn đề còn mở

Các chương trình nghiên cứu về trừu xuất hình thức đang tiếp tục mở rộng đường biên tri thức với những hướng đi đầy triển vọng:

Tự động hóa quá trình trừu xuất (Autoformalization): Khai thác các mô hình ngôn ngữ lớn tiên tiến kết hợp với các bộ kiểm tra kiểu logic để tự động chuyển dịch văn bản toán học viết bằng ngôn ngữ tự nhiên sang mã nguồn hình thức hóa, giảm bớt sự can thiệp thủ công của con người.
Tích hợp ngôn ngữ tự nhiên có kiểm soát (CNL): Phát triển các ngữ pháp hình thức bán tự nhiên giúp nhà nghiên cứu có thể viết bài báo khoa học bằng cú pháp gần gũi với tiếng Anh học thuật hàng ngày nhưng trình biên dịch vẫn có thể chuyển đổi trực tiếp thành các bản trừu xuất hình thức chuẩn xác.
Mở rộng phạm vi sang các khoa học thực nghiệm: Vận dụng phương pháp luận trừu xuất hình thức để tiên đề hóa các lý thuyết vật lý lượng tử, mô hình hóa cấu trúc gene trong sinh học tính toán và thiết lập các chuẩn mực kiểm chứng an toàn cho các hệ thống phần mềm tự hành.