Нейросеть+логический движок для математических доказательств

[Anton_Peplov]

Ende
Выделено из темы «О возможности создания сверхчеловеческого ИИ»

Oleksandr Rybakov
Я согласен, что проблема логических ошибок, допускаемых генеративными языковыми нейросетями, будет решена в том или ином виде. Но не уверен, что за счёт логических движков. Чтобы прикрутить движок, нужен перевод с естественного языка, на котором обучалась нейросеть, на язык логического движка. То есть нейросеть нужно научить формализовать рассуждения для движка. Проще ли это, чем научить её рассуждать без движка?

[Oleksandr Rybakov]

Anton_Peplov
Скорость вычислений хреновая у ИИ. Логика и так экспоненциальна, а тут ее надо через триллион параметров прогнать. ИИ переводит с человеческого на С++. А в чем проблема с человеческого на язык логического движка?

[Sender]

Oleksandr Rybakov в сообщении #1687718 писал(а):

А в чем проблема с человеческого на язык логического движка?

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

Цитата:

Despite impressive progress, neural models commonly display generalization and robustness failures on reasoning tasks.

, даже с арифметикой трудности.

[Anton_Peplov]

Oleksandr Rybakov в сообщении #1687718 писал(а):

Скорость вычислений хреновая у ИИ. Логика и так экспоненциальна, а тут ее надо через триллион параметров прогнать.

Я бы легко с Вами согласился, если бы работоспособное решение выглядело как "нейросеть загрузила условие в логический движок $\to$ движок выполнил все логические операции $\to$ нейросеть перевела готовые выкладки движка на естественный язык". Но мне кажется, это так не работает. Движок же сам по себе не знает, куда идти, чтобы доказать утверждение. Он проверяет выкладки, а не генерирует их. Так что нейросети придется сгенерировать рассуждение, перевести его с человеческого на движковый, проверить его движком, убедиться в ошибке, сгенерировать новое рассуждение... Выигрыш в скорости становится неочевидным.

Чтобы не толочь воду в ступе, предлагаю рассмотреть пример. Поручим нейросети с логическим движком доказать правило Евклида. Пусть $a, b \in \mathbb N, a \ge b$. Тогда

$$ \text{НОД}(a, b) = \text{НОД}(a \bmod b, b) $$

(Доказательство)

Т.к. все элементы класса вычетов по модулю $b$ получаются последовательным вычитанием $b$, достаточно доказать, что $\text{НОД}(a, b) = \text{НОД}(a - b, b)$. Общий делитель чисел $a, b$ делит их разность $a - b$, так что $\text{НОД}(a, b) \le \text{НОД}(a - b, b)$. С другой стороны, общий делитель чисел $a - b, b$ делит их сумму $a - b + b = a$, так что $\text{НОД}(a, b) \ge \text{НОД}(a - b, b)$.

Я взял очень известную теорему (скорее даже элементарный факт), и нейросеть, скорее всего, просто воспроизведет готовое доказательство из интернета. Но предположим, что правило Евклида еще не известно человечеству, нас ведь в контексте разговора интересует доказательство новых теорем. Можете на этом примере показать, как нейросеть будет взаимодействовать с движком и в каком месте движок даст выигрыш в скорости?

Oleksandr Rybakov в сообщении #1687718 писал(а):

ИИ переводит с человеческого на С++.

С багами.

Oleksandr Rybakov в сообщении #1687718 писал(а):

А в чем проблема с человеческого на язык логического движка?

В том, что первый же баг обрушит все рассуждение. "Позвольте мне принять, что 2+2=5, и я докажу, что вы папа Римский".

[Oleksandr Rybakov]

Есть же системы автоматического доказательства теорем. Нейросеть формализовала посылки, движок их лопатит, строит выводы из них.

[Sender]

Oleksandr Rybakov в сообщении #1687699 писал(а):

Проигрыш по п. 4 закончится когда к ИИ прикрутят быстрый НЕ НЕЙРОСЕТЕВОЙ логический движок. Их навалом.

Можно пример одного?

[Anton_Peplov]

Oleksandr Rybakov в сообщении #1687751 писал(а):

Есть же системы автоматического доказательства теорем.

Здесь нужно различать четыре вида систем:
1. Системы автоматического доказательства. Дали формализованное утверждение, движок ищет доказательство. В этом случае возможности нейросети что-то доказывать будут ограничены эвристиками прикрученной системы доказательства. Успех таких систем пока очень ограничен, именно потому, что нет эффективных алгоритмов поиска доказательства. Из нетривиальных результатов, полученных такими системами, я знаю только доказательство гипотезы Робинсона об аксиоматике булевой алгебры (я, конечно, не специалист).
2. Пруфчекеры. Человек переводит доказательство с человеческого на движковый, движок проверяет. Это ситуация, которую я описывал в сообщении выше, про правило Евклида. Есть опасность неправильного перевода. Также есть вопросы, даст ли движок выигрыш в скорости по сравнению с рассуждениями нейросети без движка.
3. Системы символьных вычислений, в т.ч. компьютерной алгебры. Хорошая штука, но узкоспециальная. Интеграл возьмет, а концептуальную теорему не докажет.
4. Computer-assisted proof. Человек доказывает: любой возможный случай, подпадающий под утверждение теоремы, сводится к какому-нибудь из 100500 частных. Так что если утверждение теоремы верно в этих случаях, то оно верно всегда. После этого эти 100500 частных случаев перебираются компьютером, он проверяет, что утверждение теоремы в этих случаях верно, и доказательство считается завершенным. В контексте разговора этот случай не интересен.

Вариант использования движков, который вижу я - это обучить нейросеть (а не движок), получив на вход формализованное (человеком или самой сетью, или другой сетью) утверждение, строить его формальное доказательство. А движок пусть проверяет это доказательство, как пруфчекер (случай 2). Однако нужна обучающая выборка из овердофига формальных доказательств. У нас столько нету.

[dgwuqtj]

Anton_Peplov в сообщении #1687757 писал(а):

Человек переводит доказательство с человеческого на движковый, движок проверяет. Это ситуация, которую я описывал в сообщении выше, про правило Евклида. Есть опасность неправильного перевода.

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

[Anton_Peplov]

dgwuqtj в сообщении #1687759 писал(а):

Для начала достаточно, чтобы нейросеть делала перевод только доказательства, а формулировки переводились вручную.

Не очень понимаю разделение на перевод доказательства и перевод формулировок. Можно игрушечный пример?

[dgwuqtj]

Просто смысл в том, что не надо будет бояться ошибок нейросети, всё проверит пруфчекер. С тем же правилом Евклида хорошо бы, чтобы нейросеть переводила ваше человеческое доказательство, имея формулировку на русском и уже готовый перевод $\forall a, b \in \mathbb N \enskip (a \geq b \Rightarrow \gcd(a, b) = \gcd(a \bmod b, b))$. А если дать нейросети переводить всё, то перевод формулировки всё равно придётся проверять и иногда корректировать.

[mihaild]

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

Плюс можно разрешить модели по ходу дела задавать вопросы - "я не понимаю этого перехода, распиши подробнее". В общем эта задача выглядит гораздо проще, чем построение доказательства, хоть формализованного, хоть нет, с нуля.

[Anton_Peplov]

mihaild
Я уже и сам сообразил. Вы отвечали на удаленное сообщение. Тем не менее спасибо за ответ, он полезен.

mihaild в сообщении #1687763 писал(а):

Тут надо смотреть, но я ожидаю, что можно обойтись без очень уж большой базы формальных доказательств.

Вашими бы устами да мед пить. А можно привести аргументы в пользу такого ожидания?

Я так понимаю, всякие GPT и Gemini хороши в том числе потому, что их обучали на дофигабайтах текста. Не достаточное условие, но необходимое.

[Sender]

Если на то пошло, небольшие формальные доказательства можно и автоматически синтезировать.

[Anton_Peplov]

Sender в сообщении #1687767 писал(а):

Если на то пошло, небольшие формальные доказательства можно и автоматически синтезировать.

Очень небольшие, ибо комбинаторный взрыв. Боюсь, нейросеть, видевшая только очень короткие доказательства, и формализовывать научиться лишь такие же короткие.

[mihaild]

Anton_Peplov в сообщении #1687766 писал(а):

А можно привести аргументы в пользу такого ожидания?

Модели уже довольно хороши в обобщении, и, например, способны использовать библиотеки, прочитав документацию (и не обучаясь на примерах использования).
Вот, например, что gemini выдает на просьбу записать и доказать правило Евклида на coq.

(Оффтоп)

Require Import Coq.ZArith.ZArith.
Require Import Coq.ZArith.Znumtheory. (* For Z.gcd_nonneg, Z.gcd_greatest, Z.divide_antisym_abs, Z.divide_add, Z.divide_sub, Z.divide_mul_r_s (Zdivide_factor_r) *)
Require Import Lia. (* For the lia tactic, useful for arithmetic goals *)

Open Scope Z_scope.

Theorem gcd_mod_b_left_proof (a b : Z) : Z.gcd a b = Z.gcd (a mod b) b.
Proof.
  (* Handle the case b = 0 separately *)
  destruct (Z.eq_dec b 0) as [Hb0 | Hbn0].
  { (* Case: b = 0 *)
    rewrite Hb0.
    rewrite Z.modulo_0_l. (* a mod 0 = a *)
    reflexivity. (* Z.gcd a 0 = Z.gcd a 0 *)
  }
  { (* Case: b <> 0 *)
    (* We use the property that for x, y such that Z.abs x = x and Z.abs y = y (i.e., x,y >=0), *)
    (* x = y <-> (Z.divide x y /\ Z.divide y x). *)
    (* Z.gcd results are non-negative by Z.gcd_nonneg. *)
    apply Z.divide_antisym_abs.
    { (* Z.gcd a b >= 0 *)
      apply Z.gcd_nonneg.
    }
    { (* Z.gcd (a mod b) b >= 0 *)
      apply Z.gcd_nonneg.
    }
    split.
    { (* Goal 1: Z.divide (Z.gcd a b) (Z.gcd (a mod b) b) *)
      (* Let g1 = Z.gcd a b. We need to show g1 divides Z.gcd (a mod b) b. *)
      (* By Z.gcd_greatest, it's enough to show g1 divides (a mod b) and g1 divides b. *)
      apply Z.gcd_greatest.
      { (* Show: Z.gcd a b divides (a mod b) *)
        (* We use the property a mod b = a - b * (a / b), which holds for b <> 0. *)
        (* This is Z.div_mod_relation_2: forall z1 z2, z2 <> 0 -> z1 - z2 * (z1 / z2) = z1 mod z2. *)
        assert (H_mod_eq: a mod b = a - b * (a / b)).
        { symmetry. apply Z.div_mod_relation_2. exact Hbn0. }
        rewrite H_mod_eq.
        (* Z.gcd a b divides a (by Z.gcd_divide_l). *)
        (* Z.gcd a b divides b (by Z.gcd_divide_r). *)
        (* So, Z.gcd a b divides b * (a/b) (by Zdivide_factor_r or Z.divide_mul_r_s). *)
        (* So, Z.gcd a b divides a - b * (a/b) (by Z.divide_sub). *)
        apply Z.divide_sub.
        { apply Z.gcd_divide_l. } (* Z.gcd a b | a *)
        { apply Zdivide_factor_r with (p := (a/b)). apply Z.gcd_divide_r. } (* Z.gcd a b | b implies Z.gcd a b | b * (a/b) *)
      }
      { (* Show: Z.gcd a b divides b *)
        apply Z.gcd_divide_r.
      }
    }
    { (* Goal 2: Z.divide (Z.gcd (a mod b) b) (Z.gcd a b) *)
      (* Let g2 = Z.gcd (a mod b) b. We need to show g2 divides Z.gcd a b. *)
      (* By Z.gcd_greatest, it's enough to show g2 divides a and g2 divides b. *)
      apply Z.gcd_greatest.
      { (* Show: Z.gcd (a mod b) b divides a *)
        (* We know a = b * (a/b) + (a mod b) from Z.div_mod_eq, for b <> 0. *)
        rewrite (Z.div_mod_eq a b Hbn0). (* a = b * (a / b) + a mod b *)
        (* Z.gcd (a mod b) b divides (a mod b) (by Z.gcd_divide_l). *)
        (* Z.gcd (a mod b) b divides b (by Z.gcd_divide_r). *)
        (* So, Z.gcd (a mod b) b divides b * (a/b) (by Zdivide_factor_r). *)
        (* So, Z.gcd (a mod b) b divides b * (a/b) + (a mod b) (by Z.divide_add). *)
        apply Z.divide_add.
        { apply Zdivide_factor_r with (p := (a/b)). apply Z.gcd_divide_r. } (* Z.gcd (a mod b) b | b implies Z.gcd (a mod b) b | b * (a/b) *)
        { apply Z.gcd_divide_l. } (* Z.gcd (a mod b) b | a mod b *)
      }
      { (* Show: Z.gcd (a mod b) b divides b *)
        apply Z.gcd_divide_r.
      }
    }
  }
Qed.

(* You can test the theorem: *)
(* Example: gcd(10, 6) = gcd(10 mod 6, 6) = gcd(4, 6) = 2 *)
Compute Z.gcd 10 6. (* Expected: 2 *)
Compute Z.gcd (10 mod 6) 6. (* Expected: Z.gcd 4 6 = 2 *)

Eval cbv in (gcd_mod_b_left_proof 10 6). (* Should yield eq_refl after computation *)
Eval cbv in (gcd_mod_b_left_proof 10 0). (* Should yield eq_refl *)

Вопрос к людям, знающим о coq что-то, кроме названия (т.е. больше, чем я) - тут что-то осмысленное написано или нет?