aSanchezStern

Not sure what the timeline on that is, but the University of Washington had housing specifically for PhD students with families in the 60s/70s IIRC

Err, turning "shouldn't be talking to each other this much" to "shouldn't be talking to each other" is quite the leap. The author is clearly referring to the minute-by-minute stimulation that a microblogging platform provides, not making the case that people should be cutting off all communication with each other.

Yeah, younger generations are spending less and less time with friends in person [1] and feeling lonelier and lonelier as a result [2].

[1] https://thehill.com/blogs/blog-briefing-room/4037619-teens-a... [2] https://www.washingtonpost.com/local/social-issues/teens-lon...

Location: Seattle, WA Remote: Yes Willing to relocate: No Technologies: C, C++, Python, Linux, Rust, PyTorch, Lisp, Formal Methods, HTML/CSS/JS. Resume/CV: https://www.alexsanchezstern.com/cv.pdf Email: alex.sanchezstern@gmail.com

PhD in formal methods using machine learning, I've done CS research on numerical methods and binary analysis too. Looking for interesting work with some stability after academia. I've led multi-year projects with multiple PhD students during my postdoc.

Uhh, endless recursion doesn't cause your typechecker to run indefinitely; all recursion is sort of "endless" from a type perspective, since the recursion only hits a base case based on values. The problem with non-well-founded recursion like `main = main` is that it prevents you from soundly using types as propositions, since you can trivially inhabit any type.

Err, only if humans have to be turing oracles to have that intuition, right? Plus, the halting problem only says that you can't have a procedure which will be 100% right on 100% of programs about whether or not they halt. Relax either of those 100%s, and it becomes possible again, just like how human intuition can be right about things 90% of the time, even if those things can't possibly be predicted 100% of the time.

The claim that "there can be no explainability of such models" is also completely unsupported. We know that some simple networks can be explained, and explanation is a human notion, not a formal one, so we can't know how much explainability is possible. There's active research in explainability of neural networks and progress is being made. I don't know how far it'll go, but it hasn't hit any sort of theoretical boundary yet. I think the author is making a similar sort of mistake that they do in invoking the halting problem here, confusing a "not forall" for a "forall not". There are certainly neural network models that can't be explained ("not every model can be explained" is true), but that doesn't mean that there aren't ones that can ("every model can not be explained" is not true).

As part of the argument on explainability, the author says "we have known for some time these models cannot represent or model symbolic structures". There might be some particular weird way of defining things where this is true, but it's certainly not true in the most basic reading. In fact, we have very strong theoretical results that a sufficiently wide neural network can compute any function, including those that are "symbolic". Whether they can be trained using gradient optimization to compute every function is an open problem, but the idea that there are functions they can't represent is provably false.

The third point, that LLM's aren't as step towards AGI. They again make the claim that there are functions a DNN can't compute (or approximate arbitrarily well) (see https://en.wikipedia.org/wiki/Universal_approximation_theore... for the theorem that this isn't true).

The rest of this point, and the fourth point, are basically just about how current LLM's are actually pretty dumb in a lot of situations. This is the only argument that's actually compelling to me; there's a lot of hype around LLMs and their abilities, but a lot of that might have to do with our brains being happy to paper over flaws to anthropomorphize things. And the fact that we haven't yet learned what to look for in artificial output, like we spent decades doing for other machine outputs before LLMs. Recall that when dumb pattern matching conversation bots were invented in the 60s (https://en.wikipedia.org/wiki/ELIZA), people thought they couldn't possibly be artificial and must really be human, even though they are obviously artificial by todays standards.

So, I agree that we don't know if LLM's are the first step towards AGI, and they probably aren't in a sense more than the fact that inventions tend to build on each other. But we don't have enough information to say definitively that they aren't that first step.

This is a particular philosophical conjecture, not a proven scientific fact. We don't understand enough about the human brain to prove whether it is fundamentally different from a very complex computer.

Uhhhh, I'm pretty sure Lean already allows for formal verification of code. In the meta theory that tools like Lean and Coq operate, proofs and programs are very intertwined; it's not really possible to build a proving system in this metatheory without also allowing for program verification. Maybe you're talking about gaining support for formal verification of code not written in Lean? Like, being able to verify C? In that case, it's actually just a library issue. Nothing needs to be changed about the core Lean language, someone just needs to formalize the semantics of the target language semantics in Lean, and then add a verified compiler and verified extraction if you want to make the guarantees extend directly to the compiled assembly. Fuzzers have actually combined well with theorem proving in these kinds of tools in the past; Coq, the proof assistant that heavily inspired Lean and has been in constant use since the mid 80's, has a library QuickChick (based on QuickCheck from the Haskell world) which takes an arbitrary property and generates test inputs to test it, and has very mature support for extending it with new datatypes and invariants.

Huh, good question. I think having a herbie-style error visualization graph built into an IDE would go a long way. In practice I think dynamic sampling is pretty good at capturing error behavior, and immediate visual feedback on the floating point code you're writing would make it a lot easier to trust the working code you have, and understand the problems with the error-prone computations. Something like https://github.com/herbie-fp/odyssey, but analyzing the fp expressions in the code files you're editing.

It should be possible. Herbgrind is designed under the philosophy that it's not bad numerics themselves that are significant, it's how they affect the outputs of your program. So the reports are organized around program outputs (either through print calls, or you can annotate values you care about with macros), and errors are reported in terms of how they are affecting your outputs. That should allow you to skip any numerical errors that are insignificant in the final output, and prioritize the ones that are affecting the outputs you care about most greatly.

But Herbgrind is a heavyweight dynamic binary analysis using the Valgrind framework, so the slowdown it imposes on the runtime might be prohibitive for debugging some programs which take a while to compute their results.

I believe that's a PEBCAK error

Wow, didn't expect this tool to be on Hacker News six years after publication! Herbgrind author here, ask me any questions you like! Also, if you're interested in this stuff, the Herbie project (which I also worked on) for numerical program synthesis is also really helpful for writing numerical code, and has had a lot of development over the years.

Sounds like you've stumbled into the wonderful world of machine-learning guided proof synthesis! While I don't think the full system you're describing has been built yet, many similar systems and pieces have. In terms of the initial phase of supervised learning on existing proofs to prove new ones, there's TacticToe (https://arxiv.org/abs/1804.00596), Tactician (https://arxiv.org/pdf/2008.00120.pdf), CoqGym/ASTactic (https://arxiv.org/abs/1905.09381), Proverbot9001 (https://arxiv.org/abs/1907.07794), and Diva (https://dl.acm.org/doi/10.1145/3510003.3510138#sec-terms), among others. Most of these have some sort of language model within them, but if you're specifically looking for the LLM's that have been big recently, there's GPT-f (https://arxiv.org/abs/2009.03393), Baldur (https://arxiv.org/abs/2303.04910), and COPRA (https://arxiv.org/abs/2310.04353), though currently these models don't seem as effective as the specialized non-LLM tools. In terms of using reinforcement learning to learn beyond human written proofs, there's TacticZero (https://openreview.net/forum?id=edmYVRkYZv), this paper from OpenAI (https://arxiv.org/pdf/2202.01344.pdf), rlCoP (https://arxiv.org/abs/1805.07563), the HOList line of work (https://arxiv.org/pdf/1905.10006.pdf), and HyperTree Proof Search (https://arxiv.org/abs/2205.11491), as well as some in progress work I'm working on with a team at the University of Massachusetts.

Additionally, formal verification usability is an area of constant research, and the set of software for which it is the best ROI increases over time.

1979 :) https://en.wikipedia.org/wiki/Logic_for_Computable_Functions

Oh, I think you might misunderstand what I'm comparing it to. The other tools, like Proverbot9001, are exactly the NNUE scenario you describe, where a small neural network guides a search procedure to find proofs; they are more effective at finding formal proofs than Llemma. For other tasks, like non-formal proof generation, Llemma has novel results as far as I know; it's just in terms of producing formal proofs that it currently seems to lack as compared to the state of the art.

Not directly, but COPRA which they compare to (and show about 3% more theorems proved than) is based on GPT-4 using an agent framework. And in the COPRA paper, they compare to using GPT-4 directly as a one-shot, and find it can only get 10% of theorems in miniF2F, as opposed to 23% with their agent based approach. So if the eval line up correctly, we would see GPT-4 one-shot proving 10.6% of theorems in miniF2F, as opposed to Llemma-7b proving 26.23%, a pretty significant improvement. Still not as good as other specialized tools though, especially when you look at tools in other theorem proving languages (see my other comment for more detail about a cross-language comparison).

Note that this still doesn't seem as good at solving proofs as some of the specialized prover models at formal theorem proving that aren't LLM-based. In particular, they show a 3% increase in proves solved over COPRA on the MiniF2F Lean dataset, but in COPRA's own paper they show that they prove about 18.5% fewer theorems than Proverbot9001 on the CompCert dataset (their pitch is that they are faster, but not better at proving, than other tools). Assuming COPRA isn't just way better at Lean than Coq (there should be some amount of difference, but given that it's the same algorithm run on a uniform interface over Coq and Lean it's unlikely to be large), Llemma should be proving 10-15% fewer proofs than Proverbot9001's algorithm. There's a bit of trickiness to trying to do this kind of cross-benchmark comparison, and COPRA picks a bit of a weird dataset to compare to Proverbot9001 on to save costs, but they also use a slightly older version which has worse results. So it probably still washes out to the best LLM-based provers being about 10-15% worse at proving theorems than the best specialized models.

EDIT: To be clear, that's 10-15% of the total theorems in a test set, not a relative 10-15% improvement. Given that solve rates for tools are in the 10-30% range, that's much more than a relative 10-15% improvement.

That... doesn't seem to check out. It can't be the going rate if it's infeasible. By definition the going rate is the rate that would allow you to afford doing the startup. Maybe you're comparing to the going rate of running a much better funded startup? But that's not the going rate for a startup of your funding size.

Cool to see this new garbage collection work from OOPSLA 2023 coming up in blog posts! The blog post doesn't mention that this new algorithm looks like it's going to become the default in Firefox, and is being implemented in Chrome [1]. Also, the paper is open access so click the links if you want more details, it won't be paywalled like some other papers.

[1] https://marisa.moe/balancer.html

> which effectively means you work most of the year for the tax man and not yourself

That would be true, if we lived in a world where your gross salary corresponded linearly to the amount of work you did. In that world, the hardest-working CEO would make 3x (maybe in some extreme cases 5x) what the laziest server made. But instead we live in a world where the "successful" make 100x-1000x, because that money isn't coming from their effort, it's coming from a combination of government subsidies (you may not be using the NHS, but the poor people who make your job possible certaintly are) and extreme power imbalances in market conditions that allow them to pay the people on the ground creating the value very little.

I think if you could be a little more specific about what institutions think it's okay to discriminate against you in particular, it would really help.

Hmm, but saying that you have privilege is not the same thing as saying you've done something wrong or are guilty, right? Even if you were born into an overall advantage, it wouldn't mean you had done anything wrong.

Hmm, has anyone here met someone who espoused the argument "White people are inherently morally guilty due to racism"? I'm getting the sense that it might be mostly a strawman argument. Those I've actually talked to about anti-racism seem to fall into two camps; either white people (a very hard to define group of people, but mostly you know what I mean) aren't all racist, but they have benefited from past racism, so they hold extra power unjustly (though not due to a fault of their own); or they are "racist", but where "racist" is defined as prejudice + power, and we understand that many people are prejudiced due to societal and cultural messaging, so being "racist" doesn't mean you're individually guilty.

I believe you're basically referring to the computable reals; for the curious, here's the wikipedia page (kind of abstract): https://en.wikipedia.org/wiki/Computable_number and here's the paper where they implement them programmatically, including for the android calculator application (I believe this is how the android calculator works now): https://dl.acm.org/doi/abs/10.1145/3385412.3386037

This is actually fewer bits than they're using in the article, but that's not clear because they refer to their numbers by how many "[decimal] digits", not how many bits. The hardware doubles they're starting with are 64-bits wide, representing 15.5 decimal digits, but then they move into 128- and 256-bit representations. 80-bit math, such as that available on the old x87 floating point co-processors, is I believe about 21 decimal digits.

Unfortunately while Posits (and Unums) are more accurate for some computations, they are still designed around using small numbers of bits to represent numbers, so they have error in computations just like floating point. The argument for posits are mostly that they produce less error on the inputs you care about, and more on the ones you don't, but it really depends on your computation; you really have to know what you're doing to use them safely.

For those curious, this tool uses arbitrary precision floating-point arithmetic (up to 3000 bits) to sample the input space and measure the error of different implementations of the function, then some clever numerical program synthesis to generate candidates and search for the most accurate implementation.

Yeah there are a few number systems that can do this kind of thing, ranging from rational implementations where the numerator and denominator are stored, all the way to the computable reals (https://en.wikipedia.org/wiki/Computable_number), which can handle even trancendentals exactly! Fun fact, the built-in calculator on android actually uses the computable reals (https://dl.acm.org/doi/abs/10.1145/3385412.3386037), so you can do any calculation on it, and then ask for any number of digits (keep scrolling the result), and it will always be correct. The only downside is that they're a little too slow to use in a lot of performance-sensitive numerical applications.