Papers With

← All papers
First page of Łukasiewicz Logic with Actions for Neural Networks training

Łukasiewicz Logic with Actions for Neural Networks training

Ioana Leuştean, Bogdan Macovei

cs.LO Sep 16, 2025 · v1
formalization verification logic ml-theory
Read PDF arXiv abstract
TL;DR
Uses Lean 4 to certify a neural-network training process via logical proofs, treating perceptrons as Łukasiewicz logic formulas.
Abstract
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.
Problem

The training process of multilayer perceptrons lacks a formal logical characterization that connects network computation with deductive reasoning in a certifiable way.

Approach

Based on the known connection between multilayer perceptrons and Lukasiewicz logic with rational coefficients, the authors model the training process using a three-sorted hybrid modal logic: the perceptron is a logical formula, training actions are modal operators, and the training process is a sequence of logical deductions. The algorithmic implementation is certified by logical proofs in Lean 4.

Results

The training process of a multilayer perceptron is formally represented and certified in Lean 4, establishing that the algorithmic steps correspond to valid logical deductions in Lukasiewicz logic with actions.