Tyler R. Josephson (atomslab.bsky.social)

@andrewwhite01 Reminds me of this gem: reddit.com/r/notebooklm/c…

During testing of our agents, someone said "Hello" and it spiraled and ran for 45 minutes trying to understand the meaning and history of the word hello. Great adversarial test for autonomous agents.

I had a great time! Thanks for your hospitality!

I'll be getting more videos up over the coming weeks. In the meantime, the code and slides from the whole course are here: github.com/ATOMSLab/LFSE2…

Interested in learning a new programming language that enables you to prove the code you've written is correct? I taught "Lean for Scientists and Engineers" in Summer 2024. Soon, we'll have all the lectures on YouTube! Here's the first one: youtube.com/watch?v=s9Dyiu…

@LNuzhna What is science if not chains of abstractions? The process of explaining the physical world in words and numbers is exactly why it’s so hard, and so rewarding.

@inigo_iribarren I teach from this free textbook in my course: clauswilke.com/dataviz/ Figure 2.5 is a nice illustration of how to present 5-dimensional data in a static 2D plot.

Hello beautiful community I am preparing a seminar about making nice scientific figures and graphs (because, apparently, work intrusion is my real passion). Do you have any good figures/graphs that I should show? I will obviously include the greatest figure of all time.

Full job descriptions are here: atomslab.github.io/join/ The ad says PhD projects; the Monte Carlo project is relevant for postdoc applicants, as well.

I'm excited to announce *two* funded positions in the ATOMS Lab! Come join us, as we develop computational methods for simulating water pollutants, and AI methods for evaluating scientific claims. We want to hire by Spring 2025; check it out and share with your network!

ATOMS lab (@trjosephson) at @UMBC is looking for #PhD students to start #spring 2025 #graduateschool Learn more at the ATOMS lab website atomslab.github.io #Chemicalengineering #AI #LLM #UMBCEngineering @trjosephson is attending #AICHE2024. Reach out if interested

Our department is hiring a TT faculty member! Come work with us! We'll also be AIChE if you want to connect. cbee.umbc.edu/facultysearch/

Slides for my recent talk on: "Reasoning with inference-time compute" wellecks.com/data/welleck20… Papers: - Lean-STaR: arxiv.org/abs/2407.10040 - Easy-to-hard: arxiv.org/abs/2403.09472 - Compute-optimal inference: arxiv.org/abs/2408.00724 - Meta-generation: arxiv.org/abs/2406.16838

The 24-25 ChemEng faculty list is heating up! Check out the current 33 tenure-track and 11 teaching-track faculty openings. #gid=1692417990" target="_blank" rel="nofollow noopener">docs.google.com/spreadsheets/d…

ok here's my full review of this paper. It's easy and short, you should just read it if you want to. arxiv.org/abs/2409.04109

a collection of set theorists who are so excited that they cannot contain themselves

We're halfway through the course! So far, we've introduced logic and proofs for scientists and engineers. This week we pivot to writing programs in Lean, before bringing everything together. It's not too late to register!

Check out this excellent video on proving the continuity of various functions using Lean 4. It's a fantastic introduction to Lean, and its tactic framework for proof automation. youtube.com/watch?v=BZjAgh…

@ejmaginn @OBIdient_MrB I enjoyed the poster!

Group member Barnabas (⁦⁦@OBIdient_MrB⁩ ) presents a lightening talk on his research focused on new refrigerant molecule discovery. #FOMMS2024

Interested in LLMs and Lean? Check out LLMLean, a tool for using LLMs to suggest proof steps and complete proofs in Lean: github.com/cmu-l3/llmlean Here's an example of using LLMLean with GPT-4o to solve problems from Mathematics in Lean:

Stoked to head to #FOMMS 2024! Really excited to connect with the molecular-simulation community @fommsconf

The question of whether LLMs can reason is, in many ways, the wrong question. The more interesting question is whether they are limited to memorization / interpolative retrieval, or whether they can adapt to novelty beyond what they know. (They can't, at least until you start doing active inference, or using them in a search loop, etc.) There are two distinct things you can call "reasoning", and no benchmark aside from ARC-AGI makes any attempt to distinguish between the two. First, there is memorizing & retrieving program templates to tackle known tasks, such as "solve ax+b=c" -- you probably memorized the "algorithm" for finding x when you were in school. LLMs *can* do this! In fact, this is *most* of what they do. However, they are notoriously bad at it, because their memorized programs are vector functions fitted to training data, that generalize via interpolation. This is a very suboptimal approach for representing any kind of discrete symbolic program. This is why LLMs on their own still struggle with digit addition, for instance -- they need to be trained on millions of examples of digit addition, but they only achieve ~70% accuracy on new numbers. This way of doing "reasoning" is not fundamentally different from purely memorizing the answers to a set of questions (e.g. 3x+5=2, 2x+3=6, etc.) -- it's just a higher order version of the same. It's still memorization and retrieval -- applied to templates rather than pointwise answers. The other way you can define reasoning is as the ability to *synthesize* new programs (from existing parts) in order to solve tasks you've never seen before. Like, solving ax+b=c without having ever learned to do it, while only knowing about addition, subtraction, multiplication and division. That's how you can adapt to novelty. LLMs *cannot* do this, at least not on their own. They can however be incorporated into a program search process capable of this kind of reasoning. This second definition is by far the more valuable form of reasoning. This is the difference between the smart kids in the back of the class that aren't paying attention but ace tests by improvisation, and the studious kids that spend their time doing homework and get medium-good grades, but are actually complete idiots that can't deviate one bit from what they've memorized. Which one would you hire? LLMs cannot do this because they are very much limited to retrieval of memorized programs. They're static program stores. However, can display some amount of adaptability, because not only are the stored programs capable of generalization via interpolation, the *program store itself* is interpolative: you can interpolate between programs, or otherwise "move around" in continuous program space. But this only yields local generalization, not any real ability to make sense of new situations. This is why LLMs need to be trained on enormous amounts of data: the only way to make them somewhat useful is to expose them to a *dense sampling* of absolutely everything there is to know and everything there is to do. Humans don't work like this -- even the really dumb ones are still vastly more intelligent than LLMs, despite having far less knowledge.