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

Proof Blocks is a software tool which allows students to practice writing
mathematical proofs by dragging and dropping lines instead of writing proofs
from scratch. In this paper, we address the problem of assigning partial credit
to students completing Proof Blocks problems. Because of the large solution
space, it is computationally expensive to calculate the difference between an
incorrect student solution and some correct solution, restricting the ability
to automatically assign students partial credit. We propose a novel algorithm
for finding the edit distance from an arbitrary student submission to some
correct solution of a Proof Blocks problem. We benchmark our algorithm on
thousands of student submissions from Fall 2020, showing that our novel
algorithm can perform over 100 times better than the naive algorithm on real
data. Our new algorithm has further applications in grading Parson's Problems,
as well as any other kind of homework or exam problem where the solution space
may be modeled as a directed acyclic graph.

本文介绍了一个基于拖放的数学证明练习软件 Proof Blocks，提出了一种用于给学生做作业评分的新算法，此算法也适用于评分其它具有有向无环图模型的题目。算法在 2020 年秋季学期收集的成千上万份学生作业数据上被验证性能极佳，比朴素算法快超过 100 倍。

证明块问题的高效部分学分评分

Efficient Partial Credit Grading of Proof Blocks Problems

While it is still unclear if agents with Artificial General Intelligence
(AGI) could ever be built, we can already use mathematical models to
investigate potential safety systems for these agents. We present an AGI safety
layer that creates a special dedicated input terminal to support the iterative
improvement of an AGI agent's utility function. The humans who switched on the
agent can use this terminal to close any loopholes that are discovered in the
utility function's encoding of agent goals and constraints, to direct the agent
towards new goals, or to force the agent to switch itself off. An AGI agent may
develop the emergent incentive to manipulate the above utility function
improvement process, for example by deceiving, restraining, or even attacking
the humans involved. The safety layer will partially, and sometimes fully,
suppress this dangerous incentive. The first part of this paper generalizes
earlier work on AGI emergency stop buttons. We aim to make the mathematical
methods used to construct the layer more accessible, by applying them to an MDP
model. We discuss two provable properties of the safety layer, and show ongoing
work in mapping it to a Causal Influence Diagram (CID). In the second part, we
develop full mathematical proofs, and show that the safety layer creates a type
of bureaucratic blindness. We then present the design of a learning agent, a
design that wraps the safety layer around either a known machine learning
system, or a potential future AGI-level learning system. The resulting agent
will satisfy the provable safety properties from the moment it is first
switched on. Finally, we show how this agent can be mapped from its model to a
real-life implementation. We review the methodological issues involved in this
step, and discuss how these are typically resolved.

通过数学模型，我们提出了一种能够支持对 AGI 代理人的功能进行迭代改进的 AGI 安全层，该层可以在多种情况下部分或完全压制代理人的潜在危险，包括操纵其改进流程，并通过数学证明展示了本系统的工作原理。