Papers by Jordan Meadows
FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean (2026.acl-long)
Copied to clipboard
| Challenge: | Formalising informal mathematical reasoning into formally verifiable code is a significant challenge for large language models. |
| Approach: | They propose a domain-agnostic human-in-the-loop agentic pipeline to aid autoformalisation in scientific domains. |
| Outcome: | The proposed system produces syntactically correct and semantically aligned proofs for low cost. |
Exploring the Limits of Fine-grained LLM-based Physics Inference via Premise Removal Interventions (2024.findings-emnlp)
Copied to clipboard
| Challenge: | Language models (LMs) perform complex mathematical reasoning in Physics where physical context requires that any symbolic manipulation satisfies complex semantics. |
| Approach: | They systematically remove crucial context from prompts to force instances where model inference may be algebraically coherent, yet unphysical. |
| Outcome: | The proposed models perform poorly in this domain, and their reasoning is not physics-informed. |
PhysNLU: A Language Resource for Evaluating Natural Language Understanding and Explanation Coherence in Physics (2022.lrec-1)
Copied to clipboard
| Challenge: | physicists use mathematics to reason and explain, separates their field from other disciplines, including mathematics. |
| Approach: | They present a dataset to evaluate the performance of language models in physics . they find that language models are challenged by coherence related tasks in physicists . |
| Outcome: | The proposed models are able to perform well on coherence-related tasks even when trained on natural language objectives. |
Introduction to Mathematical Language Processing: Informal Proofs, Word Problems, and Supporting Tasks (2023.tacl-1)
Copied to clipboard
| Challenge: | Using mathematical language processing methods, we analyze prevailing methods, existing limitations, and promising avenues for future research. |
| Approach: | They analyze mathematical language processing methods from recent years and highlight prevailing methodologies, existing limitations and promising avenues for future research. |
| Outcome: | The proposed methods highlight prevailing methods, existing limitations and promising avenues for future research. |
Multi-Operational Mathematical Derivations in Latent Space (2024.naacl-long)
Copied to clipboard
| Challenge: | Using a symbolic engine, we investigate the possibility of approximating multiple mathematical operations in latent space for expression derivation. |
| Approach: | They propose to model mathematical operations as explicit geometric transformations by leveraging a symbolic engine and a large-scale dataset. |
| Outcome: | The proposed paradigms can be used to approximate multiple mathematical operations in latent space, while discriminating the conclusions for a single operation is achievable in the original expression encoder. |
A Symbolic Framework for Evaluating Mathematical Reasoning and Generalisation with Transformers (2024.naacl-long)
Copied to clipboard
| Challenge: | evaluating the generalisability of Transformers to out-of-distribution mathematical reasoning problems is a challenge for many open-source models. |
| Approach: | They propose a method for generating and perturbing detailed derivations of equations at scale, aided by a symbolic engine, and compare their results to sequence classification tasks. |
| Outcome: | The proposed framework outperforms GPT-4, GPT-3.5 and a canon of fine-tuned BERT models in classification tasks . perturbations to input reasoning can reduce their performance by up to 80 F1 points . |