ESTO PURUS · ESTO UNUS
TENE FIDEM · TENE MODUM
Lex Blog
Recent Blogs
可满足性模理论 (Satisfiability Modulo Theories)
很多实际问题用纯命题逻辑（SAT）表达时，要么根本无法表达。而用一般的一阶逻辑或高阶逻辑表达虽然自然，却无法自动高效求解。人们要么用专用算法解决特定问题（如线性规划、等价性检查），难以组合多种约束。SMT 把 SAT 的布尔搜索与多个理论求解器组合起来，使得混合理论约束可以被统一、自动地判定。
数学与画家
结构本身就是定理，AI 也有结构，只是那种结构人读不懂。关键在于可翻译性，以及把计算翻译成结构的制度是否跟得上。硬算常给出有限情形的答案而非「为什么」，而把针对性的结果一般化、翻译成可复用结构的制度，在 AI 数学的产出链条里是断的。
F-散度族及其推论
f-散度族（f-divergence）用一个凸函数 f 统一刻画两个概率分布之间的差异，KL、JS、全变差、卡方、Hellinger、α-散度都是它的特例。
克劳德·香农小传
从密歇根小镇那根架在铁丝围栏上的电报线，到贝尔实验室走廊里的独轮车，再到麻省理工那间堆满零件的办公室。他给「信息」下了数学定义，自己却一辈子只对有意思的东西负责。
Dirichlet 分布与证据深度学习
Dirichlet 是单纯形上的分布、多项分布的共轭先验，也是「关于概率的概率」这一二阶对象的自然载体。本文先给出它在定义、矩结构、共轭更新与分裂构造上的完整形式化，神经网络的输出重解释为证据并参数化迪利克雷分布，推导证据深度学习的对数损失等应用。