По следам моего недавнего поста про то, в какой степени математика основана на логической строгости оформления доказательств (в том числе
( Read more... )
Ну так это же проблема останова. Как, глядя на программу, понять, зависает она или нет, не запуская интерпретатор? как известно - никак. Доказательство, как известно, это то же самое что программа. Если бы, глядя на доказательство, но не разбирая его детально, можно было бы понять, валидно оно или нет - у нас был бы способ решения проблемы останова...
Не сказал бы что это ровно та же проблема. Аналогия хорошая. Но насколько я знаю, никакие попытки алгоритмизировать процесс проверки нетривиальных доказательств не удались, даже записать любое сложное док-во так, чтобы программа могла его проверять (и при этом действительно ловить настоящие ошибки, если они там есть), оказалось непосильным для человека адским трудом.
Так что связь с проблемой останова алгоритма тут пока что только умозрительная, а не фактическая.
По-моему, аналогия достаточно строгая (хотя чтобы показать всё строго надо написать много букв). Соответствие между доказательствами и программами - это вполне строгая теорема (изоморфизм Карри-Ховарда). Заставить компьютер автоматически доказывать теоремы не получается в основном просто потому, что у компьютера "нет фантазии" (он не может просто посмотреть на теорему и решить, а давай-ка по индукции). В принципе, в существующих системах автоматизации доказательств (agda2, idris, epigram, coq) есть режим автоматизированного доказательства: человек говорит "попробуй индукцию по N", машина пробует и пишет что получилось. Т.е. от человека требуется описать последовательность применяемых приёмов (здесь по индукции, а вот это выделить в лемму, а лемму доказать от противного, итд). В нынешних условиях в принципе даже немного удивительно, что никто ещё не прикрутил нейросеть в этом месте (но понятно: мало материала для обучения
( ... )
Небезызвестная контора Дипмайнд вполне себе пытается прикрутить, врут, что почти забороли геометрию.
Проблема конечно же в том, что то, что сейчас называется "обучением языковых моделей" обучением в полноценном смысле слова не является. Более того, легко заметить, что люди, как правило, обучаются на очень небольшом количестве информации, иногда хватает сотни - другой байт чтоб обучающийся смог домыслить идею. :-)
Математика - это не язык программирования и не способ организовать машинную проверку. Математика - это язык, на котором люди общаются с людьми, а доказательства - это человекопонимаемые объяснения. Аскольд Хованский вообще меня учил, что если у теоремы есть только одно доказательство - значит, мы ещё не до конца понимаем эту теорему.
А формальная корректность объяснений появляется тогда, когда из-за двусмысленностей естественных языков возникает двусмысленность утверждений. Скажем, пока вы занимаетесь чистой арифметикой (4 операции, "поле"), то, говоря про "числа", вы можете не уточнять, какие "числа" вы имеете в виду, рациональные, вещественные или какие-то промежуточные расширения. Но как только вы доберётесь до разрешимости уравнений, становится понятно, что "числа" бывают разными. Пока ваши уравнения алгебраические, вам не нужно детальное понимание того, что такое вещественное число, но как только понадобится понятие предела - всё, возвращайтесь назад (вперёд) и занимайтесь аккуратным построением.
Спасибо за пояснения и комментарии, и мы с вами примерно это уже обсуждали тут.
В посте я попытался высветить именно мысль, что пониманию этого нельзя научить, по крайней мере научить иначе кроме как методом "смотри как я и делай примерно так же".
Научить умножать числа столбиком можно, объяснив смысл процедуры (можно и не объясняя, конечно, но не будем о грустном). Но научить составлять правильные доказательства или искать ошибки в доказательствах никакими мета-алгоритмами невозможно, по-моему.
если учитель заявляет, что доказательство ученика неверно - он должен свое заявление доказать.Как раз с этим то проблем особых нет. Либо это просто ошибка в логическом выводе(из А следует Б а на самом деле не следует), либо необоснованное неправильное утверждение(приводится контрпример), либо необоснованное правильное утверждение(то есть когда то, что надо доказать проговаривается другими словами, но не доказывается). Так вот во всех этих случаях учителю (заметим что в математике, когда учитель и ученик это вообще один и тот же человек, является скорее типичным чем исключением) помогает именно понимание почему результат должен быть верен или неверен. Понимания, которое обычно вне контекста пространства конкретного доказательства. Например когда ученик пытается доказать более общее утверждение, которое попросту не является верным в этом более общем контексте. Например, некоторое утверждение для конечномерных операторов заведомо не является верным для бесконечномерных(с явными, заранее известными учителю, контрпримерами), и если в
( ... )
Было это где-то в 2006 году. Осознал я это в их первом летнем лагере, между 5 и 6 классом... Ну, рано же в таком возрасте их этому учить - только портить и отбивать охоту через страх непонимания. В таком возрасте надо решать задачки из Кордемского или Сахарова, смекалку прокачивать. А качать формализм - лучший способ похоронить интерес.
У вас большой опыт обучения детей в маткружках? Опыт показал, что именно этих - не рано было. Ни у кого интерес не похоронился. Задачки на смекалку они уже до того целый год в кружке в городе решали. Те, кто не решали, в лагерь не поехали.
Кроме того, формализм особо не прокачивался - таблички истинности сами по себе и упрощения логических выражений это еще не формализм.
Кружковцы особ статья, там предварительная селекция пройдена. Но всё равно рано. Класса с 8 нормально. Тогда усвоят все, а не только избранные.
Детей прошлым летом по Кордемскому натаскивал с абсолютного нуля в течение месяца. Опытная группа была в 8-13 человек, состав плавал. Решали во дворе, прямо на скамейке, за конфеты решившим. Символическая награда, но с утра ко мне летел за задачами весь двор )
Comments 65
Ну так это же проблема останова. Как, глядя на программу, понять, зависает она или нет, не запуская интерпретатор? как известно - никак. Доказательство, как известно, это то же самое что программа. Если бы, глядя на доказательство, но не разбирая его детально, можно было бы понять, валидно оно или нет - у нас был бы способ решения проблемы останова...
Reply
Но насколько я знаю, никакие попытки алгоритмизировать процесс проверки нетривиальных доказательств не удались, даже записать любое сложное док-во так, чтобы программа могла его проверять (и при этом действительно ловить настоящие ошибки, если они там есть), оказалось непосильным для человека адским трудом.
Так что связь с проблемой останова алгоритма тут пока что только умозрительная, а не фактическая.
Reply
Reply
Проблема конечно же в том, что то, что сейчас называется "обучением языковых моделей" обучением в полноценном смысле слова не является. Более того, легко заметить, что люди, как правило, обучаются на очень небольшом количестве информации, иногда хватает сотни - другой байт чтоб обучающийся смог домыслить идею. :-)
Reply
Математика - это не язык программирования и не способ организовать машинную проверку. Математика - это язык, на котором люди общаются с людьми, а доказательства - это человекопонимаемые объяснения. Аскольд Хованский вообще меня учил, что если у теоремы есть только одно доказательство - значит, мы ещё не до конца понимаем эту теорему.
А формальная корректность объяснений появляется тогда, когда из-за двусмысленностей естественных языков возникает двусмысленность утверждений. Скажем, пока вы занимаетесь чистой арифметикой (4 операции, "поле"), то, говоря про "числа", вы можете не уточнять, какие "числа" вы имеете в виду, рациональные, вещественные или какие-то промежуточные расширения. Но как только вы доберётесь до разрешимости уравнений, становится понятно, что "числа" бывают разными. Пока ваши уравнения алгебраические, вам не нужно детальное понимание того, что такое вещественное число, но как только понадобится понятие предела - всё, возвращайтесь назад (вперёд) и занимайтесь аккуратным построением.
Что может быть более очевидным ( ... )
Reply
В посте я попытался высветить именно мысль, что пониманию этого нельзя научить, по крайней мере научить иначе кроме как методом "смотри как я и делай примерно так же".
Научить умножать числа столбиком можно, объяснив смысл процедуры (можно и не объясняя, конечно, но не будем о грустном). Но научить составлять правильные доказательства или искать ошибки в доказательствах никакими мета-алгоритмами невозможно, по-моему.
Reply
Reply
Reply
> казалось бы, доказательство от противного - отлично объясняется на табличках истинности
Я вот, честно говоря, не понимаю. Таблички, конечно, дадут нам tertium non datur - ну, и что? Метод доказательства-то тут где?
Кроме того - а как на такой подход натянется та же т.н. интуиционистская логика?
С уважением,
Гастрит
Reply
Было это где-то в 2006 году. Осознал я это в их первом летнем лагере, между 5 и 6 классом...
Ну, рано же в таком возрасте их этому учить - только портить и отбивать охоту через страх непонимания. В таком возрасте надо решать задачки из Кордемского или Сахарова, смекалку прокачивать. А качать формализм - лучший способ похоронить интерес.
Reply
> задачки из Кордемского
Да, мне всегда нравилось навернуть дерево секвенций на задачу об украденном кошельке.
С уважением,
Гастрит
Reply
Опыт показал, что именно этих - не рано было. Ни у кого интерес не похоронился.
Задачки на смекалку они уже до того целый год в кружке в городе решали. Те, кто не решали, в лагерь не поехали.
Кроме того, формализм особо не прокачивался - таблички истинности сами по себе и упрощения логических выражений это еще не формализм.
Reply
Кружковцы особ статья, там предварительная селекция пройдена. Но всё равно рано. Класса с 8 нормально. Тогда усвоят все, а не только избранные.
Детей прошлым летом по Кордемскому натаскивал с абсолютного нуля в течение месяца. Опытная группа была в 8-13 человек, состав плавал. Решали во дворе, прямо на скамейке, за конфеты решившим. Символическая награда, но с утра ко мне летел за задачами весь двор )
Reply
Leave a comment