В минулому році в Академічному університеті пройшов перший конкурс студентських робіт з теоретичної інформатики та дискретної математики ім. Алана Тюрінга. Нещодавно ми оголосили другий конкурс (термін подачі робіт 10 травня 2017 року), а в цій статті ми розповімо про підсумки першого конкурсу.


Читати далі →

Теоретична інформатика в Санкт-Петербурзі


У Санкт-Петербурзі, та й взагалі в Росії, ще кілька років тому не було навчальних закладів, в яких би з першого курсу була побудована цілісна програма, що дозволяє оволодіти теоретичною інформатикою на сучасному рівні.

У минулому році в Санкт-Петербурзькому академічному університеті відкрився бакалаврат (А), готує студентів з інформатики з подальшою спеціалізацією з теоретичної інформатики, розробки програмного забезпечення або біоінформатики.

В цьому році в Санкт-Петербурзькому державному університеті відкривається бакалаврат (Ч) з математики та теоретичної інформатики.

Оскільки я брав участь у створенні обох цих програм, колеги настійливо рекомендують мені порозумітися. (Мене звати Едуард Гірш, і я працюю в лабораторії математичної логіки ПОМІ РАН.)

Читати далі →

«Що таке доказ?»: погляд з теоретичної інформатики

  Теоретична інформатика — один з напрямків навчання на кафедрі Математичних та інформаційні технологій Академічного університету. Нас часто запитують, чим займається теоретична інформатика. Теоретична інформатика — активно розвивається наукове напрямок, що включає в себе як фундаментальні області: алгоритми, складність обчислень, криптографія, теорія інформації, теорія кодування, алгоритмічна теорія ігор, так і більш прикладні: штучний інтелект, машинне навчання, семантика мов програмування, верифікація, автоматичне доказ теорем і багато іншого. Цю статтю ми присвятимо огляду лише невеликого сюжету, а саме розповімо про незвичайні підходах до поняття докази, які розглядає теоретична інформатика.
 
 
 
Щоб пояснити, про якого роду доказах піде мова, розглянемо приклад: є комп'ютерна програма, автори якої стверджують, що програма робить щось певне (конкретні приклади будуть трохи пізніше). Програму можна запустити і отримати відповідь. А як можна впевнитися, що програма робить те, що повинна робити? Добре б, якщо крім відповіді програма видавала б доказ того, що ця відповідь правильна.
 
Розглянемо більш конкретний приклад: ми хочемо мати програму, яка в дводольному графі знаходить паросполучення максимального розміру разом з доказом його максимальності.
 
 
 
Нагадаємо, що граф називається дводольним, якщо його вершини можна пофарбувати в два кольори так, що ребра графа з'єднують вершини різних кольорів. Паросполучення в графі називається така безліч ребер, що ніякі дві з них не мають спільного кінця. Безліч вершин графа називається покриває, якщо кожне ребро графа має як мінімум один кінець в цій множині. Теорема Кеніга свідчить, що в дводольному графі розмір максимального паросполучення збігається з розміром мінімального покриває множини. Таким чином, щоб довести, що паросполучення є максимальним, можна пред'явити, заслону безліч, розмір якого збігається з розміром даного паросполучення. Дійсно, це покриває безліч буде мінімальним, оскільки кожне покриває безліч зобов'язане покрити хоча б один кінець кожного ребра цього паросполучення. Наприклад, у графі на малюнку паросполучення (M1, G3), (M2, G2), (M4, G1) буде максимальним, оскільки є покриває безліч розміру 3, яке складається з G2, G3 і M4. Відзначимо, що перевірити такий доказ набагато простіше, ніж обчислювати максимальне паросполучення: достатньо перевірити, що розмір паросполучення збігається з розміром покриває безлічі і перевірити, що всі ребра покриті.
 
Розглянемо ще один приклад, припустимо нам потрібна програма, яка перевіряє систему нестрогих лінійних нерівностей з раціональними коефіцієнтами на спільність (нагадаємо, що система нерівностей називається спільної, якщо можна підібрати такі значення змінних, що всі нерівності виконуються).
 
 
 
Як можна довести правильність результату? Якщо система сумісна, то доказом спільності може стати рішення цієї системи (неважко довести, що якщо у такої системи є рішення, то є і раціональне рішення, тобто його можна записати). А як довести, що система несумісна? Виявляється, що це зробити можна за допомогою леми Фаркаша, яка стверджує, що якщо система нестрогих лінійних нерівностей несовместна, то можна скласти ці нерівності з невід'ємними коефіцієнтами і отримати суперечливе нерівність 0 ≥ 1. Наприклад, система на малюнку несовместна, і якщо скласти перше рівняння з коефіцієнтом 1, другий з коефіцієнтом 2, а третє з коефіцієнтом 1, то вийде 0 ≥ 1. Доказом несумісності буде якраз набір невід'ємних коефіцієнтів.
 
У цій статті ми поговоримо про те, чи потрібні докази, або перевірка докази завжди не простіше, ніж самостійне рішення задачі. (В прикладі про максимальне паросполучення ми не довели, що не існує алгоритму, вирішального завдання за той же час, скільки займає перевірка докази.) Якщо ми не обмежуємо розмір докази, то виявиться, що докази потрібні, а якщо будемо вимагати, щоб докази були коректними, то питання про потрібність доказів еквівалентний найважливішого відкритого питання про рівність класів P і NP. Потім ми поговоримо про інтерактивні доказах (докази в діалозі). Обговоримо криптографічні докази, які не розголошують зайву інформацію, крім вірності доказуваного затвердження. І закінчимо обговоренням вероятностно перевіряються доказів і знаменитої PCP-теореми, яка використовується для доказу труднощі наближення оптимізаційних завдань.
 
У цій статті ми не будемо торкатися автоматичного доведення теорем та докази коректності програм, хоча ці теми теж досить цікаві.
 
 
Читати далі →