What are the benefits of storing known_hosts in a hashed form? From what I read, it is supposed to protect the list of servers I am connecting to, presumably in a scenario where my account has been compromised (and known_hosts file stolen) 

If my account were indeed to be compromised, having known_hosts hashed would be very little consolation. An attacker could see from my bash history to which servers I am connecting. And also from my .ssh/config where all my servers are listed.

Are there any benefits that I am missing in my description here?

I don't think you are missing much.  The only change is that if a machine is compromised, the idea is to minimize how much usable information is given to an attacker.  In the known_hosts file, more information is not necessary to include (computing a few hundred HMACs is not onerous work), unlike in ~/.ssh/config where it needs to be included on the Address line if you wish to connect via your alias (hashing wouldn't work) and in your command line history - if you choose to keep one.

Presumably you could have a very large known_hosts (e.g., if you sync it with another computer when you setup the account), but say not use .ssh/config and not keep a command line history or have never connected to most machines in the commandline history.

In those situations, hashing the IP addresses used in your known_hosts could lessen exposure in the event of a compromise.

Furthermore, HashKnownHosts is a configurable option, and the default is to not hash (probably for reasons you specified -- it doesn't help much).  See man ssh_config:


  HashKnownHosts
  
  Indicates that ssh(1) should hash host names and addresses when they are added to ~/.ssh/known_hosts.
  These hashed names may be used normally by ssh(1) and sshd(8), but they do not reveal identifying information should the file's contents be disclosed.  The default is “no”.  Note that existing names and addresses in known hosts files will not be converted automatically, but may be manually hashed using ssh-keygen(1).  Use of this option may break facilities such as tab-completion that rely on being able to read unhashed host names from ~/.ssh/known_hosts.




Note the format of a hashed known_hosts line (example taken from here - my current configuration is not to hash) for an entry for 192.168.1.61:

|1|F1E1KeoE/eEWhi10WpGv4OdiO6Y=|3988QV0VE8wmZL7suNrYQLITLCg= ssh-rsa ... 


where the first part F1E1KeoE/eEWhi10WpGv4OdiO6Y= is a random salt - that acts as a key for the HMAC-SHA1 to hash 192.168.1.61.

You can verify in the command line with (BSD / Mac OS X):

#### key=`echo F1E1KeoE/eEWhi10WpGv4OdiO6Y= | base64 -D | xxd -p`
#### echo -n "192.168.1.61" | openssl sha1 -mac HMAC -macopt hexkey:$key|awk '{print $2}' | xxd -r -p|base64
3988QV0VE8wmZL7suNrYQLITLCg=


or on GNU/linux with:

#### key=`echo F1E1KeoE/eEWhi10WpGv4OdiO6Y= | base64 -d | xxd -p`
#### echo -n "192.168.1.61" | openssl sha1 -mac HMAC -macopt hexkey:$key|awk '{print $2}' | xxd -r -p|base64
3988QV0VE8wmZL7suNrYQLITLCg=


where we just decoded the salt and used it as a key in a sha1 HMAC, and then re-encode the hash in base64.  Just specifying as another answer originally presumed that the HMAC may have used the user's private ssh key to compute hash-based message authentication code, but this is not the case.
