Читать «Искусственный разум» онлайн - страница 63

Итак, "мартышкин труд" предпочтительней эвристик. ЛЮБОЗАР с его колебаниями и отсутствием гарантий успешного решения должен уступить дорогу властной резолюции. Машинная логика сама, без человека одолеет любые препятствия.

Против этой достаточно распространенной постановки вопроса возражает академик В. Глушков: "Такая постановка не соответствует опыту, накопленному в других областях применения ЭВМ".

И предлагает совсем иной подход к машинному доказательству теорем. Центральной фигурой в нем является человек, квалифицированный математик, активно взаимодействующий с машиной. Чтобы взаимодействие было возможным, необходим язык, удобный для математика и понятный для ЭВМ. Чтобы взаимодействие было плодотворным, машину следует вооружить Алгоритмом Очевидности. Язык и Алгоритм - два краеугольных камня, на которых должно быть воздвигнуто новое здание "математического обеспечения для математических доказательств".

В. Глушков изложил свои новаторские идеи в начале 1965 года. Сейчас, в августе 1977 года, мы беседуем о развитии этих идей с ближайшим сотрудником В. Глушкова, профессором Ю. Капитоновой. Задаю ей естественный вопрос:

- Почему не доверить машине самой вести доказательство?

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

- Значит, я попрошу ЭВМ доказать теорему, а мой внук заберет готовое доказательство?

- На блюдечке с голубой каемочкой. Если, конечно, машина, ведущая перебор, не окажется в металлоломе, а само доказательство будет хоть кому-нибудь нужно.

- Все-таки память о дедушке... Как же хотите вы ускорить работу машины?

- Научив ее математике. Для этого и нужен особый язык, язык практической математики.

- Язык практической математики - зачем его придумывать вновь? Разве математика издавна не обладает своим строгим, точным и однозначным языком?

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

- Итак, язык практической математики делает аксиомы, теоремы, следствия - весь арсенал математики доступным машине. Но кто беседует с ЭВМ на этом языке, кто учит ее математике?

- Каждый, кому не лень. Я говорю серьезно: передача машине математических знаний - дело коллективное. Все математики должны хотеть, чтобы ЭВМ знала и фундаментальные вещи, и новейшие, только что опубликованные факты. Все математики будут стремиться к полноте и детальности машинных знаний.