The ever-growing complexity of mathematical proofs makes their manual
verification by mathematicians very cognitively demanding. Autoformalization
seeks to address this by translating proofs written in natural language into a
formal representation that is computer-verifiable via interactive theorem
provers. In this paper, we introduce a semantic parsing approach, based on the
Universal Transformer architecture, that translates elementary mathematical
proofs into an equivalent formalization in the language of the Coq interactive
theorem prover. The same architecture is also trained to translate simple
imperative code decorated with Hoare triples into formally verifiable proofs of
correctness in Coq. Experiments on a limited domain of artificial and
human-written proofs show that the models generalize well to intermediate
lengths not seen during training and variations in natural language.

本研究介绍了一种基于 Universal Transformer 体系结构的语义解析方法，可以将基本数学证明转化为 Coq 互动定理证明器中的等效形式，以及将装饰有 Hoare 三元组的简单命令式代码翻译成 Coq 中的形式验证证明。通过人工和人工写作证明的有限领域的实验表明，这些模型对于训练期间未看到的中间长度和自然语言变化具有很好的泛化能力。

基于自动正式化的数学和代码正确性研究：基础证明实验

Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs

This paper describes SEPIA, a tool for automated proof generation in Coq.
SEPIA combines model inference with interactive theorem proving. Existing proof
corpora are modelled using state-based models inferred from tactic sequences.
These can then be traversed automatically to identify proofs. The SEPIA system
is described and its performance evaluated on three Coq datasets. Our results
show that SEPIA provides a useful complement to existing automated tactics in
Coq.

SEPIA 为 Coq 提供了自动化证明的新工具，它将模型推断与交互式定理证明相结合，使用状态模型从策略序列中推断证明，经评估发现 SEPIA 在三个 Coq 数据集上的表现可作为现有自动化策略的有用补充。

使用推断自动机搜索证明的 SEPIA

SEPIA: Search for Proofs Using Inferred Automata

We present ML4PG - a machine learning extension for Proof General. It allows
users to gather proof statistics related to shapes of goals, sequences of
applied tactics, and proof tree structures from the libraries of interactive
higher-order proofs written in Coq and SSReflect. The gathered data is
clustered using the state-of-the-art machine learning algorithms available in
MATLAB and Weka. ML4PG provides automated interfacing between Proof General and
MATLAB/Weka. The results of clustering are used by ML4PG to provide proof hints
in the process of interactive proof development.

ML4PG 是 Proof General 的机器学习扩展，允许用户从 Coq 和 SSReflect 互动高阶证明库中收集与目标形状、应用策略序列和证明树结构相关的证明统计数据，并使用 MATLAB 和 Weka 中的最先进的机器学习算法对其进行聚类，提供证明提示。

Proof General 中的机器学习：接口交互

Machine Learning in Proof General: Interfacing Interfaces

The use of formal methods provides confidence in the correctness of
developments. Yet one may argue about the actual level of confidence obtained
when the method itself -- or its implementation -- is not formally checked. We
address this question for the B, a widely used formal method that allows for
the derivation of correct programs from specifications. Through a deep
embedding of the B logic in Coq, we check the B theory but also implement B
tools. Both aspects are illustrated by the description of a proved prover for
the B logic.

使用 Coq 深度嵌入 B 逻辑以检查其正确性和实现 B 工具，实现了 B 逻辑的证明器。