sanxiyn

Karma: 787

sanxiyn 27 Oct 2024 2:33 UTC
28 points
9
in reply to: localdeity’s comment on: localdeity’s Shortform
This is a good idea and it already works, it is just that AI is wholly unnecessary. Have a look at 2018 post Protecting Applications with Automated Software Diversity.

sanxiyn 18 Oct 2024 5:37 UTC
15 points
9
on: AI #86: Just Think of the Potential
If we do get powerful AI, it seems highly plausible that even if we stay in control we will ‘go too fast’ in deploying it relative to society’s ability to adapt, if only because of the need to grow fast and stay ahead of others, and because the market doesn’t care that society wants it to go slower.
After reading my interpretation was this: assuming we stay in control, that happens only if powerful AI is aligned. The market doesn’t care that society wants to go slower, but AI will care that society wants to go slower, so when the market tries to force AI to go faster, AI will refuse.
I reflected on whether I am being too generous, but I don’t think I am. Other readings didn’t make sense to me, and I am assuming Dario is trying to make sense, while you seem doubtful. That is, I think this is plausibly Dario’s actual prediction of how fast things will go, not a hope it won’t go faster. But importantly, that is assuming alignment. Since that assumption is already hopeful, it is natural the prediction under that assumption sounds hopeful.
Paul Crowley: It’s a strange essay, in that it asks us to imagine a world in which a single datacenter contains 1E6 Nobelists expert in every field and thinking at 100x speed, and asks what happens if “sci-fi” outcomes somehow don’t happen. Of course “sci-fi” stuff happens almost immediately.
I mean, yes, sci-fi style stuff does seem rather obviously like it would happen? If it didn’t, then that’s a rather chilling indictment of the field of sci-fi?
To re-state, sci-fi outcomes don’t happen because AI is aligned. Proof: if sci-fi outcomes happened, AI would be unaligned. I actually think this point is extremely clear in the essay. It literally states: “An aligned AI would not want to do these things (and if we have an unaligned AI, we’re back to talking about risks)”.

sanxiyn 8 Sep 2024 21:00 UTC
17 points
2
on: My Number 1 Epistemology Book Recommendation: Inventing Temperature
If you enjoyed Inventing Temperature, Is Water H2O? is pretty much the same genre from the same author.
My another favorite is The Emergence of Probability by Ian Hacking. It gets you feeling of how unimaginably difficult for early pioneers of probability theory to make any advance whatsoever, as well as how powerful even small advances actually are, like by enabling annuity.
I actually learned the same thing from studying early history of logic (Boole, Peirce, Frege, etc), but I am not aware of good distillation in book form. It is my pet peeve that people don’t (maybe can’t) appreciate how great intellectual achievement first order logic really is, being the end result of so much frustrating effort. Because learning to use first order logic is kind of trivial, compared to inventing it.

Next automated reasoning grand challenge: CompCert

sanxiyn20 Aug 2024 5:27 UTC

−5 points

0 comments1 min readLW link

sanxiyn 20 Aug 2024 4:50 UTC
11 points
0
on: Limitations on Formal Verification for AI Safety
I think it is important to be concrete. Jean-Baptiste Jeannin’s research interest is “Verification of cyber-physical systems, in particular aerospace applications”. In 2015, nearly a decade ago, he published “Formal Verification of ACAS X, an Industrial Airborne Collision Avoidance System”. ACAS X is now deployed by FAA. So I would say this level of formal verification is a mature technology now. It is just that it has not been widely adopted outside of aerospace applications, mostly due to cost issues and more importantly people not being aware that it is possible now.

sanxiyn 19 Aug 2024 3:12 UTC
3 points
0
in reply to: Viliam’s comment on: How unusual is the fact that there is no AI monopoly?
Result: humanity is destroyed as soon as the patent expires.

sanxiyn 26 Jul 2024 2:17 UTC
4 points
1
in reply to: cubefox’s comment on: “AI achieves silver-medal standard solving International Mathematical Olympiad problems”
The plain interpretation is that only statements to be proved (or disproved) were sourced from human data, without any actual proof steps. In Go analogy, it is like being given Go board positions without next moves.
It makes a lot of sense this is needed and helpful, because winning a game of Go from the empty board is a different and easier problem than playing best moves from arbitrary Go positions. Igo Hatsuyoron mentioned in the original post is a good example; additional training was needed, because such positions never come up in actual games.
Imagine AlphaZero trained from randomly sampled Go positions, each intersection being black/white/empty with uniform probability. It would play much worse game of Go. Fortunately, how to sample “relevant” Go positions is an easy problem: you just play the game, initial N moves sampled at higher temperature for diversity.
In comparison, how to sample relevant math positions is unclear. Being good at finding proofs in arbitrary formal systems from arbitrary set of axioms is actually quite different from being good at math. Using human data sidesteps this problem.

sanxiyn 26 Jul 2024 0:05 UTC
7 points
1
in reply to: cubefox’s comment on: “AI achieves silver-medal standard solving International Mathematical Olympiad problems”
Namely translating, and somehow expanding, one million human written proofs into 100 million formal Lean proofs.
We obviously should wait for the paper and more details, but I am certain this is incorrect. Both your quote and diagram is clear that it is one million problems, not proofs.

sanxiyn 25 Jul 2024 23:10 UTC
9 points
0
on: “AI achieves silver-medal standard solving International Mathematical Olympiad problems”
It feels to me like it shouldn’t be so hard to teach an LLM to convert IMO problems into Lean or whatever
To the contrary, this used to be very hard. Of course, LLM can learn to translate “real number” to “R”. But that’s only possible because R is formalized in Lean/Mathlib! Formalization of real number is a research level problem, which in history occupied much of the 19th century mathematics.
Recently I came across a paper Codification, Technology Absorption, and the Globalization of the Industrial Revolution which discusses the role of translation and dictionary in industrialization of Japan. The following quote is illustrative.
The second stylized fact is that the Japanese language is unique in starting at a low base of codified knowledge in 1870 and catching up with the West by 1887. By 1890, there were more technical books in the Japanese National Diet Library (NDL) than in either Deutsche Nationalbibliotek or in Italian, as reported by WorldCat. By 1910, there were more technical books written in Japanese in our sample than in any other language in our sample except French.
How did Japan achieve such a remarkable growth in the supply of technical books? We show that the Japanese government was instrumental in overcoming a complex public goods problem, which enabled Japanese speakers to achieve technical literacy in the 1880s. We document that Japanese publishers, translators, and entrepreneurs initially could not translate Western scientific works because Japanese words describing the technologies of the Industrial Revolution did not exist. The Japanese government solved the problem by creating a large dictionary that contained Japanese jargon for many technical words. Indeed, we find that new word coinage in the Japanese language grew suddenly after a massive government effort to subsidize translations produced technical dictionaries and, subsequently, a large number of translations of technical books.
Just as, say, translating The Wealth of Nations to Japanese is of entirely different difficulty between the 19th century and 20th century (the 19th century Japanese started by debating how to translate “society”), formalizing IMO problems in Lean is only workable thanks to Mathlib. It would not be workable in other formal systems lacking similarly developed math library, and formalizing research mathematics in Lean is similarly unworkable at the moment, until Mathlib is further developed to cover definitions and background theorems. In the past, ambitious formalization projects usually spent half their time formalizing definitions and background results needed.

sanxiyn 11 Jun 2024 13:12 UTC
7 points
−3
on: On Dwarksh’s Podcast with Leopold Aschenbrenner
First, I would like to second that the world is incredibly small. It bears repeating. I am repeating it to myself to get courage to write this comment. Maybe this is obvious, but maybe it is not. It could be helpful.
Random thoughts on alleged OpenAI memo on selling AGI to highest bidder including China and Russia. This sounds plausible to me, because as I understand before the split with Anthropic OpenAI was very much “team humanity, not team USG or team CCP”. I think this should be understood in context that getting aligned AI is higher priority than geopolitical competition.
Random thoughts on AI labs and coup. Could Los Alamos coup? I mean, obviously no in the real timeline, they didn’t have delivery, none of bomber, ICBM, and nuclear submarine. Let’s just assume after the Trinity test they could unilaterally decide to put a newly produced nuke not yet delivered to the army on ICBM and point that to Washington DC. Can Los Alamos force Truman, say, to share the nuke with Soviet Union (which many scientists actually wanted)?
By assumption, Truman should surrender (even unconditionally), but it is hard to imagine he would. Nuclear threats not only need to be executable, it also needs to be understandable. Also Los Alamos would depend on enriched uranium supply chain which is large industry not under its control, physical security of Los Alamos is under army control and what if security guards just go into Technical area?
Applying this to OpenAI or possible OpenAI-in-the-desert, OpenAI would depend on trillion dollars cluster and its supply chain, large industry not under its control, and same physical security problem. How does OpenAI defend against tanks on the street of San Francisco? With ASI-controlled drones? Why does OpenAI conveniently happen to have drones and drone factories on premise?
I am trying to push back against “if you have ASI you are the government”. If the government is monopoly on violence, millions of perfectly coordinated Von Neumanns do not immediately overthrow USG, key word being immediately. Considering Von Neumann’s talk of nuking Moscow today instead of tomorrow and lunch instead of dinner it will be pretty quick, but it still takes time to have fabs and power plants and data centers and drone factories etc. Even if you use nanotechnology to build them, it still takes time to research nanotechnology.
Maybe they develop mind control level convincing argument and send it to key people (president, congress, NORAD, etc) or hack their iPhones and recursively down to security guards of fabs/power plants/data centers/drone factories. That may be quick enough. The point is that it is not obvious.
Random thoughts on Chinese AI researchers and immigration. US’s track record here is extremely bad, even with cold war. Do you know how China got nukes and missiles? US deported Qian Xuesen, MIT graduate, who founded JPL. He had US military ranks in WW2. He interrogated Werner von Braun for USG! Then USG decided Qian is a communist, which was completely ridiculous. Then Qian went back and worked for communists whoops. Let me quote Atomic Heritage Foundation:
Deporting Qian was the stupidest thing this country ever did. He was no more a communist than I was, and we forced him to go.
US would be well advised to avoid repeating this total fiasco. But I am not optimistic.

sanxiyn 10 Jun 2024 16:03 UTC
6 points
3
in reply to: Yair Halberstadt’s comment on: The Data Wall is Important
Unclear. I think there is a correlation, but: one determinant of crawl completeness/quality/etc is choice of seeds. It is known that Internet Archive crawl has better Chinese data than Common Crawl, because they made specific effort to improve seeds for Chinese web. Such missing data originating from choice of seeds bias probably is not particularly low quality than average of what is in Common Crawl.
(That is, to clarify, yes in general effort is spent for quality writing to be easily accessible (hence easily crawlable), but accessibility is relative to choice of seeds, and it in fact is the case that being easily accessible from Chinese web does not necessarily entail being easily accessible from English web.)

sanxiyn 10 Jun 2024 10:12 UTC
16 points
2
on: The Data Wall is Important
Modern AI is trained on a huge fraction of the internet
I want to push against this. The internet (or world wide web) is incredibly big. In fact we don’t know exactly how big it is, and measuring the size is a research problem!
When they say this what they mean is it is trained on a huge fraction of Common Crawl. Common Crawl is a crawl of world wide web that is free to use. But there are other crawls, and you could crawl world wide web yourself. Everyone uses Common Crawl because it is decent and crawling world wide web is itself a large engineering project.
But Common Crawl is not at all a complete crawl of world wide web. It is very far from being complete. For example, Google has its own proprietary crawl of world wide web (which you can access as Google cache). Probabilistic estimate of size of Google’s search index suggests it is 10x size of Common Crawl. And Google’s crawl is also not complete. Bing also has its own crawl.
It is known that Anthropic runs its own crawler called ClaudeBot. Web crawl is highly non-trivial engineering project, but it is also kind of well understood. (Although I heard that you continue to encounter new issues as you approach more and more extreme scales.) There are also failed search engines with their own web crawls and you could buy them.
There is also another independent web crawl that is public! Internet Archive has its own crawl, it is just less well known than Common Crawl. Recently someone made a use of Internet Archive crawl and analyzed overlap and difference with Common Crawl, see https://arxiv.org/abs/2403.14009.
If the data wall is a big problem, making a use of Internet Archive crawl is like the first obvious thing to try. But as far as I know, that 2024 paper is first public literature to do so. At least, any analysis of data wall should take into account both Common Crawl and Internet Archive crawl with overlap excluded, but I have never seen anyone doing this.
My overall point is that Common Crawl is not world wide web. It is not complete, and there are other crawls, both public and private. You can also crawl yourself, and we know AI labs do. How much does it help is unclear, but I think 10x is very likely, although probably not 100x.

sanxiyn 22 May 2024 13:27 UTC
5 points
1
in reply to: Chris_Leong’s comment on: EIS XIII: Reflections on Anthropic’s SAE Research Circa May 2024
I don’t think the post is saying the result is not valuable. The claim is that it underperformed expectation. Stock prices fall if they underperformed expectation, even if they are profitable. That does not mean they made loss.

sanxiyn 22 May 2024 13:22 UTC
4 points
1
in reply to: Sebastian Schmidt’s comment on: New voluntary commitments (AI Seoul Summit)
Unsure about this. Isn’t Qwen on Chatbot Arena Leaderboard, and is made by Alibaba?

sanxiyn 2 Mar 2024 4:47 UTC
8 points
1
in reply to: Gordon Seidoh Worley’s comment on: Elon Sues OpenAI
No. Traditionally, donors have no standing to sue charity. From https://www.thetaxadviser.com/issues/2021/sep/donor-no-standing-sue-donor-advised-fund.html
California limits by statute the persons who can sue for mismanagement of a charitable corporation’s assets. The court found that the claims raised by Pinkert for breach of a fiduciary duty for mismanagement of assets were claims for breach of a charitable trust. The court determined that under California law, a suit for breach of a charitable trust can be brought by the attorney general of California...

sanxiyn 27 Jul 2023 9:01 UTC
1 point
0
in reply to: jeff8765’s comment on: The First Room-Temperature Ambient-Pressure Superconductor
The patent is not yet granted.

sanxiyn 27 Jul 2023 8:58 UTC
2 points
0
on: The First Room-Temperature Ambient-Pressure Superconductor
Someone from South Korea is extremely skeptical and wrote a long thread going into paper’s details why it must be 100% false: https://twitter.com/AK2MARU/status/1684435312557314048. Sorry it’s in Korean, but we live in the age of miracle and serviceable machine translation.

sanxiyn 22 Jul 2023 22:00 UTC
3 points
1
on: A brief history of computers
But it wasn’t until the 1940s and the advent of the electronic computer that they actually built a machine that was used to construct mathematical tables. I’m confused...
You are confused because that is not the reality. As you can read on Wikipedia’s entry on difference engine, Scheutz built a difference engine derivative, sold it, and it was used to create logarithmic tables.
You must have read this while writing this article. It is prominent in the Wikipedia article in question and hard to miss. Why did you make this mistake? If it was a deliberate act of misleading for narrative convenience I am very disappointed. Yes, the reality is rarely narratively convenient, but you shouldn’t lie about it.

sanxiyn 6 Jul 2023 11:34 UTC
2 points
0
in reply to: cubefox’s comment on: [Linkpost] Introducing Superalignment
My median estimate has been 2028 (so 5 years). I first wrote down 2028 in 2016 (so 12 years after then), and during 7 years since, I barely moved the estimate. Things roughly happened when I expected them to.

sanxiyn 20 Jun 2023 3:17 UTC
1 point
0
in reply to: mic’s comment on: OpenAI introduces function calling for GPT-4
I am curious how this fine-tuning for function calling was done, because it is user controllable. In the OpenAI API, if you pass none to function_call parameter, the model never calls a function. There seem to be one input bit and one output bit, for “you may want to call a function” and “I want to call a function”.

sanxiyn

Next au­to­mated rea­son­ing grand challenge: CompCert

Next automated reasoning grand challenge: CompCert