barthelomew

6 ms·

1.
Guardrail Your Agents with Lean(github.com)
5 points by barthelomew 7d ago|0 comments
2.
Labeling Copilot: An agent for automated data curation in computer vision(github.com)
5 points by barthelomew 5mo ago|0 comments
3.
by barthelomew 7mo ago
Yes, indeed! This work uses the Proof of Thought library and several techniques from VERGE!
4.
Toward Guarantees for Clinical Reasoning in Vision Language Models(arxiv.org)
5 points by barthelomew 7mo ago|3 comments
5.
by barthelomew 7mo ago
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. Our new paper introduces a verification layer that ch
6.
SoTA LLM Guardrails by Trusting the Typical [ICLR 2026](arxiv.org)
1 points by barthelomew 7mo ago|0 comments
7.
Predict your distributed LLM training time before you burn GPU hours(github.com)
2 points by barthelomew 8mo ago|1 comments
8.
by barthelomew 8mo ago
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 for LLM training across multi-GPU s
9.
Uncertainty Quantification for Auto Formalization [NeurIPS 2025](github.com)
1 points by barthelomew 10mo ago|0 comments
10.
Race optimization algorithms with good initializations (beat them with bonuses)(debargha.com)
8 points by barthelomew 10mo ago|8 comments
11.
by barthelomew 10mo ago
You can get bonuses though. The optimization algorithms do not get bonuses.
12.
by barthelomew 11mo ago
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-trivial insights. Often, they reveal a simpler version of the
13.
by barthelomew 1y ago
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; as tested our at the behest of reviewers at NeurIPS. I wou
14.
by barthelomew 1y ago
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 )
15.
by barthelomew 1y ago
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*. The newer structured output APIs are a significant impro
16.
by barthelomew 1y ago
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 between text and SMT, while others are not.
17.
by barthelomew 1y ago
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 performance on text-only vs SMT-only. o3-mini
18.
by barthelomew 1y ago
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 paper ( https://arxiv.org/abs/2505.20047
19.
by barthelomew 1y ago
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 we started designing the DSL, and besides, creating a regex t
20.
by barthelomew 1y ago
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 that work is not public, you can play with the generally avail
21.
by barthelomew 1y ago
The autoformalization gap is pretty difficult to bridge indeed. We explored uncertainty quantification of autoformalization on well-defined grammars in our NeurIPS 2025 paper : https://arxiv.org/abs/2505.20047 . If you
22.
ProofOfThought: LLM-based reasoning using Z3 theorem proving(github.com)
326 points by barthelomew 1y ago|175 comments
23.
A Deep Research Agent for Curating Vision Datasets(arxiv.org)
12 points by barthelomew 1y ago|0 comments
24.
Provably guarantee correctness of (some of) your LLM outputs(aws.amazon.com)
3 points by barthelomew 1y ago|0 comments
25.
K^4: Online Log Anomaly Detection via Unsupervised Typicality Learning(arxiv.org)
3 points by barthelomew 1y ago|1 comments
26.
Grammars of Formal Uncertainty(arxiv.org)
34 points by barthelomew 1y ago|5 comments
27.
Show HN: Drop-In Out-of-Distribution Data Detector(github.com)
4 points by barthelomew 2y ago|0 comments
28.
Proof of Thought: Neurosymbolic Program Synthesis for Interpretable Reasoning(arxiv.org)
4 points by barthelomew 2y ago|1 comments
29.
by barthelomew 2y ago
Large Language Models (LLMs) have revolutionized natural language processing, yet they struggle with inconsistent reasoning, particularly in novel domains and complex logical sequences. This research introduces Proof of Thought, a framework
30.
by barthelomew 3y ago
Yes, it does seem like it's concept stage.

More ›