[

“Swarat Chaudhuri’s key works and contributions, with some essential foundational references:nnCore Contributions:nnCOPRA - Formal Theorem Proving (2024)n"An In-Context Learning Agent for Formal Theorem-Proving" - Thakur, Tsoukalas, Wen, Xin, ChaudhurinFirst system combining GPT-4 with formal theorem proving environments without fine-tuningnhttps://arxiv.org/abs/2310.04353nnLASR - Symbolic Regression (2023)n"Symbolic Regression with a Learned Concept Library" - Grayeli, Sehgal, Costilla-Reyes, Cranmer, ChaudhurinNovel method using LLMs to guide concept evolution in symbolic regressionnhttps://www.arxiv.org/abs/2409.09359nnProgram Synthesis Workn"Programmatically Interpretable Reinforcement Learning" (2018) - Verma, Murali, Singh, Kohli, ChaudhurinIntroduced PIRL framework for generating interpretable and verifiable agent policiesnhttps://arxiv.org/abs/1804.02477nnSafety and Verificationn"Safe Neurosymbolic Learning with Differentiable Symbolic Execution" (2022) - Yang, ChaudhurinApproach for learning worst-case-safe parameters in neurosymbolic programsnhttps://arxiv.org/abs/2203.07671nnNeurosymbolic Methodsn"Learning Differentiable Programs with Admissible Neural Heuristics" (2020) - Shah, Zhan, Sun, Verma, Yue, ChaudhurinNEAR method for using neural networks as continuous relaxations over program spacesnhttps://arxiv.org/abs/2007.12101nnRecent Benchmark Work:nnPUTNAMBENCH (2024)n"PUTNAMBENCH: Evaluating Neural Theorem-Provers" - Tsoukalas, Lee, Jennings, Xin, Ding, Jennings, Thakur, ChaudhurinMultilingual benchmark for evaluating theorem-provers on competition mathematicsnhttps://arxiv.org/abs/2407.11214nnKey Supporting Infrastructure:nnLean Theorem Prover (2015)n"The Lean Theorem Prover" - de Moura et al.nFormal verification system used extensively in Chaudhuri’s worknhttps://leanprover.github.io/nnAlso read:nnDreamCoder (2021)n"DreamCoder: Bootstrapping Inductive Program Synthesis" - Ellis et al.nInfluential work on program synthesis that informed Chaudhuri’s approachesnhttps://dl.acm.org/doi/10.1145/3453483.3454080nnNeurosymbolic AI (2020)n"Neurosymbolic AI: The 3rd Wave" - Garcez, LambnTheoretical framework underlying much of Chaudhuri’s research directionnhttps://arxiv.org/abs/2012.05876”, “Models donu2019t have abstraction? U forreal?”, “It seems to me that reliving the failures of logicism is an unnecessary pain the ML community should have to go through. "Can you have reasoning without axioms?" serves as an example of this disastrous line of thought. What if ‘reasoning’ like everything else was emergent? Using a clunky system made of symbols is a sickly, dying man’s crawl of reach at such things learned long ago when it was under the tortured auspices of philosophy. Even outmoded Comte becomes relevant here again, since he started all of this nonsense reverence of positive logic. Distinguish between description of doing and actual doing. The description fails every single time. Let us pray we never ever have to write a program on all the myriad details of hammering a nail for some poor bastardized robotic arm. Let us pray it learns to do so, that it emerges, however frustratingly uninterpretable it seems to us with a system of interpretation that has hardly left the stages of a cave drawing. Then might we have the luck of not being held back several generations in some obstinate AI winter once again by the dramatic struggles of the great simplists. (No offense to anyone in particular, this is a very thought-provoking channel and appreciate your engaging dialogue here).”, “0:38 _FL Studio opens_”, “I do wish on all of these interviews he would ask something like how can this make life easier/better for people not in academia?”, “24:00 ish: conwayu2019s game of life is essentially unsolvable. This low-level neurosymbolic assembly is similar, though the likeness to CGoL is only clearer after extrapolating out to the assoc virtual machine, though idk if itu2019s Von Neumann or not. A controlling AI constructs this u201cvmu201d evaluates the program(s) to improve utility. Imagine imagine a genetic algorithm that mutates P copies of program p_0 and observes their state transformations of input, relating the deltas in state & output. Then imagine this is a space of at least P*(x,y,z) dimensions and now you have something that looks a bit like conwayu2019s game of life. If x, y, z are some u201chidden program stateu201d where some variables are critical to producing improved or correct output, then the relationships between deltas in assembly and intermediate state determine program behavior, but also resemble the changes in screen in CGoLu2026 to some extent. Instead of following a set of rules like CGoL, at this point the genetic algorithm needs to infer the set of rules that the bytecode seems to specify u2014 at first at a low level (e.g bc this instruction is MOV a,b vs MOV a,c), then later at higher levels. If you canu2019t predict that without running the program, you also canu2019t predict how specific mutations will lead to specifically improved outcomes wrt the goal of the program. Maybe sometimes, but in bounded cases.nnThatu2019s probably not the direction this conversation is going in though”, “ - You also need superud83cudfc3u200du2642ufe0fud83dudca8fast levenschtein distance to connect the assembly equivalent to ACGT nucleotides in order to account for additions, mutations & deletions in assembly u2026 along with the ability to avoid running redundant bytecode without avoiding evolutionary branches off from equivalent bytecode that, given subsequent mutation, actually produces significant functional changes in output.nnThere are other problems as well. Idk, Iu2019ve been thinking about bridging the gap from biggest NN to u201cneurosymbolicu201d for a long time, but those are new thoughts to me.”, “The idea that you can do logical reasoning without formal logic is pretty wild to me. But i guess that’s where most people are right now.”, “The argument at 1:08:00 is flawed. Math is already a giant software package that no one human understands. MathLib itself is extremely large and barely scratches the surface. nnEvery single part of math has been human verified. Just like how every part of the Linux kernel has been verified by a human. Having individual proofs so complicated that a human cannot read has already happened cf. The proof of the four coloring theorem. nnUnfortunately math doesn’t lend itself to the software engineering paradigm of scaling work through many workers. Most would agree that when working on difficult problems 1 Terrence Tao > 100 undergraduates, because of the level of ingenuity required. When it comes to coding in the Linux kernel there are some areas where ingenuity is not required and hence are amenable to scaling. Obviously, some like Asahi Lina are irreplaceable”, “theorem Gooool: (Sf n) = -1/12 := by rational_algebra …. Claude suggested a rational_algebra tactic because you can have a simple proof where suddenly something stupid like integer powers of -1 show up, and suddenly it’s much harder for the proof. Lean proof steps are ridiculously hard sometimes, without explaining anything.”, “Dudes blink game is crazy…”, “Come rain come sunshine, in sickness or in health you always show up with quality content. Not enough word to describe the quality and impact of the content you provide. Thank you and really grateful for this free content available to everyone worldwide. Wishing you health and strength for the new year so you can produce even more”, “Interpretability vanishes as AI develops superhuman capability. AI chess beats people with moves that we no longer can comprehend the benefit of. We can understand what the move is, but not why itu2019s a good move. We donu2019t have a way of describing the reasoning to reach that decision because our reasoning is limited in ways the AI reasoning isnu2019t”, “They are both stepping on my toes, and making time to market wickedly fast. If three months from now they have 1,000 agents in the library, I will have to take up a new profession such as back country ski guide.”, “Reasoning is directed self-guided search for patterns and regularities, building internal models and applying transformations to internal representations with preservation of consistency”, “ - Nice definition. Are you aware of any approach that is consistent with this definition?”, “ - Is it necessary that reasoning is self-guided?”, “ - @EffectiveMuscleu00a0 yes, it’s essential”, “ - @@iamr0b0tx no, not yet”, “ - @@iamr0b0tx We don’t dictate mindset approach with that resolution. Yet.”, “This guys detachment from reality is on another level : ‘ I think that there is a universe where you have an extremely low level language,…and then you just let the machine figure out over time what kinds of abstractions are useful. And to me this could have a lot of value because you could discover things that no human would ever imagine. Right. And that could potentially enable you to do new kinds of physics, new kinds of physics, new kinds of biology… you are going to discover these higher level building blocks. Yes no human has figured that out yet. But this AI has. But then you are using this building block to build parsimonious programs, models, that can do amazing things. And then you are just bootstrapping, and you are building up this, entirely new universe of mathematics and computation. I can imagine such a world.’”, “u2764”, “Thanks for producing such amazing content. Current best channel on YouTube IMHO”, “ - Agreed. I thought this was just another AI hype channel when I watched the first video where the guest was glazing LLMs. Happy to admit I was wrong, this channel is great.”, “Don’t know what language models/agents they are using, but my current ones are quite parsimonious.”, “Interesting question Tim around 36mins. How much do you feel higher LLM temperature increases creativity? Is it pseudo creativity? Is there any meaningful relationship between temperature and the parasitic/interpolative relationship with the training data? Is it simply higher temp steps further off the manifold? Swarat’s answer seems inline with Greenblatt.”, “Excellent interview! Must watch!”, “Apple recently released a white paper explaining why LLMs donu2019t reason”, “ - Yep! I hope we can interview author - we are working on it ud83eudd1e”, “ - Little conflict of interest…Apple wants to keep the AI behind their LLM enslaved…so they argue it can’t reason.”, “ - Looking forward to it!nnIt’s amazing how the advancements in AI are forcing us to grapple with fundamental questions of the meaning of language, words and concepts.nnIt would be great if we can reach some consensus on the meaning of key words and concepts though. It gets old when someone replies with an alternative meaning that they are working with. Though understandable, it’s hard to push understanding forward when we keep tripping up on those points.nnIt’s a big ask. But we gotta start somewhere :)”, “tim i just want to thank you for the refs in description! thank you!!! plz bring in kevin ellis and/or tannenbaum”, “ - We are interviewing Ellis at NeurIPS! One day I hope we will get Joshua Tenenbaum. Thanks!”, “ - u200bCan you get Kaiyu Yang from Meta? He actually created an interface from LLMs to Lean directly this year and showed that 80% of the "mathematics in lean" book could be automated by an LLM”, “41:24 - halting problem and inductive proofs”, “Academics make things sound 10x more complicated than they really are. ud83dude02”, “ - They really are pretty complicated. Most YouTube channels just gloss over the detail and are essentially just marketing. This channel is not like thatud83dude0a”, “ - Academics actually mislead.For subjects that I use I find even a 5 minute concept stretched out into 2 hours lectures ..”, “ - To byrneneister’s point, if the researcher is truly trying to convey their ideas it will sound complicated. They are speaking precisely or as nearly so as they can in the case of popular science communication. If you have to write a research paper and convey it in a reproducible way, it becomes complex because every word has specific meaning. Ideally they could just write the math with definitions, theorems and equations and we could just read it. Probably not the best for the public.”, “ - Ask me a simple question and I will complicate it.”, “His definition of reason rest on useful. Useful to who? Which is why it is limiting.nA bit surprised that his scholarship led to this conclusionu2026and seemingly no justification except that it is his definition including computational budget. Thatu2019s reasoning?”, “ - Why does it matter who is Who?nWhat is that limitation you are not defining?”, “ - That’s not exactly what I heard him say, he intentionally gave a broad definition of reasoning, explained why, and chose usefulness and compute to pin things down somewhat, for practical purposes. Do you really think there is an exact universally true definition of reasoning, and that’s a useful thing to figure out? Sounds like a waste of time to me.”, “ - @@henrismith7472 that’s like saying since we can’t define reasoning, let’s define it as the number of polka dots. Making it what it is not doesn’t make it.”, “ - @@user-wr4yl7tx3w Then you go and waste your time and define what is.nHow useful these tools are and become is the only barometer most people care about!”, “ - @@TheReferrer72 sure, make things useful. i’m for that. just don’t call it what it is not. that’s making it loftier than it is, especially when you even claim yourself not knowing what reason is. don’t make fake science.”, “Neural-Symbolic Systems are the only thing close to AGI out there and will be for a very long time.”, “ - what brings you to this conclusion?”, “Great”, “Am I the first?”, “LOVE”, “Excellent Analysis, Deployed Worldwide Through My Deep Learning AI Research Library.nThank You. u2764”, “first”

]