Теоремы Гёделя и границы вычислимости для сильного ИИ

Материал из MachineLearning.

1. Теоремы Гёделя и границы вычислимости для сильного ИИ

• • Теоремы Гёделя о неполноте** — две фундаментальные теоремы математической логики, доказанные Куртом Гёделем в 1931 году. Эти теоремы установили принципиальные границы доказуемости в формальных аксиоматических системах и оказали глубокое влияние на философию математики, теорию вычислимости и дискуссии о природе искусственного интеллекта. В контексте сильного ИИ (AGI) теоремы Гёделя часто интерпретируются как указание на фундаментальные вычислительные ограничения, которые невозможно преодолеть путём увеличения вычислительной мощности или объёма данных.

1. 1. Исторический контекст

В начале XX века Давид Гильберт поставил амбициозную задачу — найти полную и непротиворечивую систему аксиом, охватывающую всю математику (программа Гильберта). Считалось, что такая формализация позволит механически разрешать любые математические утверждения. Гёдель показал, что эта программа принципиально невыполнима. Его результаты стали частью серии открытий о границах формальных систем, включая теорему Тарского о неопределимости (1933), доказательство Алонзо Чёрчем неразрешимости проблемы разрешимости (1936) и теорему Тьюринга о неразрешимости проблемы остановки (1936).

1. 1. Теоремы Гёделя о неполноте

1. 1. 1. Формальные системы

Теоремы Гёделя применимы к формальным системам, которые обладают тремя свойствами:

1. Достаточная выразительная сила — система способна выражать арифметику натуральных чисел;
2. Непротиворечивость — в системе не выводимы одновременно утверждение и его отрицание;
3. Эффективная аксиоматизируемость — существует алгоритм, позволяющий механически определить, является ли данное утверждение аксиомой.

Формальная система называется полной, если для любого утверждения языка системы либо само утверждение, либо его отрицание может быть выведено (доказано) в системе.

1. 1. 1. Первая теорема о неполноте

Первая теорема Гёделя о неполноте утверждает, что в любой непротиворечивой формальной системе, достаточно богатой для выражения арифметики натуральных чисел, существуют утверждения, которые не могут быть ни доказаны, ни опровергнуты в рамках этой системы. Иными словами, любая такая система неполна.

Ключевым конструктивным элементом доказательства является гёделево предложение — утверждение, которое в метаматематической интерпретации гласит: «Я недоказуемо в данной системе». Рассуждение строится следующим образом:

• Если предположить, что это утверждение доказуемо, то оно истинно (поскольку утверждает свою недоказуемость), но тогда система содержит недоказуемое истинное утверждение — противоречие.
• Если же предположить, что оно недоказуемо, то оно истинно, и именно это оно и утверждает.

Таким образом, при условии непротиворечивости системы, гёделево предложение оказывается истинным, но недоказуемым.

1. 1. 1. Вторая теорема о неполноте

Вторая теорема Гёделя о неполноте является усилением первой. Она утверждает, что никакая непротиворечивая формальная система, достаточно богатая для арифметики, не может доказать собственную непротиворечивость. Это означает, что система не может из своих собственных аксиом установить, что в ней не возникает противоречий.

1. 1. Теоремы Гёделя и вычислимость

Теоремы Гёделя тесно связаны с теорией вычислимости через понятие вычислимой функции и машины Тьюринга. Поскольку любая рекурсивно перечислимая формальная система может быть реализована как алгоритм (и, следовательно, как программа на машине Тьюринга), теоремы Гёделя накладывают ограничения на то, что может быть вычислено или доказано с помощью алгоритмических средств.

В частности, из теорем Гёделя следует неразрешимость проблемы определения истинности для любого утверждения в достаточно богатой формальной системе. Это ограничение распространяется на все алгоритмические системы, включая системы машинного обучения и искусственного интеллекта, поскольку их работа основана на вычислимых процедурах.

1. 1. Значение для сильного ИИ

В дискуссиях о возможности создания сильного искусственного интеллекта (AGI) теоремы Гёделя часто используются для аргументации принципиальной невыводимости некоторых аспектов человеческого мышления из вычислительных процедур. Наиболее известной является аргумент Лукаса — Пенроуза, согласно которому человек способен «увидеть» истинность гёделева предложения для любой формальной системы, тогда как сама система этого сделать не может. Отсюда делается вывод, что человеческий разум не является машиной Тьюринга.

Однако этот аргумент не является общепринятым. Критики указывают на следующие слабые места:

• Аргумент предполагает непротиворечивость человеческого разума, что не является доказанным фактом;
• Он требует, чтобы человек охватывал всю формальную систему целиком, что является идеализацией;
• Не существует формального критерия, позволяющего гарантировать, что человек действительно распознаёт непротиворечивость произвольной системы.

Тем не менее, теоремы Гёделя остаются важным напоминанием о том, что любой алгоритмический агент сталкивается с фундаментальными границами, которые не могут быть преодолены простым наращиванием вычислительных мощностей или объёмов данных.

1. 1. См. также

• Курт Гёдель
• Теория вычислимости
• Машина Тьюринга
• Проблема остановки
• Сильный ИИ
• Философия искусственного интеллекта
• Теорема Чёрча — Тьюринга

1. 1. Примечания

1. 1. Литература

• Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38, 173–198.
• Raatikainen, P. (2013). [Gödel's Incompleteness Theorems](https://plato.stanford.edu/entries/goedel-incompleteness/). In The Stanford Encyclopedia of Philosophy (Fall 2020 Edition).
• [Gödel's incompleteness theorems](https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems). Wikipedia.
• [Penrose–Lucas argument](https://en.wikipedia.org/wiki/Penrose–Lucas_argument). Wikipedia.
• [Lucas-Penrose Argument about Gödel's Theorem](https://iep.utm.edu/lp-argue/). Internet Encyclopedia of Philosophy.
• Turing, A. M. (1936). On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 42(1), 230–265.
• [Artificial Intelligence](https://plato.stanford.edu/archives/sum2020/entries/artificial-intelligence/). Stanford Encyclopedia of Philosophy.