Viewing profile — barthelomew

Yes, indeed! This work uses the Proof of Thought library and several techniques from VERGE!

AI (VLM-based) radiology models can sound confident and still be wrong ; hallucinating diagnoses that their own findings don't support. This is a silent, and dangerous failure mode…

Predict your distributed LLM training time before you burn GPU hours. We've open-sourced a tool ( https://github.com/DebarghaG/estimate-train-time ) that estimates wall-clock time …

You can get bonuses though. The optimization algorithms do not get bonuses.

Paper LaTeX files often contain surprising details. When a paper lacks code, looking at latex source has become a part of my reproduction workflow. The comments often reveal non-tr…

Yep! Datalog syntax for Z3 is pretty neat! We used SMT [1] in our grammars paper because it allowed the most interoperability with solvers, but our technique also works with PROLOG…

Hey! Thank you for the interest! I shall do that. Meanwhile, check out Page 11 onwards. We describe a lot of situations! ( https://arxiv.org/pdf/2409.17270 )

You're right about the 2023 JSON mode, but our project required enforcing a much more complex DSL grammar (look in Appendix for details), not just ensuring a *valid JSON object*. T…

Yep, this is a genuine problem, and this is what we term as the autoformalization gap in our follow up paper. ( https://arxiv.org/abs/2505.20047 ) Some LLMs are more consistent bet…

Yep. The paper was written last year with GPT-4o. Things have become a lot better since then with newer models. E.g. https://arxiv.org/pdf/2505.20047 Tab 1, we compare the performa…

Hey, yes! This is because the DSL (Domain Specific Language) is pretty complex, and the LLM finds it hard. We prototype a much more effective version using SMT in our NeurIPS 2025 …

Hey there! I mostly designed and wrote most of the actual interpreter during my internship at Microsoft Research last summer. Constrained decoding for GPT-4 wasn’t available when w…

Yep! I have read your work! Pretty cool! I also worked on a similar deep research agent for autoformalization this summer at AWS ARChecks, building on similar patterns. Although th…

The autoformalization gap is pretty difficult to bridge indeed. We explored uncertainty quantification of autoformalization on well-defined grammars in our NeurIPS 2025 paper : htt…

https://arxiv.org/abs/2409.17270