harfe
In this case I have some independent verification:
I had formalized the same conjecture. My formalization was done independently and before this post went up (and was not written by AI). Now there is also a proof for my formalization of the problem (the proof uses David’s lean files and some small glue code to bridge the differences in formalization). I also ran the solution through comparator, which has more adversarial robustness than the standard lean type checking. This way I do not need to trust any AI output at all.
But I agree that in general this is a concern. For example, I have observed AI adding assumptions to make their job easier. See also previous discussion.
I do not understand how the debate results you describe are a crux for anything.
The Lean code includes his finite claim-tree debate game
This specific debate approach to calculating boolean formulas does not appear in the linked paper (and can be solved in linear time by the judge without debaters.)
and a one-judge-error-flips-certification result. From that it follows that one judge error flips the outcome, and that leads to false certification.
This sounds like a general statement, but the proof actually only considers a specific example where the judge is wrong and the result is wrong, which is a trivial result.
Fable: theorem debate_truth_separated_from_judge_correction_step
This looks like Fable just gave you trivial inequalities with integers there, but dressed it up by using variable names related to debate.
In general, I do find it suspect that your AI agent seems to like the
axiomkeyword a lot when writing lean code.I tried to reduce each open problem to a proposition that can be true or false.
If you actually could describe (open or resolved) propositions that are reductions of alignment-relevant open problems, that could be important (and those propositions could then receive more research attention). But from looking at the debate example, I am skeptical that your setup produces meaningful propositions.
Definition: Probability distributions on histories induced by a policy and environment
The probability distribution as defined does not sum up to 1. I think it should be
It also feels like a definition defining
For the orbital data centers, it makes more sense if you think of it as many small satellites rather then a few big ones.
SpaceX’s FCC filing talks of up to one million satellites in sun-synchronous orbit, (PDF here).
This makes the issues with cooling more manageable. The starlink v3 satellites are supposed to have 20kw of power each, so radiating out this waste heat on these scales is not impossible (Elon tweets about ~100kw per ton of satellite, and designing GPUs to run at higher temperatures).
Such an orbital GPU cloud would make more sense for inference, not training.
Overall I am not yet convinced that this is competitive with earth-based data centers, but it seems less stupid than I imagined at first.
For the purpose of whistle-blowing, I wonder whether Signal could be used as a source of keys tied to identities of real people. The advantage would be that lots of OpenBrain employees might already use signal. But there are certainly some difficulties:
Ring signatures can not be publicly verified, but they could be verified by a journalist who gets their hands on lots of Signal contacts of OpenBrain employees.
Verifying that all the signal contacts in the ring actually belong to OpenBrain employees is difficult.
The public keys are not visible in the normal signal client, so specialized tools would need to be created.
There was report that the CIA used a new tool called Ghost Murmur to detect the electromagnetic signals of a human heart from (40?) miles away, using long-range quantum magnetometry.
See also Wikipedia.
My first guess (and still a hypothesis) is that this is deliberate disinformation by the US, but i do not have the expertise required to judge the plausibility. In any case, it could have been an interesting question on the “Could a superintelligence do that?” quiz show.
Is any of the lean code public? That could give a better sense of what to expect. Saying that they are working on a “skeletal Lean code” could be very little compared to what would be required to convince other mathematicians.
Yesterday they also did an exclusive interview with Sam Altman
I learned that undersea data centers are possible. Microsoft had Project Natick, but it looks like they abandoned it. There is also a chinese project and a western startup. The main benefit seems to be reduced cooling costs.
Canada also uses FPTP, so this is not the example you should be using for examining alternatives.
Proportional representation, which is common in continental Europe, does result in a diversity of parties in practice.
There’s no bigger narrative than the one AI industry leaders have been pushing since before the boom: AGI will soon be able to do just about anything a human can do, and will usher in an age of superpowerful technology the likes of which we can only begin to imagine. Jobs will be automated, industries transformed, cancer cured, climate change solved; AI will do quite literally everything.
The article unfortunately does not seriously consider the possibility that AGI has the potential to automate most jobs in a few years. The large investments into AI would be justified in this case, even if current revenue is small! I think this is an important difference to past bubbles.
OpenAI, Anthropic, and the AI-embracing tech giants are burning through billions, inference costs haven’t fallen (those companies still lose money on nearly every user query), and the long-term viability of their enterprise programs are a big question mark at best.
The part about inference costs seems false, unless they mean total inference costs of all their instances.
Most[1] problems with unbounded utility functions go away if you restrict yourself to summable utility functions[2]. Summable utility functions can still be unbounded.
For example, if each planet in the universe gives you 1 utility, and for , then your utility function is unbounded but summable. In such a universe it would be very unlikely for a casino to hand out a large number of planets.
Your proof relies on the assumption
assuming that the casino has unbounded utility to hand out.
and this assumption would be wrong in my example.
Note that GWWC is shutting down their donor lottery, among other things: https://forum.effectivealtruism.org/posts/f7yQFP3ZhtfDkD7pr/gwwc-is-retiring-10-initiatives
Mid 2027 seems too late to me for such a candidate to start the official campaign.
For the 2020 presidential election, many democratic candidates announced their campaign in early 2019, and Yang already in 2017. Debates happened already in June 2019. As a likely unknown candidate, you probably need a longer run time to accumulate a bit of fame.
Also Musk’s regulatory plan is polling well
What plan are you referring to? Is this something AI safety specific?
I wouldn’t say so, I don’t think his campaign has made UBI advocacy more difficult.
But an AI notkilleveryoneism campaign seems more risky. It could end up making the worries look silly, for example.
Their platform would be whatever version and framing of AI notkilleveryoneism the candidates personally endorse, plus maybe some other smaller things. They should be open that they consider the potential human disempowerment or extinction to be the main problem of our time.
As for the concrete policy proposals, I am not sure. The focus could be on international treaties, or banning or heavy regulation of AI models who were trained with more than a trillion quadrillion (10^27) operations. (not sure I understand the intent behind your question).
A potentially impactful thing: someone competent runs as a candidate for the 2028 election on an AI notkilleveryoneism[1] platform. Maybe even two people should run, one for the democratic primary, and one in the republican primary. While getting the nomination is rather unlikely, there could be lots of benefits even if you fail to gain the nomination (like other presidential candidates becoming sympathetic to AI notkilleveryoneism, or more popularity of AI notkilleveryoneism in the population, etc.)
On the other hand, attempting a presidential run can easily backfire.
A relevant previous example to this kind of approach is the 2020 campaign by Andrew Yang, which focussed on universal basic income (and downsides of automation). While the campaign attracted some attention, it seems like it didn’t succeed in making UBI a popular policy among democrats.
- ↩︎
Not necessarily using that name.
- ↩︎
This can easily be done in the cryptographic example above: B can sample a new number , and then present to a fresh copy of A that has not seen the transcript for so far.
I don’t understand how this is supposed to help. I guess the point is to somehow catch a fresh copy of A in a lie about a problem that is different from the original problem, and conclude that A is the dishonest debater?
But couldn’t A just answer “I don’t know”?
Even if it is a fresh copy, it would notice that it does not know the secret factors, so it could display different behavior than in the case where A knows the secret factors .
If they decided to throw the kitchen sink at trying to beat them to it, they might also have decided to look at the logs. They also could have decided to do some finetuning on a subset of recent codex sessions instead of looking at the logs directly.