Logic-based computational method in extremal combinatorics

• 양홍석 교수님
• 발표자료

왜 PL커뮤니티에 강연하나?

Flag algebra는 logic에서 나옴. 요약 해석등의 개념이, 갈루아 연결도, flag algebra의 증명과정에서 쓰임.

Math to CS

Auto-formalization (수학개념->전산논리)

• Morph社의 Trinity가 ABC 추측의 weak ver. 증명

Flag algebra

옛날에 유행하던. 10년 동안 open problem을 풀음. Stability = opt.sol이 근본적으로 유일한지, 아니면 여러 구조가 비슷한 최적치를 갖는지 subgraph density 가 중요 개념. $p (H, G)$ $(,|,H,|,=m \le ,|,G,|,=n)$

infinite case ($n\to \infty$)일 때 flag alg. 가 잘 작동. e.g. $\lim_{ n \to \infty }\sup K_{3}\text{-free}$

semidefinite problem solver 인 flagmatic이용해 풀음. Flag Algebra defines a proof system, which flagmatic searches on.

Subgraph density

G 는 feature vector로 간주. $p(-, G)$라는 $\infty$-차원 벡터로 이해 (embedding)

• 모든 $H$마다 하나의 index. H 는 feature map로 간주. $p(H, -):FinGraph \to \mathbb{R}$

Limiting graph = $\infty$-차원 벡터.

$(G_{n}){n\in\mathbb{N}}$ is increasing , converging ($\forall H.\exists\lim{n \to \infty } p(H, G_{n})$) Set of limiting graphs $\Phi={\lim_{ n \to \infty } p(-, G_{n})}$

• “graphon 이론"과 같은 범주

FA logic

• Expression $E\coloneqq H,|,r\times E,|,0,|,+,|,1,|,\times$
• Assertions. $A\coloneqq E=E,|,E\le E,|,A\land A,|,\neg A$
• Semantics. $[ [E] ]:\Phi\to \mathbb{R}$. $[ [A] ]:\Phi\to \mathbb{B}$

Non-trivial ineq.어떻게?

$H_{\cdot}$ 으로, single-labelled vertex가진 subgraph를 Expression에서 사용. monotone $\alpha:Expr_{\cdot}\to Expr$ 도 정의. $E_{\cdot}$ $k$개 뽑은 후 $\sum_{k} E_{\cdot, i}^{2}\ge 0$ 사용. 후, 양변에 $\alpha$ wrapping (monotone하므로 ㄱㄴ)

[!QUESTION] 그 sum-of-squares 항등식에서 labelled vertex가 하는 일을 모르겠다. $\alpha$ 만들때 말고 언제 쓰이나?

A. $\times$ 등을 계산할 때 역할을 한다.

무슨 $\alpha_{d}$?

adjoint. 내지는 갈루아 연결과 비슷. $\gamma_{d}:FinGraph\to Pr(FinGraph_{\cdot})$ 생각. vertex 암거나 선택해 label주는 확률. Galois connection이 여기서는 $$p(\alpha_{d} (H_{\cdot}), G)=\mathbb{E}{G{\cdot}\sim\gamma_{d}(G)}[p_{\cdot}(H_{\cdot},G_{\cdot})]$$임. 선형대수에서도 $\langle MV, w\rangle = \langle MV, M^{T}w\rangle$에서 비슷한 adjoint relationship이 성립.

monotone한 증명 : gamma 이용해서..

Lean으로 도입

엄상일 교수님, 대학원생들과 직접 하는중인데. subtype coercion (Lean이 두 타입을 같다고 인식을 못함) 그리고 many calculation to be verified. automate하면 좋은데.

purely logical

checking $E\ge 0$ is undecidable 생각) 따라서 SDP solver(Flagmatic 등)으로 bounded-depth relaxation을 쓰는 것.

[!QUESTION] flagmatic의 UB 구하는 과정 중에 결국 search depth에 의존적인 부분이 있는데, Lean에서는 그걸 사용하지 않을 수 있게 되나?

A. 아직은 그걸 하는게 아니고, 이미 증명된 것들을 옮겨오는 중이다.