Мне не нравится любой подход, который начинается с того, что conjecture приводится к conjunctive normal form. Люди так не доказывают теоремы.

>не получится применить обычное машинное обучение т.к. мы не имеем тут дело с дифференцируемыми функциями
Нет, я ошибался. Можно использовать graph neural networks, а логическое высказывание представляется в виде дерева.

Точнее не в виде дерева, а в виде DAG.

@632e9@632e96c06ea648dcba4b59ef7f9ca489 Мне это не нравится также потому, что cnf не существует в интуиционистской логике. А меня интересует именно она, потому что мне нужны конструктивные доказательства существования.

>1. подавляющее большинство существующих доказательств не записаны на формальном языке. И автоматически перевести их в формальный язык - это очень сложная задача.

Нужно синтезировать теоремы и их пруфы. Обучение через self-play. Adversarial подход.

https://arxiv.org/pdf/2002.07019.pdf
Learning to Prove Theorems by Learning to Generate Theorems
Abstract
We consider the task of automated theorem proving, a key AI task. Deep learning
has shown promise for training theorem provers, but there are limited humanwritten theorems and proofs available for supervised learning. To address this
limitation, we propose to learn a neural generator that automatically synthesizes
theorems and proofs for the purpose of training a theorem prover. Experiments on
real-world tasks demonstrate that synthetic data from our approach improves the
theorem prover and advances the state of the art of automated theorem proving in
Metamath. Code is available at https://github.com/princeton-vl/MetaGen.

https://arxiv.org/abs/1904.03241 HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
https://sites.google.com/view/holist/home

Reinforcement Learning. Training does not use any human proofs.
https://arxiv.org/abs/1905.10501 Learning to Reason in Large Theories without Imitation
Abstract
In this paper, we demonstrate how to do automated theorem proving in the presence of a large knowledge base of potential premises without learning from human proofs. We suggest an exploration mechanism that mixes in additional premises selected by a tf-idf (term frequency-inverse document frequency) based lookup in a deep reinforcement learning scenario. This helps with exploring and learning which premises are relevant for proving a new theorem. Our experiments show that the theorem prover trained with this exploration mechanism outperforms provers that are trained only on human proofs. It approaches the performance of a prover trained by a combination of imitation and reinforcement learning. We perform multiple experiments to understand the importance of the underlying assumptions that make our exploration approach work, thus explaining our design choices.

https://github.com/tensorflow/deepmath/tree/master/deepmath/deephol DeepHol source code
https://github.com/tensorflow/deepmath The Deepmath project seeks to improve automated theorem proving using deep learning and other machine learning techniques. Deepmath is a collaboration between Google Research and several universities.

Но эта работа @4e1f8@4e1f8fcc7271482d9e192cf0dc3c18ac обисрает эту @4e25d@4e25db0760ab401e8a5edee234802712
Вот цитата из https://arxiv.org/pdf/2002.07019.pdf
>Kaliszyk et al. (2018); Bansal et al. (2019a,b); Balunovic et al. (2018) use reinforcement learning
>to train provers with only human-written theorems or SMT conjectures but not proofs. During
>training, a prover collects rewards only upon finding full proofs. In contrast, we always train our
>prover using imitation learning. Under the same setting with only human-written theorems but not
>proofs, we use reinforcement learning to train our generator, whose reward is the similarity between
>a generated theorem and human-written theorems, as measured by an adversarial discriminator. Our
>reinforcement learning task is much easier because the reward is continuous and there are many ways
>to generate theorems similar to human-written ones.
Выглядит убедительно. Мне этот подход больше нравится.

https://github.com/dwhalen/holophrasm Holophrasm: a purely neural automated theorem prover for Metamath
https://arxiv.org/pdf/1608.02644.pdf
Holophrasm: a neural Automated Theorem Prover for higher-order logic. 2016
Abstract
I propose a system for Automated Theorem Proving in higher order logic using deep learning and eschewing hand-constructed features. Holophrasm exploits
the formalism of the Metamath language and explores partial proof trees using
a neural-network-augmented bandit algorithm and a sequence-to-sequence model
for action enumeration. The system proves 14% of its test theorems from Metamath’s set.mm module.

https://arxiv.org/abs/1606.04442 DeepMath - Deep Sequence Models for Premise Selection 2016
Abstract
We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving on a large scale.

Перспективный подход: одна нейросеть синтезирует теоремы, вторая их доказывает. Реворд для первой - найти теорему, которую не может доказать вторая сеть. Реворд для второй - найти доказательство.

@4e1f8@4e1f8fcc7271482d9e192cf0dc3c18ac
Тут не такой подход:
> Also of note is that we have no adversarial self-play. The goal of the generator is to discover novel theorems similar to human-written ones, not to beat the prover.
Автор гипотезирует, что синтезированные теоремы должны быть похожи на человеческие - на таких прувер будет лучше обучаться.
С хуя ли - непонятно. Я так не считаю.

https://www.cs.ru.nl/~freek/100/ "Formalizing 100 Theorems" challenge.
HOL Light привлекательно выглядит. https://en.wikipedia.org/wiki/HOL_Light - простая и понятная система. Отпугивает использование богомерзкого OCaml.

https://arxiv.org/abs/2006.11259 Learning to Prove from Synthetic Theorems 2020
Abstract
A major challenge in applying machine learning to automated theorem proving is the scarcity of training data, which is a key ingredient in training successful deep learning models. To tackle this problem, we propose an approach that relies on training with synthetic theorems, generated from a set of axioms. We show that such theorems can be used to train an automated prover and that the learned prover transfers successfully to human-generated theorems. We demonstrate that a prover trained exclusively on synthetic theorems can solve a substantial fraction of problems in TPTP, a benchmark dataset that is used to compare state-of-the-art heuristic provers. Our approach outperforms a model trained on human-generated problems in most axiom sets, thereby showing the promise of using synthetic data for this task.

https://kwarc.info/teaching/CICM21WS/dp3.pdf Deep Learning for Automated Theorem Proving 2021
Abstract
The field of Artificial Intelligence has seen great advances with the use of Deep Neural Networks.
However, the problem of creating a system capable of abstract reasoning remains unsolved. One way to
force AI to perform abstract reasoning is to directly learn an abstract task – such as Automated Theorem
Proving. In ATP, the goal is to construct a formal proof of a mathematical statement. This requires
finding a correct sequence of inferences in an exponentially large space of possibilities. This search can
be guided by a Deep Neural Network. Towards this end, I have worked on creating a neural architecture
that would work well with mathematical formulas and providing a way to generate training data to train
such neural networks.

https://en.wikipedia.org/wiki/Sequent_calculus мне этот стиль больше нравится чем гильбертовский. Лучше его использовать.

>1. подавляющее большинство существующих доказательств не записаны на формальном языке. И автоматически перевести их в формальный язык - это очень сложная задача.

Возможно не такая и сложная.
https://arxiv.org/abs/2205.12615
Abstract
Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence. While the long-term goal of autoformalization seemed elusive for a long time, we show large language models provide new prospects towards this goal. We make the surprising observation that LLMs can correctly translate a significant portion (25.3%) of mathematical competition problems perfectly to formal specifications in Isabelle/HOL. We demonstrate the usefulness of this process by improving a previously introduced neural theorem prover via training on these autoformalized theorems. Our methodology results in a new state-of-the-art result on the MiniF2F theorem proving benchmark, improving the proof rate from 29.6% to 35.2%.

> 3. даже если бы у нас был огромный трейнинг сет из пар (теорема, доказательство), не получится применить обычное машинное обучение т.к. мы не имеем тут дело с дифференцируемыми функциями и поэтому backpropagation не будет работать.

Это неверно. Нейросеть выдаёт ответ в виде вероятностного распределения токенов. Кросс энтропия от распределения и ground truth дифференцируема. В этом плане нет отличия от обычного NLP.

Вижу очень перспективной идею взять LLM и прикрутить к ней формальную систему для обратной связи посредством ответов про генерённые доказательства "правильно/неправильно". У LLM есть интуиция и интерпретация действий, а у формальной системы точность.

@03ab9@03ab9aa1c90a4be183de3d935ff7b6fe
>Нейросеть выдаёт ответ в виде вероятностного распределения токенов. Кросс энтропия от распределения и ground truth дифференцируема. В этом плане нет отличия от обычного NLP.
Возможно.

>Вижу очень перспективной идею взять LLM и прикрутить к ней формальную систему для обратной связи посредством ответов про генерённые доказательства "правильно/неправильно". У LLM есть интуиция и интерпретация действий, а у формальной системы точность.
Да, это интересно. И данных для трейнинга сколько угодно можно нагенерить.

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
Вот как они решили первую проблему из ОП:
>We established a bridge between these two complementary spheres by fine-tuning a Gemini model to automatically translate natural language problem statements into formal statements, creating a large library of formal problems of varying difficulty.
Прикольно. Т.е. LLM чисто для формализации пруфов используется. Ну и правильно, сами математические проблемы оно не вывезет решать.
>Around one million informal math problems are translated into a formal math language by a formalizer network. Then a solver network searches for proofs or disproofs of the problems, progressively training itself via the AlphaZero algorithm to solve more challenging problems.

@131ea@131ead6ca0e64ac595a3887b5bb4f4f3 Тао рассказывал, что для искусственного интеллекта требуется совершенно другой подход и даже не понятно, как к нему подступиться. Но имеющиеся инструменты хорошо сочетаются с системами автоматического доказательства теорем.

Ебать, смогли https://deepmind.google/discover/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/ Вот это круто.

@919ea@919ea8dced7b45899b6180a8bc6e2592 окей, убедили