Cтраница 1
Геометрическая машина фактически представляет собой частную реализацию электронной машины для обработки информации IBM-704; программа эта довольно длинная и сложная. Запрограммированная так машина состоит из трех частей: синтаксической машины ( СМ) и машины-чертежника ( МЧ), которые связаны с эвристической машиной ( ЭМ), являющейся исполнительной ( управляющей) программой. Эти связи показаны на фиг. [1]
Геометрическая машина может доказать многие теоремы в пределах заданной ей формальной системы, используя чертеж лишь для того, чтобы указать, какие подцели, вероятно, справедливы. [2]
Геометрическая машина способна находить доказательства большого числа теорем в пределах выбранной для данного случая формальной системы ( включая теоремы о параллельных линиях, о подобии и о равенстве и неравенстве отрезков и углов), не применяя какого-либо решающего алгоритма и не используя полного перебора всех возможных последовательностей, могущих привести к доказательству. Вместо этого машина опирается на эвристические методы, позволяющие предотвращать вырабатывание таких последовательностей, которые имеют низкую априорную вероятность привести к доказательству рассматриваемой теоремы. [3]
Подобно математику, геометрическая машина использует богатые эвристические свойства чертежа для лучшего различения истинных и ложных последовательностей. Хотя чертеж используется машиной и для других целей, уже одна эвристика отбрось как ложные любые утверждения, не удовлетворяющие чертежу позволяет машине доказать большой класс интересных теорем, часть которых содержит некоторые тривиальные построения. [4]
Именно в этом кроются дополнительные возможности геометрической машины в поиске доказательства теорем, необходимые для такой сложной формальной системы. Они не были нужны, а потому и не искались в машине Логик-теоретик Ньюэлла, Шоу и Саймона ( см. Пойа [870]), предназначенной для исчисления высказываний. [5]
Перед тем как перейти к детальному рассмотрению структуры геометрической машины, мы сделаем замечание о двух основных ( почти очевидных) принципах, которыми необходимо руководствоваться при выборе эвристик для любой машины, решающей задачи. [6]
Как и Логик-теоретик Ньюэлла, Шоу и Саймона, геометрическая машина для достижения этой цели опирается на хорошо известный аналитический метод. Метод обратного просмотра гарантирует машине, что каждая рассматриваемая ею последовательность действительно оканчивается на требуемом утверждении. Однако само по себе это без использования дополнительных эвристик не представляет значительного улучшения по сравнению с полным перебором, ибо преимущества метода обратного просмотра покупаются дорогой ценой, так как нет никакой гарантии, что каждая вырабатываемая последовательность, оканчивающаяся нужным образом, вообще служит доказательством чего-либо. Действительно, большинство цепочек, полученных таким способом, будут ложными. Но именно в этом и состоит сила аналитического метода, так как, если бы оказалось возможным найти способ обнаружения ложных последовательностей, такие последовательности можно было бы немедленно отбрасывать, что позволило бы отсекать от богато разветвленного дерева решений сухие ветви. Набор последовательностей, вырабатываемых таким процессом, содержал бы на любой глубине поиска на несколько порядков меньше членов, и плотность возможных доказательств теоремы среди этих последовательностей была бы соответственно выше. [7]
Очевиден следующий подход к проблеме внесения элемента обучения в геометрическую машину: машине дают возможность так регулировать все параметры, определяющие ее конкретные семантические эвристики, чтобы максимизировать предсказанную пригодность тех подцелей, которые оказываются полезными на практике. Таким путем машина будет улучшать согласование своих эвристических фильтров с классом задач, считающихся достаточно интересными, чтобы задаваться машине. [8]
Логик-теоретик и машина для игры в шахматы Ньюэлла, Шоу и Саймона [789, 792] и геометрическая машина Гелерн-тера и Рочестера [363] являются примерами работающих эвристических программ в других областях. [9]
Рассмотрим, наконец, значение нашей работы для основной проблемы - создания разумной машины. Нам кажется, что геометрическая машина служит убедительным доводом в пользу силы и плодотворности метода эвристического программирования для решения машиной определенного класса задач. В нашей экспериментальной работе с машиной введение одной-единствен-ной эвристики часто было эквивалентно увеличению скорости машины или емкости ее памяти в 3 - 5 раз. [10]
Наша программа оказалась не пригодной для исследования простейших видов обучения, основанных на методе проб и ошибок, в основном из-за низкой скорости, с которой она приобретает опыт. Однако разумно ожидать, что геометрическая машина может еще оказаться полезной при исследовании более совершенных видов обучения, основанных на понимании смысла понятий, если только когда-нибудь станет известно, как сформулировать эту задачу. [11]
Личный опыт немедленно подсказывает нам примеры структур памяти, обладающие этими свойствами. Гелернтер [365], например, создал геометрическую машину, основной источник разумности которой заключается в способности отбрасывать большинство из формально возможных последовательностей шагов доказательства, основываясь на том критерии, что они видимо не являются правильными. В результате машина, основываясь на посылках подлежащей доказательству теоремы, создает свой чертеж. На самом деле, машина снабжена таким чертежом, причем проблема создания этого чертежа, хотя и оказывается сложной, не обременяет память и не снижает скорость вычисления. Следствия из посылок в явном виде содержатся в этом чертеже наряду с некоторыми отношениями, не являющимися следствиями, однако большинство их отбрасывается. Машина затем просто отвергает из возможных подцелей ( промежуточных шагов) все, что не соответствует чертежу. Например, посылки треугольник ABC, АВ - ВС, A, D, С колли-неарны и AD DC даются вместе с координатами каждой точки, например Л ( 0, 0), В ( 5, 5), С ( 10, 0) и D ( 5, 0) ( фиг. Машина никогда не попытается доказать, что треугольник ABC совпадает с треугольником ABD, потому что это не справедливо для данного чертежа. Машина может определить это, вычислив относительные периметры этих треугольников. [12]
Кроме всего прочего, наша работа дает качественную оценку порядка трудности задач, которые, по-видимому, можно решать при современном состоянии вычислительной техники. Три года назад преобладало мнение, что геометрическая машина не будет создана к настоящему времени. Сейчас же специалист вряд ли будет оспаривать, что через три года машина будет доказывать интересные теоремы из области теории чисел. [13]
Большинство же можно вывести ( правда, обычно с некоторыми трудностями) из уже известных ему аксиом. Вместе с тем такая ситуация позволяет значительно упростить доказательство, оставляя его в то же время осмысленным. Геометрическая машина в явном виде записывает все предположения, используемые ею в данном доказательстве. Она может, если потребуется, свести к минимуму опасность того, что доказывается лишь частный случай данной теоремы, строя добавочные чертежи для проверки общности ее предположений. [14]
В современной модификации системы проблема углов решается следующим образом. Машине дают возможность использовать чертеж для отождествления данного угла с полной системой его обозначений, и она точно так же, как это делает человек, может заключать, что различные обозначения одного и того же угла имеют один и тот же смысл. В современном варианте геометрическая машина может доказывать теоремы, которые по уровню сложности соответствуют приводимой ниже. [15]