Based on the already known connection between multilayer perceptrons and Lukasiewicz logic with rational coefficients, we take a step forward in analyzing its training process using a three-sorted hybrid modal logic: a multilayer perceptron is a logical formula; the actions of the training process are modal operators; the training process is a sequence of logical deductions. Using the proof assistant and the programming language Lean 4, the algorithmic implementation of the training process is certified by logical proofs.

翻译：基于多层感知机与带有理系数的Łukasiewicz逻辑之间已有的联系，本文进一步采用一种三类别混合模态逻辑来分析其训练过程：将多层感知机视为逻辑公式；将训练过程中的操作视为模态算子；将训练过程视为一系列逻辑推导。借助证明辅助工具及编程语言Lean 4，训练过程的算法实现通过逻辑证明得到形式化验证。