Isabelle / 子模优化形式化
已完成总量九千六百多行的 thy 文件,正在准备 clean up 发 AFP。
已完成总量九千六百多行的 thy 文件,正在准备 clean up 发 AFP。
还在看混音和画PV
发现所有拉格朗日对偶都会崩塌到 trivial 的 0 bound,只有 conjugate 对偶有 nontrivial 的可能性,所以正在往这个方向继续探索,看看能不能把对偶做成某种打分器。
当两条最自然的 Lagrangian dual 路线都塌到 trivial 0 bound 之后,留下来的反而是一个和 Range(B)、cycle consistency 与 instance difficulty 相关的 dual-based structural score。
Read More从 classical greedy 的 theorem line,走到 LazyGreedy extension、StochasticGreedy skeleton 与一套可继续扩展的 Isabelle/HOL library。
Read More从连续音频到可玩的谱面:起音检测、节拍网格、段落对齐与可玩性约束。
Read More从纯数学走向优化研究:一个学期的研究训练与新的问题切入口。
Read More查看完整的数学栏目文章列表与更新记录。