0%

在刚搭起博客的时候,我用的评论系统是Disqus,大概长这个样子

Disqus在世界范围内的用户很多,也比较有名。但问题也是显而易见的:需要登录社交账号来留言,太笨重;而且如果不科学上网,Disqus根本无法使用。

因此,我希望能找到一个墙内可用、不需要登录的轻量的评论系统,然后我从同学的blog那里看到了valine

valine的使用需要基于BaaS平台leanCloud,依据快速开始页进行设置就好。

然后在/themes/next/_config.yml里配置:

1
2
comments:
active: valine
1
2
3
4
5
6
7
8
9
valine:
enable: true
appid: [自己的appid]
appkey: [自己的appkey]
notify: false # 因为常看blog,就不用邮件提醒了
verify: false # 不会有人在我这刷评论吧?
placeholder: (((*°▽°*)八(*°▽°*))) # 可可爱爱
avatar: https://www.gravatar.com/avatar/[自己的hash] #Gravatar的头像链接或者mp这种通用头像
language: zh-cn

然后hexo clean && hexo g就可以了!

大概长这个样子:

清爽多了。

又水了一篇blog。

论文链接

我家鲨鱼觉得我太摸了,亲自跑到电脑前面来替我写论文笔记(×

废话:

看了这三篇我才反应过来我看的顺序好像有点问题……

Soft Reasoner是最先的,这篇PRover是第二个,然后才是ProofWriter(那个基于T5-11B,全程diss PRover的)。

反正是用神经方法做推理……玄而又玄,众妙之门

摘要

作者提出了PRover,一个可解释的、基于Transformer的模型,既可以在自然语言规则库上进行推理(判断对错),也可以写出推理结论的证明。

阅读全文 »

论文链接

单纯觉得这个灯泡表情非常魔性……

摘要

作者提出了名叫RuleTaker的推理模型,其中的事实和规则都是自然语言(而不需要逻辑表示或者概率表示这种规范表示),以Transformer为基础在自然语言上进行推理。

值得一提的是,作者本人也不很信任这个推理,所以也叫它软推理……

这一模型在两个人工创作的规则集上有较好的泛化表现。

阅读全文 »

论文链接

废话:

我感觉这就是拿着T5做了个finetune……它的迭代式模型很有意思,也很暴力。刚看到一次性模型和迭代式模型的表现差不多的时候我还挺失望的,后来发现迭代式模型在泛化能力上的优势还是有的。

感觉是不是可以怎么优化一下迭代式模型的迭代过程,不要没头苍蝇式的地乱撞。不行可以backward chaining?

摘要

作者提出了一个叫做ProofWriter的生成式模型,既可以用自生成理论的含义,又可以写出用自然语言表示的证明过程。

阅读全文 »

论文地址

引入

现有的QA数据集大多数并不涉及复杂的推理过程(只在一个文段内推理,或者只需要一步推理)。

那些需要多跳推理的数据集,则主要围绕已有的知识库构建,限制了其多样性(问题一定围绕着知识库的架构来走),问题的解答也很单一。

另外,问题的监督粒度也太粗,只能针对问题来监督回答是否正确。

基于这三个问题,作者提出了HotpotQA数据集,特点在于:

  • 多跳推理
  • 不基于任何的范式,更加自然
  • 引入了一类全新的“实体比较”类问题,可以测试模型在常识方面的理解
阅读全文 »

今天写论文笔记的时候,发现hexo对mathjax渲染的时候Markdown和\(\LaTeX\)会产生冲突,主要是_*这两个字符。之前因为问题加个\就解决了,所以也没有在意。但是今天这个冲突比较厉害,一时间改不过来,去查找解决方案的时候发现可以把hexo的渲染引擎改为pandoc。

阅读全文 »

论文链接

摘要

目前的多条推理数据集的一个重大缺陷是它们所要求的推理步骤都【显式地】表达在问题中。本文介绍StrategyQA,一个推理步骤【隐式地】包含在问题中,需要用策略来推导的QA基准测试。

StrategyQA一共包含2780个条目,每个条目包括:

  • 一个策略问题(推理步骤隐含)
  • 若干子问题,是策略问题的分解(每个推理步骤一个子问题)
  • 包含了每个子问题答案的维基百科文段

回答是yes/no。

这些问题都很短而且覆盖了很大的范围,人类表现约为87%,而baseline则是66%。

阅读全文 »

论文地址

摘要

作者将神经方法和逻辑推理结合起来,给出了一个新模型来处理自然语言上的多跳推理。作者提出,还是应用Prolog prover进行推理,但是应用了一个基于预训练语句encoder的相似度函数,通过反向传播来fine-tune相似度函数的表示。这样就可以在自然语言上实现基于规则的推理,也可以引入领域内的特定知识。

阅读全文 »

论文地址

引入

作者希望用神经网络来解决SAT问题,提出了NeuroSAT模型。

NeuroSAT在训练过程中对每个问题的监督只有“可满足”和“不可满足”两种状态。测试时,每次给一个SAT问题P,NeuroSAT就会给出这个问题是否可满足,而且如果一个问题被判定为可满足,我们几乎总是可以从激活函数中找到一组合法的值代入。

他们又对模型进行了修改,输入的是有少量矛盾的不可满足问题,让模型自己去找到矛盾并改正,他们把这个修改叫NeuroUNSAT。

阅读全文 »

End-to-End Differentiable Proving

论文链接

写在前面的废话

刚开始认认真真地看论文,只是看的速度实在是太慢了。感觉记录下来的东西有点类似于不正式的翻译,非常流水账,但是什么东西都不记又什么都记不住,左耳朵进右耳朵出了。 学长分配给的论文还有6篇,这篇也刚刚看完结构和LOSS,道阻且长……

前置知识

知识库自动补全(automated Knowledge Base completion)

给定知识库中已有的一部分信息,自动推导出缺失的信息。

多跳的(multi-hop)

与一步的逻辑推理相对,指\(A\, \wedge (A\to B)\,\wedge (B\to C) \, \wedge (C\to D)\Rightarrow D\)这类需要经过多步的推理。

次符号的(subsymbolic)

我还没理解。似乎是指粒度比符号更小?

Introduction

目前的知识库自动补全SOTA模型使用神经链预测模型(neural link prediction model)来学习符号的分布向量表示。向量表示允许模型通过相似性来对未知的事实进行泛化。

然而,神经链预测模型对于需要多个步骤进行预测的情况预测不佳(A是B的父亲,B是C的家长=>A是C的祖父或祖母)。与之相反,符号定理证明器(symbolic theorem prover)正好可以处理这类问题。进一步,归纳逻辑程序设计(Inductive Logic Programming)利用这些证明器来从数据中学到可解释的规则并且在完成知识库的过程中进行应用。 但是,symbolic prover在subsymbolic表示的学习和相似度比较上能力比较差,这限制了他们对相似但不完全相同的询问进行泛化的能力。

尽管逻辑和机器学习的联系的问题已经由统计相关学习方法(statistical relational learning approaches)所解决了,以往的模型要么不支持次符号表示的推理,要么不是端到端训练出来的。神经多跳推理模型(neural multi-hop reasoning chain)通过将推理链encode到向量空间上去(也就是:在与答案进行比对之前,先迭代地将subsymbolic representation进行refine),在某种程度上解决了这个问题。但是它也有问题:可解释性差,而且难以显式地将领域内知识(例如作为某条规则)传递进去。

受到Prolog的反向链式算法和使用次符号表示的可微的归一化操作的方法,作者提出了Neural Theorem Prover。

阅读全文 »