Observation to prompt
VacuumWorld agent percepts are serialised into a prompt under one of four scaffolding conditions, holding everything else fixed.
Research & experience
Measuring what a model actually learned
Autoformalization, symbolic evaluation, and the engineering that keeps an experiment honest. Jun 2026 – present, DICE Lab, Royal Holloway.
Current project
LLM autoformalization in VacuumWorld
Funded UROP fellowship · Prof. Kostas Stathis & Dr. Agnieszka Mensfelt · selected from 30+ applicants.
The task is to turn what an agent can see into a Prolog knowledge base. The research question is whether the model wrote a rule or a lookup table.
A boundary wall in a grid world can be described two ways. One is a general rule — a wall exists wherever a coordinate sits on the edge. The other is a list of every wall cell the model happened to be shown. Both score identically on a small grid, and only one of them is knowledge. Separating the two is the whole problem, and it is an evaluation problem before it is a modelling one.
Nine models were run across four prompt conditions — zero-shot, instruction, schema, and one-shot — with a composition table designed so that every scaffolding factor appears as a single-variable contrast rather than a bundle of changes. Outputs are scored by a nine-constraint symbolic evaluator, and an F1-vs-N grid-size sweep exposes enumeration that only looks correct while N stays small.
- Finding · capability × scaffolding The two interact rather than add. Model tier sets the ceiling on abstraction; scaffolding decides whether a model climbs to it. Better prompting cannot lift a weak model past its ceiling, and a strong model left unscaffolded will sit well below its own.
- Finding · frontier outlier DeepSeek-V3 does not fit the pattern its tier predicts: partial hardcoding persists across all four conditions instead of clearing up under stronger scaffolding.
- Correction · evaluator bug A bug in the evaluator was silently zeroing scores on exactly the rule-based outputs the study was designed to reward. Diagnosing and patching it changed the headline result.
- Correction · prompt confound One condition varied two things at once, which would have credited the wrong factor. Documented and corrected in the condition design.
Method
How the harness works
Prolog knowledge base
The model returns a knowledge base. Nothing about its phrasing is trusted: the artefact is what gets judged, not the explanation around it.
Nine-constraint evaluator
A symbolic evaluator checks nine constraints on the output. Symbolic, not textual, so a correct rule written unusually still scores as correct.
F1 against grid size
Sweeping N upward is what separates induction from enumeration. A real rule holds its F1; a lookup table decays as the grid grows.
Positions
Where I have worked
Society roles and awards are on the about page.
-
Jun 2026 – present
Undergraduate Research Fellow UROP · funded
DICE Lab, Royal Holloway — Prof. Kostas Stathis & Dr. Agnieszka Mensfelt
- Selected as one of eight fellows from a field of more than thirty applicants.
- Investigating LLM autoformalization: translating VacuumWorld agent percepts into Prolog knowledge bases, and measuring whether models induce general boundary-wall rules or hardcode enumerated facts.
- Designed and ran a nine-model × four-prompt-condition sweep with a composition table isolating each scaffolding factor as a single-variable contrast.
- Built a nine-constraint symbolic evaluator and an F1-vs-N grid-size sweep to separate true rule induction from enumeration that only appears correct at small N.
- Diagnosed and patched an evaluator bug silently zeroing scores on rule-based outputs, and documented a prompt confound in the condition design — both corrected the headline results.
-
2026
Research Software Contributor
DICE Lab Autoformalization Paper Catalogue, Royal Holloway
- Built dataset filters and CI/CD pipelines in TypeScript for the lab's public catalogue of autoformalization literature.
- The filters are used to triage papers for ongoing survey work.
DICE Lab autoformalization paper catalogue -
2026 – present
Early Engineer
Sharper Future Ltd — remote, UK
- Early technical hire shipping production features across the stack with LLM APIs and evaluation tooling.
- Contract includes an IP carve-out preserving independent university research.
Outputs
Writing it up
Status is stated plainly: targeted means submission intended, not accepted.
In preparation
Full technical report
Complete write-up of the sweep: method, composition table, evaluator design, and the F1-vs-N results.
Targeted
Interpretability workshop
Submission targeted at the NeurIPS interpretability workshop track.
Targeted
Student Abstract track
Short-form submission targeted at the AAAI Student Abstract track.
Collaboration
Looking for Summer 2027 research internships
Interpretability, neurosymbolic reasoning, and evaluation design. Happy to talk through the method in detail, including the parts that went wrong first.