发表机构
Clone Systems; Aristotle University of Thessaloniki; International Hellenic University; University of Southampton; Cyprus University of Technology（克隆系统公司; 塞萨洛尼基亚里士多德大学; 国际希腊大学; 南安普顿大学; 塞浦路斯理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文按被形式化对象将事实核查领域分为五层，综述121项工作，发现现有形式化机制多未应用于此，并指出核查系统验证及两个核查阶段缺乏形式化规范，最后提出开放问题。
AI 中文摘要
自动化事实核查系统会返回一个标签：声明为真或为假。在许多此类系统中，裁决仍是主要输出。通常缺失的是：哪份文件解决了该问题、要改变裁决需要哪些条件不同、或者同一声明经改写后是否会得到相同判断的记录。我们将这一缺失部分称为“论证依据”：一份单独陈述，说明什么得到了保证以及基于何种理由。形式化方法能产生此类证据，而法规也开始要求提供这些证据，因为《数字服务法》和《人工智能法案》均要求提供关于系统行为方式的可审计证据。对自动化事实核查的综述通常按流水线阶段组织，并将逻辑视为众多技术之一。我们转而按被形式化的对象来组织该领域，这给出了五个层级：声明、推理、执行核查的系统、声明传播的生态系统以及监管义务。将121项工作归类到这些层级中，出现了两种模式。大多数相关的形式化机制已经存在，但它们是为其他领域构建的，很少在此应用，且差距最大的是验证核查系统本身。常规专业事实核查人员遵循的几个阶段也没有明确说明的正确性标准，其中两个阶段——以可核查形式撰写声明和纠正已发布的裁决——在我们编码的任何工作中都没有被正式规定。我们以开放问题作结，每个问题都附有建议的第一步。
英文摘要
An automated fact-checking system returns a label: the claim is true, or it is false. In many such systems the verdict remains the primary output. What is generally missing is a record of which document settled the question, of what would have had to be different for the verdict to change, or of whether the same claim, reworded, would have been judged the same way. We call the missing piece a warrant: a separate statement of what was guaranteed and on what grounds. Formal methods produce evidence of this kind, and regulation is beginning to ask for it, since the Digital Services Act and the AI Act both call for auditable evidence about how systems behave. Surveys of automated fact-checking are usually organised by pipeline stage, and treat logic as one technique among many. We organise the field by what is being formalised instead, which gives five levels: the claim, the reasoning, the system doing the checking, the ecosystem the claim spreads through, and the regulatory obligation. Sorting 121 works into those levels, two patterns stand out. Most of the relevant formal machinery already exists, but it was built for other domains and has rarely been applied here, and the gap is widest for verifying the checking system itself. Several stages of the routine professional fact-checkers follow also have no stated correctness criterion, and two of them, writing a claim in checkable form and correcting a verdict already published, are not formally specified in any work we coded. We close with open problems, each with a suggested first step.
