Здравствуйте, Gaperton, Вы писали:
G>Вы не об этом. Это не может быть причиной. Известен набор пар точка-значение. Использовать можно ЛЮБОЙ метод, при этом хотите вы этого или нет, интерполяционная функция будет принадлежать какому-то наперед известному классу параметрических функций. Будь то сплайны, отрезки ряда фурье, полиномы, или (в случае НС) многослойный персептрон. Все перечисленные функции кроме персептрона имеют очевидные свойства и предсказуемое поведение, при равной персептрону описательной силе, которая в большей степени определяется количеством настраиваемых параметров, а не видом функции. Вид функции влияет на скорость сходимости (точность приближения), и здесь персептрон тоже в аутсайдерах.
Если понимать под нейронными сетями ТОЛЬКО функции вида пороговая функция от суммы произведения значений в точках на вес. То это верно. Но разве я что то говорил про ПЕРСЕПТРОН? А если идею обучения некоторой функции по входным значениям? Тогда Ваши же аргументы работают против Вас. Посокольку все те чудные свойства функций ЛЮБОГО заданного класса — остаются. Как и прогнозированное поведение. И добавляется лишь ещё одни и довольно эффективный метод работы с ними. Что по определению расширяет возможности. Из известных мне работ уже давным давно никто персептроном не пользуется. Используются именно идеи и подходы, которые были применены в древности к персептрону. Но не он сам.
AF>>Это если бы задачей было построить компилятор на одних нейронных сетях. Тут и спорить не о чем. Задача то была — найти возможность применения НС в поиске ошибок. И не там, где они заведомо не будут работать. А именно конекст — в котором они работать будут и способ их применения. AF>> Хотя для данной области НС — далеко не лучший выбор, что однако и так очевидно...
G>Экстраполяционные методы здесь не то что "лучший" или "худший" — это вообще не выбор, если вы еще не поняли. Задача принцпиально не разрешима в данной постановке, и этот факт доказан. При наличии формальных спецификаций можно попробовать проверить программу на соответствие этим спецификациям, но это совсем другая песня, и другая математика.
Не выбор для чего? Для того, что бы в случае ошибки (например "неверно задан идентификатор") по написанию идентификатора определить его подобие с другими, и выдвинуть предположение, что это описка в таком-то имени? Для того, что бы оценить подобие имён? Для этого вполне подходят. Если для того, что бы парсировать текст на C++ — то очвидно нет. Даже теоретически.
Здравствуйте, AndreyFedotov, Вы писали:
AF>Здравствуйте, Gaperton, Вы писали:
G>>Вы не об этом. Это не может быть причиной. Известен набор пар точка-значение. Использовать можно ЛЮБОЙ метод, при этом хотите вы этого или нет, интерполяционная функция будет принадлежать какому-то наперед известному классу параметрических функций. Будь то сплайны, отрезки ряда фурье, полиномы, или (в случае НС) многослойный персептрон. Все перечисленные функции кроме персептрона имеют очевидные свойства и предсказуемое поведение, при равной персептрону описательной силе, которая в большей степени определяется количеством настраиваемых параметров, а не видом функции. Вид функции влияет на скорость сходимости (точность приближения), и здесь персептрон тоже в аутсайдерах. AF>Если понимать под нейронными сетями ТОЛЬКО функции вида пороговая функция от суммы произведения значений в точках на вес. То это верно. Но разве я что то говорил про ПЕРСЕПТРОН? А если идею обучения некоторой функции по входным значениям? Тогда Ваши же аргументы работают против Вас. Посокольку все те чудные свойства функций ЛЮБОГО заданного класса — остаются. Как и прогнозированное поведение. И добавляется лишь ещё одни и довольно эффективный метод работы с ними. Что по определению расширяет возможности. Из известных мне работ уже давным давно никто персептроном не пользуется. Используются именно идеи и подходы, которые были применены в древности к персептрону. Но не он сам.
Ох, не хотел в дисскуссию ввязываться, но здесь не могу удержаться. Хватаем за язык.
Объясните четко и недвусмысленно про "довольно эффективный метод", который "еще один" и "добавляется". На примере:
1) Рядов фурье.
2) Многочленов. (метод наименьших квадратов)
Что мы там хотим добавить к этим методам?
Объясните волшебные идеи и подходы, примененные в древности к персептрону. Ну не о backpropagation же вы хотите рассказать?
И, наконец, подробнее про революционную "идею обучения некоторой функции по входным значениям" . Извините, но мы теорию функций вообще знаем, или как? Судя по вашим постам на форуме, от вас можно ожидать что знаете. Вы в состоянии понять, что здесь имеет место быть просто подмена термина?
И про расширенные возможности подробнее, пожалуйста.
Здравствуйте, Gaperton, Вы писали:
G>Здравствуйте, AndreyFedotov, Вы писали:
AF>>Здравствуйте, Gaperton, Вы писали:
G>>>Вы не об этом. Это не может быть причиной. Известен набор пар точка-значение. Использовать можно ЛЮБОЙ метод, при этом хотите вы этого или нет, интерполяционная функция будет принадлежать какому-то наперед известному классу параметрических функций. Будь то сплайны, отрезки ряда фурье, полиномы, или (в случае НС) многослойный персептрон. Все перечисленные функции кроме персептрона имеют очевидные свойства и предсказуемое поведение, при равной персептрону описательной силе, которая в большей степени определяется количеством настраиваемых параметров, а не видом функции. Вид функции влияет на скорость сходимости (точность приближения), и здесь персептрон тоже в аутсайдерах. AF>>Если понимать под нейронными сетями ТОЛЬКО функции вида пороговая функция от суммы произведения значений в точках на вес. То это верно. Но разве я что то говорил про ПЕРСЕПТРОН? А если идею обучения некоторой функции по входным значениям? Тогда Ваши же аргументы работают против Вас. Посокольку все те чудные свойства функций ЛЮБОГО заданного класса — остаются. Как и прогнозированное поведение. И добавляется лишь ещё одни и довольно эффективный метод работы с ними. Что по определению расширяет возможности. Из известных мне работ уже давным давно никто персептроном не пользуется. Используются именно идеи и подходы, которые были применены в древности к персептрону. Но не он сам.
G>Ох, не хотел в дисскуссию ввязываться, но здесь не могу удержаться. Хватаем за язык.
G>Объясните четко и недвусмысленно про "довольно эффективный метод", который "еще один" и "добавляется". На примере: G>1) Рядов фурье. G>2) Многочленов. (метод наименьших квадратов) G>Что мы там хотим добавить к этим методам?
Вот и поясните на примере этих же методов, как их применить на обучающей выборке? А не заданной функции, к которой их применяют. БЕЗ исползования Backpropagation и подходов используемых в теории НС. Если сумеете — как говриться — съем свою шляпу...
G>Объясните волшебные идеи и подходы, примененные в древности к персептрону. Ну не о backpropagation же вы хотите рассказать?
В том числе и backpropagation. Где этот медод применялся до НС? Не в математике — а в технике, особенно применительно к распознаванию?
G>И, наконец, подробнее про революционную "идею обучения некоторой функции по входным значениям" . Извините, но мы теорию функций вообще знаем, или как? Судя по вашим постам на форуме, от вас можно ожидать что знаете. Вы в состоянии понять, что здесь имеет место быть просто подмена термина?
Знаем. Да это действительно другое название одного и того же. Причём подмена термина идёт в обе стороны.
G>И про расширенные возможности подробнее, пожалуйста.
Как раз определение коэффициентов тех же многчленов или рядов фурье по обучающим выборкам.
Здравствуйте, AndreyFedotov, Вы писали:
G>>Объясните четко и недвусмысленно про "довольно эффективный метод", который "еще один" и "добавляется". На примере: G>>1) Рядов фурье. G>>2) Многочленов. (метод наименьших квадратов) G>>Что мы там хотим добавить к этим методам? AF>Вот и поясните на примере этих же методов, как их применить на обучающей выборке? А не заданной функции, к которой их применяют. БЕЗ исползования Backpropagation и подходов используемых в теории НС. Если сумеете — как говриться — съем свою шляпу...
G>>Объясните волшебные идеи и подходы, примененные в древности к персептрону. Ну не о backpropagation же вы хотите рассказать? AF>В том числе и backpropagation. Где этот медод применялся до НС? Не в математике — а в технике, особенно применительно к распознаванию?
Ну, это легко. Я объясню для одномерного случая, в многомерном все то же самое.
Начнем с того, что обобщенный метод фурье дает решение с наименьшим квадратичным отклонением. Базис можно выбирать любой, в том числе и многочлены. Поэтому ограничимся рядом фурье. Если кратко, применяем стандартный для физиков прием: раскладываем в ряд функцию
Сумма( ДельтаФункцияДирака( x — x[ i ] ) * y[ i ] ).
Сетка будет вообще говоря неравномерна, поэтому делаем так. Берем выборку из наших пар (точка, значение). Определяем скалярное произведение в функциональном пространстве так:
( f, g ) = Сумма( f( x[i] ) * g( x[ i ] ), i = 1..n ), где x[ i ] — точка из обучающего множества.
Готово. Далее, мы должны добиться того, чтобы базис был ортонормированным в нашем пространстве. Этого легко добиться применив метод ортогонализации (линейная алгебра, первый курс, первый семестр). Легко видеть, что так как мы ввели сетку, задача сводится к задаче линейной алгебры.
Теперь, вычисляем коэффициенты фурье.
K[ j ] = ( f[ j ], y ) / ( y, y ), где f[ j ] — отнормированный базис, y — вектор значений.
Получаем интерполяционный многочлен
F( x ) = Сумма( K[ j ] * f[ j ] );
Я наверняка где-то немного ошибся (пишу по памяти), но я надеюсь идею вы поняли. А идея здесь в том, что коэффициенты входят в многочлен линейно, поэтому их можно посчитать напрямую, без всяких извращений типа минимизации невязки градиентным спуском, как в НС.
Ну а метод наименьших квадратов применительно к многочленам известен и широко описан в литературе.
Здравствуйте, Mikola, Вы писали:
M>Здравствуйте, LaptevVV, Вы писали:
LVV>>А Mikola молчит чего-то LVV>>Давай, Колись поконкретней, чего надо-то?
M>Ну поконкретней я уж написал — хотя бы в общих чертах (описание процесса, без текста проги): Как нейронная сеть может обучаться и ловить в потом логические ошибки в программе. Язык — все-равно какой. Чтоб это можно было бы сдать как РГЗ. M>Вы говорили, что Вам студенты дипломы сдавали на эту тему. Можт кинете чего мне. Мне ж не для продажи надо, а чтоб сдать это РГЗ. Так сказать, для умственного развития M>Потому что самому такое придумать — мозгов не хватает пока
Тогда главное — правильно отобразить проблемы синтаксического анализа во входные сигналы нейросети. Если это сумеешь — дальше просто. Найди книжку Роберта Каллана "Основные концепции нейронных сетей" или книжку Уотермена "Нейронные сети" — там подробно написано. Вся закавыка — как и что поставить в соответствие входным сигналам нейросети.
В этом вся докторская и состоит.
Хочешь быть счастливым — будь им!
Без булдырабыз!!!
Здравствуйте, AndreyFedotov, Вы писали:
G>>Объясните волшебные идеи и подходы, примененные в древности к персептрону. Ну не о backpropagation же вы хотите рассказать? AF>В том числе и backpropagation. Где этот медод применялся до НС? Не в математике — а в технике, особенно применительно к распознаванию?
Небольшой комментарий по этому вопросу.
Метод backpropagation представляет собой минимизацию функции ошибки (невязки) для многослойного персептрона методом сопряженного градиента. Подобные медоды применялись в вычислительной математике, но с многослойным персептроном из-за его идиотского вида была проблема. Дело в том, что там не так просто посчитать градиент. Основная заслуга автора метода backpropagation как раз и состоит в изобретении метода расчета градиента для многослойного персептрона, что и вдохнуло жизнь в заглохшее было направление.
Соответственно, я не стал бы говорить об огромном значении метода backpropagation для остальной математики, и теории функций в частности.
Здравствуйте, Gaperton, Вы писали:
G>Здравствуйте, AndreyFedotov, Вы писали:
G>>>Объясните волшебные идеи и подходы, примененные в древности к персептрону. Ну не о backpropagation же вы хотите рассказать? AF>>В том числе и backpropagation. Где этот медод применялся до НС? Не в математике — а в технике, особенно применительно к распознаванию?
G>Небольшой комментарий по этому вопросу.
G>Метод backpropagation представляет собой минимизацию функции ошибки (невязки) для многослойного персептрона методом сопряженного градиента. Подобные медоды применялись в вычислительной математике, но с многослойным персептроном из-за его идиотского вида была проблема. Дело в том, что там не так просто посчитать градиент. Основная заслуга автора метода backpropagation как раз и состоит в изобретении метода расчета градиента для многослойного персептрона, что и вдохнуло жизнь в заглохшее было направление.
G>Соответственно, я не стал бы говорить об огромном значении метода backpropagation для остальной математики, и теории функций в частности.
Согласен. Новизна на мой взгляд состояла не в самом применении этого метода (который был известен давно), а в посторении опреденённой дисциплины из многих известных методов. Пользу тут приносит не столько каждый конкретный метод, сколь их компиляция.
Здравствуйте, Gaperton, Вы писали:
G>Здравствуйте, AndreyFedotov, Вы писали:
G>>>Объясните четко и недвусмысленно про "довольно эффективный метод", который "еще один" и "добавляется". На примере: G>>>1) Рядов фурье. G>>>2) Многочленов. (метод наименьших квадратов) G>>>Что мы там хотим добавить к этим методам? AF>>Вот и поясните на примере этих же методов, как их применить на обучающей выборке? А не заданной функции, к которой их применяют. БЕЗ исползования Backpropagation и подходов используемых в теории НС. Если сумеете — как говриться — съем свою шляпу...
G>>>Объясните волшебные идеи и подходы, примененные в древности к персептрону. Ну не о backpropagation же вы хотите рассказать? AF>>В том числе и backpropagation. Где этот медод применялся до НС? Не в математике — а в технике, особенно применительно к распознаванию?
G>Ну, это легко. Я объясню для одномерного случая, в многомерном все то же самое.
G>Начнем с того, что обобщенный метод фурье дает решение с наименьшим квадратичным отклонением. Базис можно выбирать любой, в том числе и многочлены. Поэтому ограничимся рядом фурье. Если кратко, применяем стандартный для физиков прием: раскладываем в ряд функцию G>Сумма( ДельтаФункцияДирака( x — x[ i ] ) * y[ i ] ).
G>Сетка будет вообще говоря неравномерна, поэтому делаем так. Берем выборку из наших пар (точка, значение). Определяем скалярное произведение в функциональном пространстве так: G>( f, g ) = Сумма( f( x[i] ) * g( x[ i ] ), i = 1..n ), где x[ i ] — точка из обучающего множества.
G>Готово. Далее, мы должны добиться того, чтобы базис был ортонормированным в нашем пространстве. Этого легко добиться применив метод ортогонализации (линейная алгебра, первый курс, первый семестр). Легко видеть, что так как мы ввели сетку, задача сводится к задаче линейной алгебры.
G>Теперь, вычисляем коэффициенты фурье.
G>K[ j ] = ( f[ j ], y ) / ( y, y ), где f[ j ] — отнормированный базис, y — вектор значений.
G>Получаем интерполяционный многочлен
G>F( x ) = Сумма( K[ j ] * f[ j ] );
G>Я наверняка где-то немного ошибся (пишу по памяти), но я надеюсь идею вы поняли. А идея здесь в том, что коэффициенты входят в многочлен линейно, поэтому их можно посчитать напрямую, без всяких извращений типа минимизации невязки градиентным спуском, как в НС.
По памяти написано верно и идея прекрасная. Для случая, когда выборка одна и фиксирована. Но как это будет работать, когда в одних и тех же точках в разных обучающих выборках будут разные значения?
G>Ну а метод наименьших квадратов применительно к многочленам известен и широко описан в литературе.
Метод наименьших квадратов преполагает, насколько я помню, что все выборки известны сразу...
Здравствуйте, AndreyFedotov, Вы писали:
AF>По памяти написано верно и идея прекрасная. Для случая, когда выборка одна и фиксирована. Но как это будет работать, когда в одних и тех же точках в разных обучающих выборках будут разные значения?
Например, так. Для каждой дублирующейся точки добавляем вес (количество дубликатов) в соответсвующий член скаларного произведения.
у[i] в точке-дубликате считаем за среднее значений в этой точке. И все. Здесь, правда, неплохо-бы доказать что получится решение с наименьшим отклонением. Но оно так или иначе получится (не так, так по другому), здесь принципиальных проблем нет.
Вариант №2, для сильно многомерного случая. Используем метод монте-карло для расчета коэффициентов фурье, предполагаем что обучающая выборка является "случайной" последовательностью, ортогонализацию базиса не проводим, скалярное произведение не меняем (пусть будет стандартное для L2). Здесь проблема дубликатов не стоит, а интегралы можно вычислять итеративно. Никакого отличия от НС "по интерфейсу".
Ну как там насчет шляпы? Есть-то придется G>>Ну а метод наименьших квадратов применительно к многочленам известен и широко описан в литературе.
AF>Метод наименьших квадратов преполагает, насколько я помню, что все выборки известны сразу...
Ну и что? Чем именно это плохо? Все равно сеть сначала обучают, а потом используют, она не может "дообучатся" по мере использования. Так что где практическая разница?
Здравствуйте, Gaperton, Вы писали:
G>Здравствуйте, AndreyFedotov, Вы писали:
AF>>По памяти написано верно и идея прекрасная. Для случая, когда выборка одна и фиксирована. Но как это будет работать, когда в одних и тех же точках в разных обучающих выборках будут разные значения?
G>Например, так. Для каждой дублирующейся точки добавляем вес (количество дубликатов) в соответсвующий член скаларного произведения. G>у[i] в точке-дубликате считаем за среднее значений в этой точке. И все. Здесь, правда, неплохо-бы доказать что получится решение с наименьшим отклонением. Но оно так или иначе получится (не так, так по другому), здесь принципиальных проблем нет.
G>Вариант №2, для сильно многомерного случая. Используем метод монте-карло для расчета коэффициентов фурье, предполагаем что обучающая выборка является "случайной" последовательностью, ортогонализацию базиса не проводим, скалярное произведение не меняем (пусть будет стандартное для L2). Здесь проблема дубликатов не стоит, а интегралы можно вычислять итеративно. Никакого отличия от НС "по интерфейсу".
G>Ну как там насчет шляпы? Есть-то придется G>>>Ну а метод наименьших квадратов применительно к многочленам известен и широко описан в литературе.
AF>>Метод наименьших квадратов преполагает, насколько я помню, что все выборки известны сразу... G>Ну и что? Чем именно это плохо? Все равно сеть сначала обучают, а потом используют, она не может "дообучатся" по мере использования. Так что где практическая разница?
Во-первых сети то как раз могут дообучаться.
Во-вторых дообучение можно организовать и для рядов Фурье и для наименьшего квадрата.
В-третьих наш подход ничем не отличается. Метод backpropagation можно применить и к многочленам и к рядам Фурье.
В чётвёртых — ряд Фурье или многочлен так же можно рассматривать как нелинейную нейронную сеть. Это всего лишь вопрос определения того, что называть нейронной сетью. (Кто сказал что только функции вида СУММА( wi * xi ) ? )
Так что как не крути — а шлапу придётся есть нам обоим. Я честно извиняюсь за непарламенские выражения, примённые мной по недомыслию в ходе состоявшейся дискусии, признаю себя ослом и ем свою половину шляпы...
Здравствуйте, AndreyFedotov, Вы писали:
AF>Здравствуйте, Socrat, Вы писали:
S>>А у меня вопрос: а можно заставить нейронные сети играть в шахматы? Или хотя бы в шашки?
AF>Можно. Правда пока не слышал, что бы это кто-то сделал...
А в чем проблема? Или речь идет уже о создании ИИ, который еще предстоит научить играть в шахматы?
Здравствуйте, Socrat, Вы писали:
S>Здравствуйте, AndreyFedotov, Вы писали:
AF>>Здравствуйте, Socrat, Вы писали:
S>>>А у меня вопрос: а можно заставить нейронные сети играть в шахматы? Или хотя бы в шашки?
AF>>Можно. Правда пока не слышал, что бы это кто-то сделал...
S>А в чем проблема? Или речь идет уже о создании ИИ, который еще предстоит научить играть в шахматы?
Теоретически проблем нет. Тут как раз очень хорошая ситуация для обучения сети. Правда огромное число вариантов. Такие работы делались, правда на уровне отдельных ходов. Что бы был достигнут уровень хорошей игры в целом — я не слышал. Хотя теоретически это вполне возможно...
Здравствуйте, AndreyFedotov, Вы писали:
AF>Здравствуйте, Socrat, Вы писали:
S>>Здравствуйте, AndreyFedotov, Вы писали:
AF>>>Здравствуйте, Socrat, Вы писали:
S>>>>А у меня вопрос: а можно заставить нейронные сети играть в шахматы? Или хотя бы в шашки?
AF>>>Можно. Правда пока не слышал, что бы это кто-то сделал...
S>>А в чем проблема? Или речь идет уже о создании ИИ, который еще предстоит научить играть в шахматы?
AF>Теоретически проблем нет. Тут как раз очень хорошая ситуация для обучения сети. Правда огромное число вариантов. Такие работы делались, правда на уровне отдельных ходов. Что бы был достигнут уровень хорошей игры в целом — я не слышал. Хотя теоретически это вполне возможно...
А обучение там велось по каждому ходу или по результатам всей партии?
Здравствуйте, Socrat, Вы писали:
S>Здравствуйте, AndreyFedotov, Вы писали:
AF>>Здравствуйте, Socrat, Вы писали:
S>>>Здравствуйте, AndreyFedotov, Вы писали:
AF>>>>Здравствуйте, Socrat, Вы писали:
S>>>>>А у меня вопрос: а можно заставить нейронные сети играть в шахматы? Или хотя бы в шашки?
AF>>>>Можно. Правда пока не слышал, что бы это кто-то сделал...
S>>>А в чем проблема? Или речь идет уже о создании ИИ, который еще предстоит научить играть в шахматы?
AF>>Теоретически проблем нет. Тут как раз очень хорошая ситуация для обучения сети. Правда огромное число вариантов. Такие работы делались, правда на уровне отдельных ходов. Что бы был достигнут уровень хорошей игры в целом — я не слышал. Хотя теоретически это вполне возможно...
S>А обучение там велось по каждому ходу или по результатам всей партии?
По-разному.
Мне известен следующий подход:
Настраиваются отдельные сети на различные ходы. Каждая сеть распознаёт одну или несколько комбинаций и вариантов действий. Затем сети объединяются и при анализе положения фигур на доске — голосуют, за тот или иной вариант действий. Их выходы рассматриваются сетями более высокого уровня, чья задача — выбрать итоговый вариант действий.
С Уважением, Андрей
S>>А обучение там велось по каждому ходу или по результатам всей партии?
AF>По-разному. AF>Мне известен следующий подход: AF>Настраиваются отдельные сети на различные ходы. Каждая сеть распознаёт одну или несколько комбинаций и вариантов действий. Затем сети объединяются и при анализе положения фигур на доске — голосуют, за тот или иной вариант действий. Их выходы рассматриваются сетями более высокого уровня, чья задача — выбрать итоговый вариант действий. AF> С Уважением, Андрей
Так это уже получается одна сеть, более высокого порядка.
S>>>А обучение там велось по каждому ходу или по результатам всей партии?
AF>>По-разному. AF>>Мне известен следующий подход: AF>>Настраиваются отдельные сети на различные ходы. Каждая сеть распознаёт одну или несколько комбинаций и вариантов действий. Затем сети объединяются и при анализе положения фигур на доске — голосуют, за тот или иной вариант действий. Их выходы рассматриваются сетями более высокого уровня, чья задача — выбрать итоговый вариант действий. AF>> С Уважением, Андрей
S>Так это уже получается одна сеть, более высокого порядка.
В общем то да. Я просто хотел продемонстрировать общую идею построения такой сети.
Хотя за деталями лучше обращаться к тем, кто подобные сети строил. Я сам занимался распознаванием образов. Например лиц и автомобилей.
С Уважением, Андрей
Здравствуйте, Аноним, Вы писали:
А>Здравствуйте, Mikola, Вы писали:
M>>Народ, нужен алгоритм и/или описание нейронной сети, которая ищет логические ошибки в коде программы (язык-любой) M>>Помогите plz. кто чем может M>>
А> Есть теорема, указывающая на принципиальную невозможность создания системы, проверяющей логическую верность программы по её тексту...И здесь — нате
ну не знаю...
есть такая вещь, как конструктивная логика в которой требуемая функциональность системы — формула, а программа, обеспечивающая данную функциональность — доказательство ентой формулы. так что _правильно_ работающая программа енто не что-то случайное
исходя ТОЛЬКО из текста проги, может и нельзя.
но если умудриться формализовать то, что должна делать прога, доказать эту формулу исходя из каких-либо
заранее определённых аксиом с помощью каких-либо заранее определённых правил вывода, и сравнить доказательство с текстом —
вот тебе и на)
хотя, если сделать такую штуку... ну не Нобелевскую (её математикам не дают) но AMS премию точно отхватишь.
ещё придётся учебник писать и лекции читать.
принципиально енто возможно.
вот
. Извините, но мы теорию функций вообще знаем, или как? Судя по вашим постам на форуме, от вас можно ожидать что знаете. Вы в состоянии понять, что здесь имеет место быть просто подмена термина?
