|
| 1 | +[ |
| 2 | + "Swarat Chaudhuri's key works and contributions, with some essential foundational references:\n\nCore Contributions:\n\nCOPRA - Formal Theorem Proving (2024)\n\"An In-Context Learning Agent for Formal Theorem-Proving\" - Thakur, Tsoukalas, Wen, Xin, Chaudhuri\nFirst system combining GPT-4 with formal theorem proving environments without fine-tuning\nhttps://arxiv.org/abs/2310.04353\n\nLASR - Symbolic Regression (2023)\n\"Symbolic Regression with a Learned Concept Library\" - Grayeli, Sehgal, Costilla-Reyes, Cranmer, Chaudhuri\nNovel method using LLMs to guide concept evolution in symbolic regression\nhttps://www.arxiv.org/abs/2409.09359\n\nProgram Synthesis Work\n\"Programmatically Interpretable Reinforcement Learning\" (2018) - Verma, Murali, Singh, Kohli, Chaudhuri\nIntroduced PIRL framework for generating interpretable and verifiable agent policies\nhttps://arxiv.org/abs/1804.02477\n\nSafety and Verification\n\"Safe Neurosymbolic Learning with Differentiable Symbolic Execution\" (2022) - Yang, Chaudhuri\nApproach for learning worst-case-safe parameters in neurosymbolic programs\nhttps://arxiv.org/abs/2203.07671\n\nNeurosymbolic Methods\n\"Learning Differentiable Programs with Admissible Neural Heuristics\" (2020) - Shah, Zhan, Sun, Verma, Yue, Chaudhuri\nNEAR method for using neural networks as continuous relaxations over program spaces\nhttps://arxiv.org/abs/2007.12101\n\nRecent Benchmark Work:\n\nPUTNAMBENCH (2024)\n\"PUTNAMBENCH: Evaluating Neural Theorem-Provers\" - Tsoukalas, Lee, Jennings, Xin, Ding, Jennings, Thakur, Chaudhuri\nMultilingual benchmark for evaluating theorem-provers on competition mathematics\nhttps://arxiv.org/abs/2407.11214\n\nKey Supporting Infrastructure:\n\nLean Theorem Prover (2015)\n\"The Lean Theorem Prover\" - de Moura et al.\nFormal verification system used extensively in Chaudhuri's work\nhttps://leanprover.github.io/\n\nAlso read:\n\nDreamCoder (2021)\n\"DreamCoder: Bootstrapping Inductive Program Synthesis\" - Ellis et al.\nInfluential work on program synthesis that informed Chaudhuri's approaches\nhttps://dl.acm.org/doi/10.1145/3453483.3454080\n\nNeurosymbolic AI (2020)\n\"Neurosymbolic AI: The 3rd Wave\" - Garcez, Lamb\nTheoretical framework underlying much of Chaudhuri's research direction\nhttps://arxiv.org/abs/2012.05876", |
| 3 | + "Models don\u2019t have abstraction? U forreal?", |
| 4 | + "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).", |
| 5 | + "0:38 _FL Studio opens_", |
| 6 | + "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?", |
| 7 | + "24:00 ish: conway\u2019s 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 it\u2019s Von Neumann or not. A controlling AI constructs this \u201cvm\u201d 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 conway\u2019s game of life. If x, y, z are some \u201chidden program state\u201d 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 CGoL\u2026 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 can\u2019t predict that without running the program, you also can\u2019t predict how specific mutations will lead to specifically improved outcomes wrt the goal of the program. Maybe sometimes, but in bounded cases.\n\nThat\u2019s probably not the direction this conversation is going in though", |
| 8 | + " - You also need super\ud83c\udfc3\u200d\u2642\ufe0f\ud83d\udca8fast 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.\n\nThere are other problems as well. Idk, I\u2019ve been thinking about bridging the gap from biggest NN to \u201cneurosymbolic\u201d for a long time, but those are new thoughts to me.", |
| 9 | + "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.", |
| 10 | + "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. \n\nEvery 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. \n\nUnfortunately 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", |
| 11 | + "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.", |
| 12 | + "Dudes blink game is crazy...", |
| 13 | + "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", |
| 14 | + "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 it\u2019s a good move. We don\u2019t have a way of describing the reasoning to reach that decision because our reasoning is limited in ways the AI reasoning isn\u2019t", |
| 15 | + "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.", |
| 16 | + "Reasoning is directed self-guided search for patterns and regularities, building internal models and applying transformations to internal representations with preservation of consistency", |
| 17 | + " - Nice definition. Are you aware of any approach that is consistent with this definition?", |
| 18 | + " - Is it necessary that reasoning is self-guided?", |
| 19 | + " - @EffectiveMuscle\u00a0 yes, it's essential", |
| 20 | + " - @@iamr0b0tx no, not yet", |
| 21 | + " - @@iamr0b0tx We don't dictate mindset approach with that resolution. Yet.", |
| 22 | + "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.'", |
| 23 | + "\u2764", |
| 24 | + "Thanks for producing such amazing content. Current best channel on YouTube IMHO", |
| 25 | + " - 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.", |
| 26 | + "Don't know what language models/agents they are using, but my current ones are quite parsimonious.", |
| 27 | + "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.", |
| 28 | + "Excellent interview! Must watch!", |
| 29 | + "Apple recently released a white paper explaining why LLMs don\u2019t reason", |
| 30 | + " - Yep! I hope we can interview author - we are working on it \ud83e\udd1e", |
| 31 | + " - Little conflict of interest...Apple wants to keep the AI behind their LLM enslaved...so they argue it can't reason.", |
| 32 | + " - Looking forward to it!\n\nIt's amazing how the advancements in AI are forcing us to grapple with fundamental questions of the meaning of language, words and concepts.\n\nIt 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.\n\nIt's a big ask. But we gotta start somewhere :)", |
| 33 | + "tim i just want to thank you for the refs in description! thank you!!! plz bring in kevin ellis and/or tannenbaum", |
| 34 | + " - We are interviewing Ellis at NeurIPS! One day I hope we will get Joshua Tenenbaum. Thanks!", |
| 35 | + " - \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", |
| 36 | + "41:24 - halting problem and inductive proofs", |
| 37 | + "Academics make things sound 10x more complicated than they really are. \ud83d\ude02", |
| 38 | + " - They really are pretty complicated. Most YouTube channels just gloss over the detail and are essentially just marketing. This channel is not like that\ud83d\ude0a", |
| 39 | + " - Academics actually mislead.For subjects that I use I find even a 5 minute concept stretched out into 2 hours lectures ..", |
| 40 | + " - 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.", |
| 41 | + " - Ask me a simple question and I will complicate it.", |
| 42 | + "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 conclusion\u2026and seemingly no justification except that it is his definition including computational budget. That\u2019s reasoning?", |
| 43 | + " - Why does it matter who is Who?\nWhat is that limitation you are not defining?", |
| 44 | + " - 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.", |
| 45 | + " - @@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.", |
| 46 | + " - @@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!", |
| 47 | + " - @@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.", |
| 48 | + "Neural-Symbolic Systems are the only thing close to AGI out there and will be for a very long time.", |
| 49 | + " - what brings you to this conclusion?", |
| 50 | + "Great", |
| 51 | + "Am I the first?", |
| 52 | + "LOVE", |
| 53 | + "Excellent Analysis, Deployed Worldwide Through My Deep Learning AI Research Library.\nThank You. \u2764", |
| 54 | + "first" |
| 55 | +] |
0 commit comments