5 citations · 7 across the 8 of their papers we have counts for
13 papers
Partial Label Learning for Automated Theorem Proving
Zsolt Zombori, Balázs Indruck
We formulate learning guided Automated Theorem Proving as Partial Label Learning, building the first bridge across these fields of research and providing a theoretical framework fo…
Mathematical Knowledge Bases as Grammar-Compressed Proof Terms: Exploring Metamath Proof Structures
Christoph Wernhard, Zsolt Zombori
Viewing formal mathematical proofs as logical terms provides a powerful and elegant basis for analyzing how human experts tend to structure proofs and how proofs can be structured…
Do Attention Heads Compete or Cooperate during Counting?
Pál Zsámboki, Ádám Fraknói, Máté Gedeon +2
We present an in-depth mechanistic interpretability analysis of training small transformers on an elementary task, counting, which is a crucial deductive step in many algorithms. I…
Towards Unbiased Exploration in Partial Label Learning
Zsolt Zombori, Agapi Rissaki, Kristóf Szabó +2
We consider learning a probabilistic classifier from partially-labelled supervision (inputs denoted with multiple possibilities) using standard neural architectures with a softmax…
Safety without alignment
András Kornai, Michael Bukatin, Zsolt Zombori
Currently, the dominant paradigm in AI safety is alignment with human values. Here we describe progress on developing an alternative approach to safety, based on ethical rationalis…
Lemmas: Generation, Selection, Application
Michael Rawson, Christoph Wernhard, Zsolt Zombori +1
Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combin…
Towards solving the 7-in-a-row game
Domonkos Czifra, Endre Csóka, Zsolt Zombori +1
Our paper explores the game theoretic value of the 7-in-a-row game. We reduce the problem to solving a finite board game, which we target using Proof Number Search. We present a nu…
The Role of Entropy in Guiding a Connection Prover
Zsolt Zombori, Josef Urban, Miroslav Olšák
In this work we study how to learn good algorithms for selecting reasoning steps in theorem proving. We explore this in the connection tableau calculus implemented by leanCoP where…
Data-dependent Pruning to find the Winning Lottery Ticket
Dániel Lévai, Zsolt Zombori
The Lottery Ticket Hypothesis postulates that a freshly initialized neural network contains a small subnetwork that can be trained in isolation to achieve similar performance as th…
Prolog Technology Reinforcement Learning Prover
Zsolt Zombori, Josef Urban, Chad E. Brown
We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to exte…
Towards Finding Longer Proofs
Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski +2
We present a reinforcement learning (RL) based guidance system for automated theorem proving geared towards Finding Longer Proofs (FLoP). Unlike most learning based approaches, we…
Gradient Regularization Improves Accuracy of Discriminative Models
Dániel Varga, Adrián Csiszárik, Zsolt Zombori
Regularizing the gradient norm of the output of a neural network with respect to its inputs is a powerful technique, rediscovered several times. This paper presents evidence that g…
Using Constraint Handling Rules to Provide Static Type Analysis for the Q Functional Language
János Csorba, Zsolt Zombori, Péter Szeredi
We describe an application of Prolog: a type checking tool for the Q functional language. Q is a terse vector processing language, a descendant of APL, which is getting more and mo…