- PhD Student
Skip to content
Martin Fixman
PhD student in Computer Science · University of Cambridge
github.com/mfixman
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.
First-year result: SATResetCoP, a prover in which failed or unfinished tableau attempts can still leave useful ground information behind.
ML and AI · PLS and Verification
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
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.
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
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.
Monzo
Backend Engineer, Financial Crime Decisioning
I worked on financial-crime decisioning and the production lifecycle of customer-risk models.
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
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.
City St George's, University of London
MSc in Artificial Intelligence · Distinction, 82.51% average
Dissertation: Knowledge Grounding in Large Language Models.
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
abstract · code -
PALMS: A Computational Implementation for Pavlovian Associative Learning Models' Simulation
arXiv · code -
Comparison of Feature Extraction Methods and Predictors for Income Inference
arXiv -
A Bayesian Approach to Income Inference in a Communication Network
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.
