Martin Fixman

I work on automated theorem proving, mostly connection tableaux, and on ways of using machine learning without turning the prover into an inscrutable black box.

I am supervised by Dr Sean B. Holden. My first-year work asks when a SAT-aware prover should keep searching, when it should start again, and what it should remember from failed attempts. Longer term, I want to know whether better first-order search can help larger verification and formal-mathematics workflows.

Research and code

SATResetCoP

(current project)

SATResetCoP combines tableau search with an incremental SAT solver. When a tableau becomes unproductive, it starts again but retains the ground clauses accumulated so far, allowing failed attempts to contribute to a later contradiction.

In our experiments it produced a substantial improvement over both leanCoP-style and SATCoP-style baselines, including a strong showing on the bushier problems in MPTP2078. It also competed in CASC-J13, where it achieved a respectable, decidedly not-bad placing. Paper · code

A SATResetCoP run: clauses found in separate tableau attempts accumulate in the persistent SAT ground until they yield a contradiction.

PALMS

PALMS is a Python environment for specifying Pavlovian conditioning experiments and comparing classical and attentional learning models. It supports complex designs, configural cues, visualisation, and data export.

Paper · source code

PALMS running a multi-phase experiment and plotting the predictions of an associative-learning model.

Knowledge grounding in language models

My MSc dissertation tested whether language models follow retrieved evidence when it conflicts with memorised knowledge. Experiments and code.

Socioeconomic inference in communication graphs

At Grandata and the University of Buenos Aires, I used communication graphs and financial data to infer socioeconomic attributes. Bayesian method · feature comparison · code.

Industry experience

2017–2021

Meta / Facebook

Software Engineer, Abusive Accounts Detection

I built adversarial machine-learning systems for detecting fake accounts on Facebook and Instagram, including automated ground-truth signals and an account-confirmation classifier.

2021–2023

Monzo

Backend Engineer, Financial Crime Decisioning

I worked on financial-crime decisioning and the production lifecycle of customer-risk models.

2013–2017

Grandata Labs

Research Engineer, network science and data science

I researched demographic and mobility inference from large communication datasets. The work became my undergraduate thesis and first papers.

Earlier on, I interned at Google, working on profile-guided reordering of Windows executables for Chrome, and at Facebook, where I worked on Android performance and News Feed tooling.

Education

2025–present

University of Cambridge

PhD in Computer Science

Supervised by Dr Sean B. Holden. My first-year report, Fast Heuristics and Strategies for Automated Theorem Proving of First-Order Problems, studies search control in SAT-aware connection provers and uses SATResetCoP as the starting point for broader work on adaptive proof search.

2023–2024

City St George's, University of London

MSc in Artificial Intelligence · Distinction, 82.51% average

Dissertation: Knowledge Grounding in Large Language Models.

2011–2018

University of Buenos Aires

Licenciatura en Ciencias de la Computación

An integrated degree in Computer Science, with electives in artificial intelligence and formal logic. My thesis was Methods for Inference of Socioeconomic Status in a Communications Graph.

I won a silver medal at the 2010 International Olympiad in Informatics and represented the University of Buenos Aires at the 2013 ICPC World Finals. These competitions taught me to enjoy difficult search problems long before I began calling them research.

Selected papers

Reset Early, Reset Often, Eliminate Models Martin Fixman, Fredrik Rømming, and Sean B. Holden. Vampire Workshop, FLoC 2026. abstract · code
PALMS: A Computational Implementation for Pavlovian Associative Learning Models' Simulation Martin Fixman, Alessandro Abati, Julián Jiménez Nimmo, Sean Lim, and Esther Mondragón. arXiv preprint, 2026. arXiv · code
Comparison of Feature Extraction Methods and Predictors for Income Inference Martin Fixman, Martin Minnoni, and Carlos Sarraute. Argentine Symposium on Big Data (AGRANDA), 46 JAIIO, 2017. arXiv
A Bayesian Approach to Income Inference in a Communication Network Martin Fixman, Ariel Berenstein, Jorge Brea, Martin Minnoni, Matias Travizano, and Carlos Sarraute. IEEE/ACM International Conference on Advances in Social Networks Analysis and Mining (ASONAM), 2016. DOI · arXiv

Elsewhere

GitHub · LinkedIn · Cambridge talks I follow

If you would like to talk about automated reasoning, SAT-assisted proof search, machine learning for theorem proving, or an unusually stubborn benchmark, please get in touch.