Rudism's recent activity
-
Comment on Midnight Radio | Podcast trailer in ~tv
-
Comment on Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs in ~tech
Rudism Link ParentThe NL proof is the thing that's going to be read by humans and cited in other papers, so it seems bizarre to me to brush off the potential that it has mistakes and is not faithfully represented...The NL proof is the thing that's going to be read by humans and cited in other papers, so it seems bizarre to me to brush off the potential that it has mistakes and is not faithfully represented by the formal Lean proof. I suppose if the AI-boosters are right and human mathematicians just went extinct as a species, then NL proofs are pointless now anyway.
-
Comment on Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs in ~tech
Rudism Link ParentThe linked paper has concrete demonstrations of incorrect proofs that got mistranslated into compiling Lean proofs, to show that a compiling Lean proof doesn't necessarily imply that the thing the...The linked paper has concrete demonstrations of incorrect proofs that got mistranslated into compiling Lean proofs, to show that a compiling Lean proof doesn't necessarily imply that the thing the LLM is claiming to prove has actually been proven. And the fact that these concrete examples exist seems to contradict the tweet you linked where the guy seems to be implying that's not a thing that can happen and it's all a nothingburger.
-
Comment on Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs in ~tech
Rudism Link ParentSo it sounds like his argument that there is no need to verify that the natural language proof and the formalized Lean proof are the same thing because... reasons? It makes no sense to me. What...So it sounds like his argument that there is no need to verify that the natural language proof and the formalized Lean proof are the same thing because... reasons?
It makes no sense to me. What even is the purpose of the formalized Lean proof if the natural language proof is already enough to solve the problem without the extra step of verifying that the formalized proof is actually a valid representation of it?
-
Comment on Solo developer rebuilds Adobe Creative Suite in Rust using Claude, releases it free to all in ~tech
Rudism Link ParentThis idea feels like it stems from a misunderstanding of how LLMs work (though admittedly I only have a surface level understanding myself). As far as I am aware, the only reason LLMs can do what...Things will change again when we start to see more LLM optimised toolsets, langauges and tech stacks coming out.
This idea feels like it stems from a misunderstanding of how LLMs work (though admittedly I only have a surface level understanding myself). As far as I am aware, the only reason LLMs can do what they do is because they have trained on massive amounts of scraped source code that was written by humans for human-oriented toolchains. I mean they are large "language" models trained on massive, massive amounts of human language (everything they understand and can generate is rooted in human-generated language, including every line of source code ever fed into the training process). What you're implying is that somehow we'll develop non-human languages to train the LLMs on that are more efficient than what humans can comprehend and work with, but where do you think the training data for those new languages and toolchains is going to come from?
-
Comment on Introducing all-new Amazon Alexa Tablets—powerful tablets with Alexa+ built in in ~tech
Rudism Link ParentI could see it maybe one day, if someone figures out how to root them and they get custom ROMs (like a LOS port or something). Especially once they get heavily marked down because that's what...I could see it maybe one day, if someone figures out how to root them and they get custom ROMs (like a LOS port or something). Especially once they get heavily marked down because that's what inevitably happens to all Amazon hardware.
-
Comment on The return of phones with physical keyboards? in ~tech
Rudism Link ParentHave you tried Futo? It's privacy-friendly and as usable and accurate as other keyboards I've tried (though admittedly that's mostly limited to AOSP, GBoard, and a few others from F-Droid). It's...Have you tried Futo? It's privacy-friendly and as usable and accurate as other keyboards I've tried (though admittedly that's mostly limited to AOSP, GBoard, and a few others from F-Droid). It's the one I use on my Graphene OS phone.
-
Comment on Triple-A Minesweeper in ~games
Rudism LinkHonestly it was too hard for me. I could barely figure out where it wanted me to click from those vague markers. Are there plans to add a story mode for us non-hardcore gamers?Honestly it was too hard for me. I could barely figure out where it wanted me to click from those vague markers. Are there plans to add a story mode for us non-hardcore gamers?
-
Comment on What have you been watching / reading this week? (Anime/Manga) in ~anime
Rudism LinkI've been in a romcom mood, so I watched (most of) Lovely★Complex. It started out kind of rough, but hit a stride that I was enjoying for the most part, and came to pretty much a perfect and...I've been in a romcom mood, so I watched (most of) Lovely★Complex. It started out kind of rough, but hit a stride that I was enjoying for the most part, and came to pretty much a perfect and satisfying conclusion around episode 18 or 19. But then it kept going, and became unbearably tedious, so I ended up bailing. Maybe something redeeming happens in those last few episodes but I couldn't drag my way through the trenches for long enough to find out.
-
Comment on OpenAI releases findings on 377 math problems, further roiling field in ~science
Rudism Link ParentSo far, in my personal experience where I work, that does not seem to be the way things are going. It's entirely possible that I'm biased. I work on software for the aerospace industry (primarily...- Exemplary
So far, in my personal experience where I work, that does not seem to be the way things are going.
It's entirely possible that I'm biased. I work on software for the aerospace industry (primarily NASA), and our software is used and relied on in a way such that bugs in certain portions of the code could literally cost human lives. When a mission critical bug is found, it's extremely stressful even when you're working together with engineers who know the codebase intricately because they were involved in every step of its development—architecture, logic design and decisions, down to writing the code by hand themselves. I can't even imagine how much more stressful it would be if nobody actually knew the code, or only understood it as vague high-level abstractions, and instead of a bunch of experts scrutinizing the code that they all wrote together to find and fix the problem, you'd have to read and trust a bunch of sycophantic word salad LLM output about it. That idea is absolutely terrifying and I can't imagine a world where we'd all just be fine with it.
-
Comment on OpenAI releases findings on 377 math problems, further roiling field in ~science
Rudism Link ParentMost of the people I know and work with do still use IDEs (even the ones who have adopted LLMs into their projects and workflow). I'm not really saying that developers who rely on LLMs to generate...Most of the people I know and work with do still use IDEs (even the ones who have adopted LLMs into their projects and workflow). I'm not really saying that developers who rely on LLMs to generate all their code don't or won't exist, I'm just saying that developers who don't do that aren't going away any time soon and which type of developer you aspire to be (one who writes code, or one who writes no code and instead reviews and iterates on LLM generated code) will be a choice, and that both of those choices will remain a valid one, each with its own pros and cons and attractiveness to developers with different values and skillsets.
-
Comment on OpenAI releases findings on 377 math problems, further roiling field in ~science
Rudism Link ParentWe'll just have to agree to disagree on that one, to me that is an absolutely insane take.We'll just have to agree to disagree on that one, to me that is an absolutely insane take.
-
Comment on Given everything we know about AI so far, what do you think it can or cannot be good for? in ~tech
Rudism LinkTalking about generative AI and LLMs, I think it's probably one of the most impressive technologies we've developed as a species. I think its potential to improve all fields in all kinds of...Talking about generative AI and LLMs, I think it's probably one of the most impressive technologies we've developed as a species. I think its potential to improve all fields in all kinds of mind-boggling ways is absolutely bonkers—in particular I think assistive technologies for persons with disabilities and medical research stand to benefit immensely.
All that being said, I cannot in good conscience use them myself, and do my absolute best to interact with LLMs and other generative AI tools as little as humanly possible. That they are fully controlled by the absolute worst corporate powers run by the greediest people on earth, built completely without the consent of or compensation to the people who originally created the data they're being trained on, and being developed with less-than-zero regard for social and environmental consequences, makes them absolute poison to me. Additionally, that so many of my peers seem to have drowned in the flavor-aid being forced down our throats and whole-heartedly embracing them while making wild proclamations about how they'll replace all humans in various professions (to say nothing of the even wilder claims of AGI), I am even more turned off of the technology.
tl;dr I think they're awesome, I think they're being built and used irresponsibly, and I refuse to use them (until that hopefully one day changes).
-
Comment on OpenAI releases findings on 377 math problems, further roiling field in ~science
Rudism Link ParentI disagree that coding is going away. I think we still don't know what that future looks like, and LLMs will certainly play a part (especially if they ever become economically viable in a way that...I disagree that coding is going away. I think we still don't know what that future looks like, and LLMs will certainly play a part (especially if they ever become economically viable in a way that doesn't 100% rely on the worst, greediest billionaires in the world and destroying our planet), but I believe there will always be value in prioritizing a tight code base, and building and maintaining institutional knowledge over how that code actually works, and the more you rely on LLMs to do all your coding for you the more those things necessarily get sacrificed. Nobody gets into software engineering because they like reading code, and that will go a hundred fold when we're talking about reading LLM generated code. There's a reason that "vibe coding" is so derided--it produces shit. A world where "'coding' is basically over" is a world where everything is essentially vibe coded garbage and I very strongly disagree that will ever take over the industry as a whole.
-
Comment on OpenAI releases findings on 377 math problems, further roiling field in ~science
Rudism Link ParentI have a layperson (maybe dumb) question... Where do the mathematical problems that are being solved here come from? Or I guess another way to put that is, how do we become aware of these problems...I have a layperson (maybe dumb) question... Where do the mathematical problems that are being solved here come from? Or I guess another way to put that is, how do we become aware of these problems that need solving in the first place? And once they are solved, do they typically have some practical application that can benefit from that solution?
-
Comment on OpenAI releases findings on 377 math problems, further roiling field in ~science
Rudism Link ParentSoftware engineers are saying similar things about programming, and I'm not convinced of that either. There's too much hype, too much fresh fear and uncertainty, and too many corporate interests...Software engineers are saying similar things about programming, and I'm not convinced of that either. There's too much hype, too much fresh fear and uncertainty, and too many corporate interests in pushing these kinds of extreme narratives for me to take any of it without a massive grain of salt and rolling my eyes a bit.
-
Comment on OpenAI releases findings on 377 math problems, further roiling field in ~science
Rudism Link ParentI don't disagree that computers in general may already or one day be better than human mathematicians at solving certain types of problems. I disagree that LLMs are the most likely path to get us...I don't disagree that computers in general may already or one day be better than human mathematicians at solving certain types of problems. I disagree that LLMs are the most likely path to get us there though. You accuse my skepticism of being cope, but to state things like LLMs are "better than nearly all mathematicians" based on the info we have right now seems absolutely bonkers to me, so I think we're just operating on completely different wavelengths when it comes to LLMs.
-
Comment on Was watching a history YouTube video when I realized they are all AI in ~tech
Rudism LinkThis video from Christophe (not AI, I'm reasonably sure) talks a bit about how a lot of AI generated videos that pop up now are just altered or recreated beat-for-beat from content posted by real...This video from Christophe (not AI, I'm reasonably sure) talks a bit about how a lot of AI generated videos that pop up now are just altered or recreated beat-for-beat from content posted by real creators. It really does make YouTube even more useless as a content discovery platform these days. Slop is so effortless to pump out, and putting effort into actual human-created content is becoming so unrewarding and demoralizing that I can only imagine this trend is going to continue.
-
Comment on Alright, ladies and gentlemen. Thinking caps needed. #Apple #movies #tv in ~tech
Rudism LinkSlightly off topic, but this reminds me of this comment in which @CrypticCuriosity629 describes in great detail a rather complex but awesome sounding IPTV setup to replicate TV channels from the...Slightly off topic, but this reminds me of this comment in which @CrypticCuriosity629 describes in great detail a rather complex but awesome sounding IPTV setup to replicate TV channels from the 90s.
My on-topic response is, I think due to Apple's DRM very deliberately restricting unauthorized playback, you're not going to find any options here that don't involve figuring out some way to rip and remove DRM from everything you own into local storage (assuming such a thing is even possible).
-
Comment on OpenAI releases findings on 377 math problems, further roiling field in ~science
Rudism Link ParentI'd bet also that a model that's been hyper-tuned to write mathematics proofs is probably not very good at anything else, so it wouldn't be useful as a general purpose model that everyday users...I'd bet also that a model that's been hyper-tuned to write mathematics proofs is probably not very good at anything else, so it wouldn't be useful as a general purpose model that everyday users would see any benefit from (and might even be embarrassing for them once people started prodding at it).
Seems like it could be (at least partly) inspired by Art Bell's call-in shows back in the day. I grew up obsessed with Coast to Coast AM when he was the host back in the 90s.